internlm/Lean-Github huggingface dataset:
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
case neg
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c ↔ b = c
Tactic:
constructor
Proof state after:
case neg.mp
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c → b = c

case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
case neg.mp
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c → b = c

case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c
Tactic:
. exact Nat.eq_of_mul_eq_mul_left zero_lt_a
Proof state after:
case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c
Tactic:
. intro h
  rw [h]
Proof state after:
no goals
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
case neg.mp
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c → b = c
Tactic:
exact Nat.eq_of_mul_eq_mul_left zero_lt_a
Proof state after:
no goals
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c
Tactic:
intro h
Proof state after:
case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
h : b = c
⊢ a * b = a * c
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
h : b = c
⊢ a * b = a * c
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Misc.Nat.mod_add_div
Proof state before:
m k : Nat
⊢ m % k + k * (m / k) = m
Tactic:
induction m, k using Nat.mod.inductionOn with rw [Nat.div_eq, Nat.mod_eq]
| base x y h => simp only [h, ite_false, Nat.mul_zero, Nat.add_zero]
| ind x y h IH =>
  simp only [h, and_self, ite_true]
  rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]
Proof state after:
no goals
Theorem: Misc.Nat.mod_add_div
Proof state before:
case base
x y : Nat
h : ¬(0 < y ∧ y ≤ x)
⊢ ((if 0 < y ∧ y ≤ x then (x - y) % y else x) + y * if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0) = x
Tactic:
simp only [h, ite_false, Nat.mul_zero, Nat.add_zero]
Proof state after:
no goals
Theorem: Misc.Nat.mod_add_div
Proof state before:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
IH : (x - y) % y + y * ((x - y) / y) = x - y
⊢ ((if 0 < y ∧ y ≤ x then (x - y) % y else x) + y * if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0) = x
Tactic:
simp only [h, and_self, ite_true]
Proof state after:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
IH : (x - y) % y + y * ((x - y) / y) = x - y
⊢ (x - y) % y + y * ((x - y) / y + 1) = x
Theorem: Misc.Nat.mod_add_div
Proof state before:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
IH : (x - y) % y + y * ((x - y) / y) = x - y
⊢ (x - y) % y + y * ((x - y) / y + 1) = x
Tactic:
rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]
Proof state after:
no goals
Theorem: Misc.Nat.even_iff
Proof state before:
n : Nat
x✝ : Even n
m : Nat
hm : n = m + m
⊢ n % 2 = 0
Tactic:
simp only [hm, ← Nat.two_mul, Nat.mul_mod_right]
Proof state after:
no goals
Theorem: Misc.Nat.even_iff
Proof state before:
n : Nat
h : n % 2 = 0
⊢ n % 2 + 2 * (n / 2) = n / 2 + n / 2
Tactic:
simp only [h, Nat.zero_add, Nat.two_mul]
Proof state after:
no goals
Theorem: Misc.Nat.odd_iff
Proof state before:
n : Nat
x✝ : Odd n
m : Nat
hm : n = 2 * m + 1
⊢ n % 2 = 1
Tactic:
rw [hm, Nat.add_mod, Nat.mul_mod_right]
Proof state after:
no goals
Theorem: Misc.Nat.odd_iff
Proof state before:
n : Nat
h : n % 2 = 1
⊢ n % 2 + 2 * (n / 2) = 2 * (n / 2) + 1
Tactic:
rw [h, Nat.add_comm]
Proof state after:
no goals
Theorem: Misc.Nat.odd_succ_of_even
Proof state before:
n : Nat
⊢ Even n → Odd n.succ
Tactic:
intro ⟨r, hr⟩
Proof state after:
n r : Nat
hr : n = r + r
⊢ Odd n.succ
Theorem: Misc.Nat.odd_succ_of_even
Proof state before:
n r : Nat
hr : n = r + r
⊢ Odd n.succ
Tactic:
exists r
Proof state after:
n r : Nat
hr : n = r + r
⊢ n.succ = 2 * r + 1
Theorem: Misc.Nat.odd_succ_of_even
Proof state before:
n r : Nat
hr : n = r + r
⊢ n.succ = 2 * r + 1
Tactic:
simp_arith [hr]
Proof state after:
no goals
Theorem: Misc.Nat.even_succ_of_odd
Proof state before:
n : Nat
⊢ Odd n → Even n.succ
Tactic:
intro ⟨r, hr⟩
Proof state after:
n r : Nat
hr : n = 2 * r + 1
⊢ Even n.succ
Theorem: Misc.Nat.even_succ_of_odd
Proof state before:
n r : Nat
hr : n = 2 * r + 1
⊢ Even n.succ
Tactic:
exists (r+1)
Proof state after:
n r : Nat
hr : n = 2 * r + 1
⊢ n.succ = r + 1 + (r + 1)
Theorem: Misc.Nat.even_succ_of_odd
Proof state before:
n r : Nat
hr : n = 2 * r + 1
⊢ n.succ = r + 1 + (r + 1)
Tactic:
simp_arith [*]
Proof state after:
no goals
Theorem: Misc.Nat.two_div_iff_even
Proof state before:
n : Nat
⊢ 2 ∣ n ↔ Even n
Tactic:
unfold Even
Proof state after:
n : Nat
⊢ 2 ∣ n ↔ ∃ r, n = r + r
Theorem: Misc.Nat.two_div_iff_even
Proof state before:
n : Nat
⊢ 2 ∣ n ↔ ∃ r, n = r + r
Tactic:
simp only [← Nat.two_mul]
Proof state after:
n : Nat
⊢ 2 ∣ n ↔ ∃ r, n = 2 * r
Theorem: Misc.Nat.two_div_iff_even
Proof state before:
n : Nat
⊢ 2 ∣ n ↔ ∃ r, n = 2 * r
Tactic:
constructor
Proof state after:
case mp
n : Nat
⊢ 2 ∣ n → ∃ r, n = 2 * r

