From 9dbd9ec55433d50e19fba42756c242bee8d650a5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Nov 2022 07:52:54 -0800 Subject: [PATCH] chore: fix build --- src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/Nat/Linear.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 88e7ce615f..0f6f1b5412 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -583,7 +583,7 @@ theorem ext (a b : Array α) have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ have headEq : a = b := h₂ 0 hz₁ hz₂ - have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁; assumption + have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁ have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by intro i hi₁ hi₂ have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean index a5ef959918..667af7dfce 100644 --- a/src/Init/Data/Nat/Linear.lean +++ b/src/Init/Data/Nat/Linear.lean @@ -617,7 +617,7 @@ attribute [local simp] PolyCnstr.denote_combine theorem Poly.isNum?_eq_some (ctx : Context) {p : Poly} {k : Nat} : p.isNum? = some k → p.denote ctx = k := by simp [isNum?] split - next => intro h; injection h; subst k; simp + next => intro h; injection h next k v => by_cases h : v == fixedVar <;> simp [h]; intros; simp [Var.denote, eq_of_beq h]; assumption next => intros; contradiction