From be2e2cb70e47abb9d3d39b5f4941ecaa50fd9444 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Feb 2022 17:20:17 -0800 Subject: [PATCH] chore: adjust proofs affected by update stage0 --- src/Init/Data/Nat/Linear.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean index fd69eff192..0ac61fcdb4 100644 --- a/src/Init/Data/Nat/Linear.lean +++ b/src/Init/Data/Nat/Linear.lean @@ -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