case mpr
n : Nat
⊢ (∃ r, n = 2 * r) → 2 ∣ n
Theorem: Misc.Nat.two_div_iff_even
Proof state before:
case mp
n : Nat
⊢ 2 ∣ n → ∃ r, n = 2 * r

case mpr
n : Nat
⊢ (∃ r, n = 2 * r) → 2 ∣ n
Tactic:
all_goals
  intro heven
  rcases heven with ⟨i, hi⟩
  exists i
Proof state after:
no goals
Theorem: Misc.Nat.two_div_iff_even
Proof state before:
case mpr
n : Nat
⊢ (∃ r, n = 2 * r) → 2 ∣ n
Tactic:
intro heven
Proof state after:
case mpr
n : Nat
heven : ∃ r, n = 2 * r
⊢ 2 ∣ n
Theorem: Misc.Nat.two_div_iff_even
Proof state before:
case mpr
n : Nat
heven : ∃ r, n = 2 * r
⊢ 2 ∣ n
Tactic:
rcases heven with ⟨i, hi⟩
Proof state after:
case mpr.intro
n i : Nat
hi : n = 2 * i
⊢ 2 ∣ n
Theorem: Misc.Nat.two_div_iff_even
Proof state before:
case mpr.intro
n i : Nat
hi : n = 2 * i
⊢ 2 ∣ n
Tactic:
exists i
Proof state after:
no goals
Theorem: Misc.Nat.mod_two_ne_zero
Proof state before:
n : Nat
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
rcases Nat.mod_two_eq_zero_or_one n with h | h
Proof state after:
case inl
n : Nat
h : n % 2 = 0
⊢ ¬n % 2 = 0 ↔ n % 2 = 1

case inr
n : Nat
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Theorem: Misc.Nat.mod_two_ne_zero
Proof state before:
case inl
n : Nat
h : n % 2 = 0
⊢ ¬n % 2 = 0 ↔ n % 2 = 1

