max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: adjust proofs affected by update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2022-02-24 17:20:17 -08:00
parent 7480670c6a
commit be2e2cb70e
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/Nat/Linear.lean
View file

@ -320,7 +320,7 @@ theorem Poly.of_denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
| succ fuel ih =>
simp at h
split at h <;> simp <;> try assumption
rename_i k₁ v₁ m₁ k₂ v₂ m₂ h
rename_i k₁ v₁ m₁ k₂ v₂ m₂
by_cases hltv : v₁ < v₂ <;> simp [hltv] at h
. have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
. by_cases hgtv : v₁ > v₂ <;> simp [hgtv] at h
@ -399,7 +399,7 @@ theorem Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
| succ fuel ih =>
simp at h
split at h <;> simp <;> try assumption
rename_i k₁ v₁ m₁ k₂ v₂ m₂ h
rename_i k₁ v₁ m₁ k₂ v₂ m₂
by_cases hltv : v₁ < v₂ <;> simp [hltv] at h
. have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
. by_cases hgtv : v₁ > v₂ <;> simp [hgtv] at h