case inr
n : Nat
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
. simp (config := { decide := true}) only [h]
Proof state after:
case inr
n : Nat
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Theorem: Misc.Nat.mod_two_ne_zero
Proof state before:
case inr
n : Nat
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
. simp (config := { decide := true}) only [h]
Proof state after:
no goals
Theorem: Misc.Nat.mod_two_ne_zero
Proof state before:
case inl
n : Nat
h : n % 2 = 0
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
simp (config := { decide := true}) only [h]
Proof state after:
no goals
Theorem: Misc.Nat.mod_two_ne_zero
Proof state before:
case inr
n : Nat
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
simp (config := { decide := true}) only [h]
Proof state after:
no goals
Theorem: Misc.Nat.mul_div_cancel_left'
Proof state before:
a b : Nat
Hd : a ∣ b
⊢ a * (b / a) = b
Tactic:
rw [Nat.mul_comm, Nat.div_mul_cancel Hd]
Proof state after:
no goals
Theorem: Misc.Nat.not_even_iff
Proof state before:
n : Nat
⊢ ¬Even n ↔ n % 2 = 1
Tactic:
rw [even_iff, mod_two_ne_zero]
Proof state after:
no goals
Theorem: Misc.Nat.odd_iff_not_even
Proof state before:
n : Nat
⊢ Odd n ↔ ¬Even n
Tactic:
rw [not_even_iff, odd_iff]
Proof state after:
no goals
Theorem: Misc.Nat.not_odd_iff_even
Proof state before:
n : Nat
⊢ ¬Odd n ↔ Even n
Tactic:
rw [odd_iff_not_even, Classical.not_not]
Proof state after:
no goals
Theorem: Misc.Nat.odd_pred_of_even
Proof state before:
n : Nat
h : n > 0
⊢ Even n → Odd (n - 1)
Tactic:
intro
Proof state after:
n : Nat
h : n > 0
a✝ : Even n
⊢ Odd (n - 1)
Theorem: Misc.Nat.odd_pred_of_even
Proof state before:
n : Nat
h : n > 0
a✝ : Even n
⊢ Odd (n - 1)
Tactic:
apply Classical.byContradiction
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Even n
⊢ ¬Odd (n - 1) → False
Theorem: Misc.Nat.odd_pred_of_even
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Even n
⊢ ¬Odd (n - 1) → False
Tactic:
intro h'
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
⊢ False
Theorem: Misc.Nat.odd_pred_of_even
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
⊢ False
Tactic:
have := Iff.mp Nat.not_odd_iff_even h'
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this : Even (n - 1)
⊢ False
Theorem: Misc.Nat.odd_pred_of_even
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this : Even (n - 1)
⊢ False
Tactic:
have : Odd (n - 1 + 1) := Nat.odd_succ_of_even this
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝ : Even (n - 1)
this : Odd (n - 1 + 1)
⊢ False
Theorem: Misc.Nat.odd_pred_of_even
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝ : Even (n - 1)
this : Odd (n - 1 + 1)
⊢ False
Tactic:
rw [Nat.sub_add_cancel h] at this
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝ : Even (n - 1)
this : Odd n
⊢ False
Theorem: Misc.Nat.odd_pred_of_even
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝ : Even (n - 1)
this : Odd n
⊢ False
Tactic:
have := Iff.mp Nat.odd_iff_not_even this
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝¹ : Even (n - 1)
this✝ : Odd n
this : ¬Even n
⊢ False
Theorem: Misc.Nat.odd_pred_of_even
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝¹ : Even (n - 1)
this✝ : Odd n
this : ¬Even n
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Misc.Nat.even_pred_of_odd
Proof state before:
n : Nat
h : n > 0
⊢ Odd n → Even (n - 1)
Tactic:
intro
Proof state after:
n : Nat
h : n > 0
a✝ : Odd n
⊢ Even (n - 1)
Theorem: Misc.Nat.even_pred_of_odd
Proof state before:
n : Nat
h : n > 0
a✝ : Odd n
⊢ Even (n - 1)
Tactic:
apply Classical.byContradiction
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Odd n
⊢ ¬Even (n - 1) → False
Theorem: Misc.Nat.even_pred_of_odd
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Odd n
⊢ ¬Even (n - 1) → False
Tactic:
intro h'
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
⊢ False
Theorem: Misc.Nat.even_pred_of_odd
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
⊢ False
Tactic:
have := Iff.mpr Nat.odd_iff_not_even h'
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this : Odd (n - 1)
⊢ False
Theorem: Misc.Nat.even_pred_of_odd
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this : Odd (n - 1)
⊢ False
Tactic:
have : Even (n - 1 + 1) := Nat.even_succ_of_odd this
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝ : Odd (n - 1)
this : Even (n - 1 + 1)
⊢ False
Theorem: Misc.Nat.even_pred_of_odd
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝ : Odd (n - 1)
this : Even (n - 1 + 1)
⊢ False
Tactic:
rw [Nat.sub_add_cancel h] at this
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝ : Odd (n - 1)
this : Even n
⊢ False
Theorem: Misc.Nat.even_pred_of_odd
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝ : Odd (n - 1)
this : Even n
⊢ False
Tactic:
have := Iff.mpr Nat.not_odd_iff_even this
Proof state after:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝¹ : Odd (n - 1)
this✝ : Even n
this : ¬Odd n
⊢ False
Theorem: Misc.Nat.even_pred_of_odd
Proof state before:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝¹ : Odd (n - 1)
this✝ : Even n
this : ¬Odd n
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Misc.Nat.even_xor_odd
Proof state before:
n : Nat
⊢ Xor' (Even n) (Odd n)
Tactic:
simp only [Xor', odd_iff_not_even, Classical.not_not, and_self, Decidable.em (Even n)]
Proof state after:
no goals
Theorem: Misc.Nat.sub_mod_eq_zero_of_mod_eq
Proof state before:
m n k : Nat
h : m % k = n % k
⊢ (m - n) % k = 0
Tactic:
rw [← Nat.mod_add_div m k, ← Nat.mod_add_div n k, ← h, Nat.sub_add_eq,
  Nat.add_sub_cancel_left, ← Nat.mul_sub_left_distrib, Nat.mul_mod_right]
Proof state after:
no goals
Theorem: Misc.Array.range_size
Proof state before:
n : Nat
⊢ (Array.range n).size = n
Tactic:
induction n
Proof state after:
case zero

⊢ (Array.range 0).size = 0

case succ
n✝ : Nat
a✝ : (Array.range n✝).size = n✝
⊢ (Array.range (n✝ + 1)).size = n✝ + 1
Theorem: Misc.Array.range_size
Proof state before:
case zero

⊢ (Array.range 0).size = 0

case succ
n✝ : Nat
a✝ : (Array.range n✝).size = n✝
⊢ (Array.range (n✝ + 1)).size = n✝ + 1
Tactic:
. decide
Proof state after:
case succ
n✝ : Nat
a✝ : (Array.range n✝).size = n✝
⊢ (Array.range (n✝ + 1)).size = n✝ + 1
Theorem: Misc.Array.range_size
Proof state before:
case succ
n✝ : Nat
a✝ : (Array.range n✝).size = n✝
⊢ (Array.range (n✝ + 1)).size = n✝ + 1
Tactic:
. next n ih =>
  simp only [Array.range, Nat.fold, flip, Array.size_push, Nat.succ.injEq]
  simp only [Array.range, flip] at ih
  exact ih
Proof state after:
no goals
Theorem: Misc.Array.range_size
Proof state before:
case zero

⊢ (Array.range 0).size = 0
Tactic:
decide
Proof state after:
no goals
Theorem: Misc.Array.range_size
Proof state before:
case succ
n✝ : Nat
a✝ : (Array.range n✝).size = n✝
⊢ (Array.range (n✝ + 1)).size = n✝ + 1
Tactic:
next n ih =>
simp only [Array.range, Nat.fold, flip, Array.size_push, Nat.succ.injEq]
simp only [Array.range, flip] at ih
exact ih
Proof state after:
no goals
Theorem: Misc.Array.range_size
Proof state before:
n : Nat
ih : (Array.range n).size = n
⊢ (Array.range (n + 1)).size = n + 1
Tactic:
simp only [Array.range, Nat.fold, flip, Array.size_push, Nat.succ.injEq]
Proof state after:
n : Nat
ih : (Array.range n).size = n
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size = n
Theorem: Misc.Array.range_size
Proof state before:
n : Nat
ih : (Array.range n).size = n
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size = n
Tactic:
simp only [Array.range, flip] at ih
Proof state after:
n : Nat
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n)).size = n
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size = n
Theorem: Misc.Array.range_size
Proof state before:
n : Nat
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n)).size = n
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size = n
Tactic:
exact ih
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
n x : Nat
h : x < n
⊢ x < (Array.range n).size
Tactic:
rw [Array.range_size]
Proof state after:
n x : Nat
h : x < n
⊢ x < n
Theorem: Misc.Array.range_idx
Proof state before:
n x : Nat
h : x < n
⊢ x < n
Tactic:
exact h
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
n x : Nat
h : x < n
⊢ (Array.range n)[x] = x
Tactic:
induction n
Proof state after:
case zero
x : Nat
h : x < 0
⊢ (Array.range 0)[x] = x

case succ
x n✝ : Nat
a✝ : ∀ (h : x < n✝), (Array.range n✝)[x] = x
h : x < n✝ + 1
⊢ (Array.range (n✝ + 1))[x] = x
Theorem: Misc.Array.range_idx
Proof state before:
case zero
x : Nat
h : x < 0
⊢ (Array.range 0)[x] = x

case succ
x n✝ : Nat
a✝ : ∀ (h : x < n✝), (Array.range n✝)[x] = x
h : x < n✝ + 1
⊢ (Array.range (n✝ + 1))[x] = x
Tactic:
. contradiction
Proof state after:
case succ
x n✝ : Nat
a✝ : ∀ (h : x < n✝), (Array.range n✝)[x] = x
h : x < n✝ + 1
⊢ (Array.range (n✝ + 1))[x] = x
Theorem: Misc.Array.range_idx
Proof state before:
case succ
x n✝ : Nat
a✝ : ∀ (h : x < n✝), (Array.range n✝)[x] = x
h : x < n✝ + 1
⊢ (Array.range (n✝ + 1))[x] = x
Tactic:
. next n ih =>
  rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ h with x_lt_n | x_eq_n
  . specialize ih x_lt_n
    simp only [Array.range, Nat.fold, flip, Array.get_push]
    simp only [Array.range, flip] at ih
    split
    . exact ih
    . next x_ge_n =>
      exfalso
      have h_range_size : (Array.range n).size = n := Array.range_size
      simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
      simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
      exact x_ge_n x_lt_n
  . simp only [Array.range, Nat.fold, flip, Array.get_push]
    split
    . next x_lt_n =>
      exfalso
      have h_range_size : (Array.range n).size = n := Array.range_size
      simp only [Array.range, Array.mkEmpty_eq] at h_range_size
      simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
    . rw [x_eq_n]
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
case zero
x : Nat
h : x < 0
⊢ (Array.range 0)[x] = x
Tactic:
contradiction
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
case succ
x n✝ : Nat
a✝ : ∀ (h : x < n✝), (Array.range n✝)[x] = x
h : x < n✝ + 1
⊢ (Array.range (n✝ + 1))[x] = x
Tactic:
next n ih =>
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ h with x_lt_n | x_eq_n
. specialize ih x_lt_n
  simp only [Array.range, Nat.fold, flip, Array.get_push]
  simp only [Array.range, flip] at ih
  split
  . exact ih
  . next x_ge_n =>
    exfalso
    have h_range_size : (Array.range n).size = n := Array.range_size
    simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
    simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
    exact x_ge_n x_lt_n
. simp only [Array.range, Nat.fold, flip, Array.get_push]
  split
  . next x_lt_n =>
    exfalso
    have h_range_size : (Array.range n).size = n := Array.range_size
    simp only [Array.range, Array.mkEmpty_eq] at h_range_size
    simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
  . rw [x_eq_n]
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
⊢ (Array.range (n + 1))[x] = x
Tactic:
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ h with x_lt_n | x_eq_n
Proof state after:
case inl
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_lt_n : x < n
⊢ (Array.range (n + 1))[x] = x

case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (Array.range (n + 1))[x] = x
Theorem: Misc.Array.range_idx
Proof state before:
case inl
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_lt_n : x < n
⊢ (Array.range (n + 1))[x] = x

case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (Array.range (n + 1))[x] = x
Tactic:
. specialize ih x_lt_n
  simp only [Array.range, Nat.fold, flip, Array.get_push]
  simp only [Array.range, flip] at ih
  split
  . exact ih
  . next x_ge_n =>
    exfalso
    have h_range_size : (Array.range n).size = n := Array.range_size
    simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
    simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
    exact x_ge_n x_lt_n
Proof state after:
case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (Array.range (n + 1))[x] = x
Theorem: Misc.Array.range_idx
Proof state before:
case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (Array.range (n + 1))[x] = x
Tactic:
. simp only [Array.range, Nat.fold, flip, Array.get_push]
  split
  . next x_lt_n =>
    exfalso
    have h_range_size : (Array.range n).size = n := Array.range_size
    simp only [Array.range, Array.mkEmpty_eq] at h_range_size
    simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
  . rw [x_eq_n]
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
case inl
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_lt_n : x < n
⊢ (Array.range (n + 1))[x] = x
Tactic:
specialize ih x_lt_n
Proof state after:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Array.range n)[x] = x
⊢ (Array.range (n + 1))[x] = x
Theorem: Misc.Array.range_idx
Proof state before:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Array.range n)[x] = x
⊢ (Array.range (n + 1))[x] = x
Tactic:
simp only [Array.range, Nat.fold, flip, Array.get_push]
Proof state after:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Array.range n)[x] = x
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x
Theorem: Misc.Array.range_idx
Proof state before:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Array.range n)[x] = x
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x
Tactic:
simp only [Array.range, flip] at ih
Proof state after:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x
Theorem: Misc.Array.range_idx
Proof state before:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x
Tactic:
split
Proof state after:
case inl.isTrue
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x

case inl.isFalse
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Theorem: Misc.Array.range_idx
Proof state before:
case inl.isTrue
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x

case inl.isFalse
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
. exact ih
Proof state after:
case inl.isFalse
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Theorem: Misc.Array.range_idx
Proof state before:
case inl.isFalse
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
. next x_ge_n =>
  exfalso
  have h_range_size : (Array.range n).size = n := Array.range_size
  simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
  simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
  exact x_ge_n x_lt_n
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
case inl.isTrue
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x
Tactic:
exact ih
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
case inl.isFalse
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
next x_ge_n =>
exfalso
have h_range_size : (Array.range n).size = n := Array.range_size
simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
exact x_ge_n x_lt_n
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
exfalso
Proof state after:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ False