awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
m n : ℕ
inst : NeZero m
h : m ≤ n
a : ℕ
⊢ castLE h (↑a : Fin m) = (↑(a % m) : Fin n)
have h₁ : (↑(castLE h (↑a : Fin m)) : ℕ) = (↑(↑(a % m) : Fin n) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
m n : ℕ
inst : NeZero m
h : m ≤ n
a : ℕ
⊢ a % m = a % m % n
have h₁ : a % m = a % m
Tactic: rw [Nat.mod_eq_of_lt (a := a % m) (lt_of_lt_of_le (Nat.mod_lt _ m.pos_of_neZero) h)]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n m : ℕ
i : Fin (m * n)
⊢ i.rev.modNat = i.modNat.rev
have h : (↑i.rev.modNat : ℕ) = (↑i.modNat.rev : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (hypothesis)
Goal:
n m : ℕ
i : Fin (m * n)
⊢ (↑i.rev.modNat : ℕ) = (↑i.modNat.rev : ℕ)
have H₁ : (↑i : ℕ) % n + 1 ≤ n
Tactic: have H₁ : i % n + 1 ≤ n := i.modNat.is_lt
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (hypothesis)
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
⊢ (↑i.rev.modNat : ℕ) = (↑i.modNat.rev : ℕ)
have H₂ : (↑i : ℕ) / n < m
Tactic: have H₂ : i / n < m := i.divNat.is_lt
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
⊢ (m * n - ((↑i : ℕ) + 1)) % n = (m * n - ((↑i : ℕ) / n * n + (↑i : ℕ) % n + 1)) % n
have rw : (m * n - ((↑i : ℕ) + 1)) % n = (m * n - ((↑i : ℕ) + 1)) % n
Tactic: rw [Nat.div_add_mod']
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
⊢ (m * n - ((↑i : ℕ) / n * n + (↑i : ℕ) % n + 1)) % n = ((m - (↑i : ℕ) / n - 1) * n + (n - ((↑i : ℕ) % n + 1))) % n
have rw : n ≤ (m - (↑i : ℕ) / n) * n
Tactic: rw [Nat.mul_sub_right_distrib, Nat.one_mul, Nat.sub_add_sub_cancel _ H₁,
        Nat.mul_sub_right_distrib, Nat.sub_sub, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
⊢ ((m - (↑i : ℕ) / n - 1) * n + (n - ((↑i : ℕ) % n + 1))) % n = n - ((↑i : ℕ) % n + 1)
have rw : n - ((↑i : ℕ) % n + 1) < n
Tactic: rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
⊢ (↑i.rev.modNat : ℕ) = n - ((↑i.modNat : ℕ) + 1)
have n₁ : (m * n - ((↑i : ℕ) + 1)) % n = (m * n - ((↑i : ℕ) / n * n + (↑i : ℕ) % n + 1)) % n
Tactic: calc
    (m * n - (i + 1)) % n = (m * n - ((i / n) * n + i % n + 1)) % n := by rw [Nat.div_add_mod']
    _ = ((m - i / n - 1) * n + (n - (i % n + 1))) % n := by
      rw [Nat.mul_sub_right_distrib, Nat.one_mul, Nat.sub_add_sub_cancel _ H₁,
        Nat.mul_sub_right_distrib, Nat.sub_sub, Nat.add_assoc]
      exact Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂
    _ = n - (i % n + 1) := by
      rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt]; exact i.modNat.rev.is_lt
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
n₁ : (m * n - ((↑i : ℕ) + 1)) % n = (m * n - ((↑i : ℕ) / n * n + (↑i : ℕ) % n + 1)) % n
⊢ (↑i.rev.modNat : ℕ) = n - ((↑i.modNat : ℕ) + 1)
have n₂ : (m * n - ((↑i : ℕ) / n * n + (↑i : ℕ) % n + 1)) % n = ((m - (↑i : ℕ) / n - 1) * n + (n - ((↑i : ℕ) % n + 1))) % n
Tactic: calc
    (m * n - (i + 1)) % n = (m * n - ((i / n) * n + i % n + 1)) % n := by rw [Nat.div_add_mod']
    _ = ((m - i / n - 1) * n + (n - (i % n + 1))) % n := by
      rw [Nat.mul_sub_right_distrib, Nat.one_mul, Nat.sub_add_sub_cancel _ H₁,
        Nat.mul_sub_right_distrib, Nat.sub_sub, Nat.add_assoc]
      exact Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂
    _ = n - (i % n + 1) := by
      rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt]; exact i.modNat.rev.is_lt
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n m : ℕ
i : Fin (m * n)
H₁ : (↑i : ℕ) % n + 1 ≤ n
H₂ : (↑i : ℕ) / n < m
n₁ : (m * n - ((↑i : ℕ) + 1)) % n = (m * n - ((↑i : ℕ) / n * n + (↑i : ℕ) % n + 1)) % n
n₂ : (m * n - ((↑i : ℕ) / n * n + (↑i : ℕ) % n + 1)) % n = ((m - (↑i : ℕ) / n - 1) * n + (n - ((↑i : ℕ) % n + 1))) % n
⊢ (↑i.rev.modNat : ℕ) = n - ((↑i.modNat : ℕ) + 1)
have n₃ : ((m - (↑i : ℕ) / n - 1) * n + (n - ((↑i : ℕ) % n + 1))) % n = n - ((↑i : ℕ) % n + 1)
Tactic: calc
    (m * n - (i + 1)) % n = (m * n - ((i / n) * n + i % n + 1)) % n := by rw [Nat.div_add_mod']
    _ = ((m - i / n - 1) * n + (n - (i % n + 1))) % n := by
      rw [Nat.mul_sub_right_distrib, Nat.one_mul, Nat.sub_add_sub_cancel _ H₁,
        Nat.mul_sub_right_distrib, Nat.sub_sub, Nat.add_assoc]
      exact Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂
    _ = n - (i % n + 1) := by
      rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt]; exact i.modNat.rev.is_lt
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
i : Fin n
⊢ motive i
have obtain : ∀ (i : ℕ) (hi : i < n), motive ⟨i, hi⟩
Tactic: obtain ⟨i, hi⟩ := i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
i : ℕ
hi : i < n
⊢ motive ⟨i, hi⟩
have h₁ : ∀ (j : ℕ) (hj : ∀ (m : ℕ), m < j → ∀ (hi : m < n), motive ⟨m, hi⟩) (hi : j < n), motive ⟨j, hi⟩
Tactic: induction i using Nat.strong_induction_on with
  | h j hj => exact h _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁)
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f ↔ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
have mp : ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f → ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
mp : ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f → ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
⊢ ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f ↔ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
have mpr : (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
⊢ (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f
have mpr : ∀ (H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)) (i : Fin (n + 1)) (h : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i 0),
  r (f i) (f 0)
Tactic: refine fun H i => Fin.induction (fun h ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
mpr :
  ∀ (H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)) (i : Fin (n + 1)) (h : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i 0),
    r (f i) (f 0)
⊢ (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f
have mpr₁ : ∀ (H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)) (i : Fin (n + 1)) (i_1 : Fin n),
  ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i i_1.castSucc → r (f i) (f i_1.castSucc)) →
    (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i i_1.succ → r (f i) (f i_1.succ)
Tactic: refine fun H i => Fin.induction (fun h ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (hypothesis)
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij : i < j.succ
⊢ r (f i) (f j.succ)
have hij₁ : i ≤ j.castSucc
Tactic: rw [← le_castSucc_iff] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij : i ≤ j.castSucc
⊢ r (f i) (f j.succ)
have mpr : ∀ (hij : (↑i : ℕ) = (↑j.castSucc : ℕ)), r (f i) (f j.succ)
Tactic: obtain hij | hij := (le_def.1 hij).eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij : i ≤ j.castSucc
mpr : ∀ (hij : (↑i : ℕ) = (↑j.castSucc : ℕ)), r (f i) (f j.succ)
⊢ r (f i) (f j.succ)
have mpr₁ : ∀ (hij : (↑i : ℕ) < (↑j.castSucc : ℕ)), r (f i) (f j.succ)
Tactic: obtain hij | hij := (le_def.1 hij).eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij_1 : i ≤ j.castSucc
hij : (↑i : ℕ) = (↑j.castSucc : ℕ)
⊢ r (f i) (f j.succ)
have mpr : ∀ (ihj : (fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) j.castSucc j.castSucc → r (f j.castSucc) (f j.castSucc))
  (hij : j.castSucc ≤ j.castSucc) (hij : (↑j.castSucc : ℕ) = (↑j.castSucc : ℕ)), r (f j.castSucc) (f j.succ)
Tactic: obtain rfl := Fin.ext hij
Cleared hypotheses: i, ihj, hij_1, hij
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
⊢ (↑(-1) : ℕ) = n
have zero : (↑(-1) : ℕ) = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
zero : (↑(-1) : ℕ) = 0
⊢ (↑(-1) : ℕ) = n
have succ : ∀ (n : ℕ), (↑(-1) : ℕ) = n + 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
⊢ (↑(-1) : ℕ) = n + 1
have succ : n + 1 < n + 1 + 1
Tactic: rw [Fin.val_neg', Fin.val_one, Nat.add_one_sub_one, Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ (↑(last n - i) : ℕ) = (↑i.rev : ℕ)
have rw : (↑(last n) : ℕ) - (↑i : ℕ) = (↑i.rev : ℕ)
Tactic: rw [coe_sub_iff_le.2 i.le_last, val_last, val_rev, Nat.succ_sub_succ_eq_sub]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
rw : (↑(last n) : ℕ) - (↑i : ℕ) = (↑i.rev : ℕ)
⊢ (↑(last n - i) : ℕ) = (↑i.rev : ℕ)
have rw₁ : n - (↑i : ℕ) = (↑i.rev : ℕ)
Tactic: rw [coe_sub_iff_le.2 i.le_last, val_last, val_rev, Nat.succ_sub_succ_eq_sub]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
rw : (↑(last n) : ℕ) - (↑i : ℕ) = (↑i.rev : ℕ)
rw₁ : n - (↑i : ℕ) = (↑i.rev : ℕ)
⊢ (↑(last n - i) : ℕ) = (↑i.rev : ℕ)
have rw₂ : n - (↑i : ℕ) = n + 1 - ((↑i : ℕ) + 1)
Tactic: rw [coe_sub_iff_le.2 i.le_last, val_last, val_rev, Nat.succ_sub_succ_eq_sub]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
rw : (↑(last n) : ℕ) - (↑i : ℕ) = (↑i.rev : ℕ)
rw₁ : n - (↑i : ℕ) = (↑i.rev : ℕ)
rw₂ : n - (↑i : ℕ) = n + 1 - ((↑i : ℕ) + 1)
⊢ (↑(last n - i) : ℕ) = (↑i.rev : ℕ)
have rw₃ : n - (↑i : ℕ) = n - (↑i : ℕ)
Tactic: rw [coe_sub_iff_le.2 i.le_last, val_last, val_rev, Nat.succ_sub_succ_eq_sub]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ a + 1 ≤ b
have zero : ∀ {a b : Fin (HAdd.hAdd (α := ℕ) 0 1)} (h : a < b), a + 1 ≤ b
Tactic: cases n
Cleared hypotheses: n, a, b, h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
h : a < b
zero : ∀ {a b : Fin (HAdd.hAdd (α := ℕ) 0 1)} (h : a < b), a + 1 ≤ b
⊢ a + 1 ≤ b
have succ : ∀ (n : ℕ) {a b : Fin (n + 1 + 1)} (h : a < b), a + 1 ≤ b
Tactic: cases n
Cleared hypotheses: n, a, b, h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
a b : Fin (HAdd.hAdd (α := ℕ) 0 1)
h : a < b
⊢ a + 1 ≤ b
have zero : ∀ (h : LT.lt (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)),
  (if LT.lt (α := ℤ) (↑((↑a : ℕ) + (↑1 : ℕ)) : ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) then
      HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑1 : ℕ) : ℤ)
    else HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑1 : ℕ) : ℤ) - (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) ≤
    (↑(↑b : ℕ) : ℤ)
Tactic: fin_omega
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
⊢ a + 1 ≤ b
have succ : ∀ (h : LT.lt (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)),
  (if LT.lt (α := ℤ) (↑((↑a : ℕ) + 1) : ℤ) (↑(n + 1 + 1) : ℤ) then HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑1 : ℤ)
    else HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑1 : ℤ) - (↑(n + 1 + 1) : ℤ)) ≤
    (↑(↑b : ℕ) : ℤ)
Tactic: fin_omega
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
h : a ≤ b
⊢ ∃ (k : Fin n), k ≤ b ∧ b = a + k
have obtain : ∀ (k : ℕ) (hk : (↑b : ℕ) = (↑a : ℕ) + k), ∃ (k : Fin n), k ≤ b ∧ b = a + k
Tactic: obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k := Nat.exists_eq_add_of_le h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (hypothesis)
Goal:
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k
⊢ ∃ (k : Fin n), k ≤ b ∧ b = a + k
have hkb : k ≤ (↑b : ℕ)
Tactic: have hkb : k ≤ b := by lia
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k
hkb : k ≤ (↑b : ℕ)
⊢ ∃ (k : Fin n), k ≤ b ∧ b = a + k
have refine : b = a + (⟨k, sorry⟩ : Fin n)
Tactic: refine ⟨⟨k, hkb.trans_lt b.is_lt⟩, hkb, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ ∃ (k : Fin (n + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
have zero : ∀ {a b : Fin (HAdd.hAdd (α := ℕ) 0 1)} (h : a < b),
  ∃ (k : Fin (HAdd.hAdd (α := ℕ) 0 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
Tactic: cases n
Cleared hypotheses: n, a, b, h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
h : a < b
zero :
  ∀ {a b : Fin (HAdd.hAdd (α := ℕ) 0 1)} (h : a < b),
    ∃ (k : Fin (HAdd.hAdd (α := ℕ) 0 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
⊢ ∃ (k : Fin (n + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
have succ : ∀ (n : ℕ) {a b : Fin (n + 1 + 1)} (h : a < b), ∃ (k : Fin (n + 1 + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
Tactic: cases n
Cleared hypotheses: n, a, b, h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
⊢ ∃ (k : Fin (n + 1 + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
have succ : ∀ (k : ℕ) (hk : (↑b : ℕ) = (↑a : ℕ) + k + 1), ∃ (k : Fin (n + 1 + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
Tactic: obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k + 1 := Nat.exists_eq_add_of_lt h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (hypothesis)
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k + 1
⊢ ∃ (k : Fin (n + 1 + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
have hkb : k < (↑b : ℕ)
Tactic: have hkb : k < b := by lia
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k + 1
hkb : k < (↑b : ℕ)
⊢ (⟨k, ⋯⟩ : Fin (n + 1 + 1)) + 1 ≤ b
have fin_omega : ∀ (h : LT.lt (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)),
  (if LT.lt (α := ℤ) (↑(k + 1) : ℤ) (↑(n + 1 + 1) : ℤ) then HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ)
    else HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ) - (↑(n + 1 + 1) : ℤ)) ≤
    (↑(↑b : ℕ) : ℤ)
Tactic: fin_omega
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1 + 1)
h : a < b
k : ℕ
hk : (↑b : ℕ) = (↑a : ℕ) + k + 1
hkb : k < (↑b : ℕ)
⊢ ∃ (k : Fin (n + 1 + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
have succ : b = a + (⟨k, sorry⟩ : Fin (n + 1 + 1)) + 1
Tactic: refine ⟨⟨k, hkb.trans b.is_lt⟩, hkb, by fin_omega, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin (n + 2)
h : u < v
⊢ v - (u + 1) < v - u
have fin_omega : ∀ (h : LT.lt (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)),
  (if
        (if LT.lt (α := ℤ) (↑((↑u : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ) then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ)
          else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ) - (↑(n + 2) : ℤ)) ≤
          (↑(↑v : ℕ) : ℤ) then
      (↑(↑v : ℕ) : ℤ) -
        if LT.lt (α := ℤ) (↑((↑u : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ) then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ)
        else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ) - (↑(n + 2) : ℤ)
    else
      ((↑(↑v : ℕ) : ℤ) -
          if LT.lt (α := ℤ) (↑((↑u : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ) then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ)
          else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑1 : ℤ) - (↑(n + 2) : ℤ)) +
        (↑(n + 2) : ℤ)) <
    if LE.le (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) then HSub.hSub (α := ℤ) (↑(↑v : ℕ) : ℤ) (↑(↑u : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑v : ℕ) : ℤ) (↑(↑u : ℕ) : ℤ) + (↑(n + 2) : ℤ)
Tactic: fin_omega
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n m : ℕ
inst : NeZero n
inst_1 : NeZero (R := ℕ) (OfNat.ofNat m)
⊢ NeZero (R := Fin (n + OfNat.ofNat m)) (OfNat.ofNat m)
have suffices : m % (n + m) = m
Tactic: suffices m % (n + m) = m by simpa [neZero_iff, Fin.ext_iff, OfNat.ofNat, this] using NeZero.ne m
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n m : ℕ
inst : NeZero n
inst_1 : NeZero (R := ℕ) (OfNat.ofNat m)
⊢ m % (n + m) = m
have h : m < n + m
Tactic: apply Nat.mod_eq_of_lt
-- Lean 4 proof step from Mathlib.Data.Fin.Embedding (goal)
Goal:
n m : ℕ
⊢ Nonempty (Fin n ↪ Fin m) ↔ n ≤ m
have refine : ∀ (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨castLEEmb h⟩⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Embedding (goal)
Goal:
n : ℕ
ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
m : ℕ
h : Nonempty (Fin (n + 1) ↪ Fin m)
⊢ n + 1 ≤ m
have succ : ∀ (e : Fin (n + 1) ↪ Fin m), n + 1 ≤ m
Tactic: obtain ⟨e⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Embedding (goal)
Goal:
n : ℕ
ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m
⊢ n + 1 ≤ m
have succ : ∀ (m : ℕ) (e : Fin (n + 1) ↪ Fin m.succ), n + 1 ≤ m.succ
Tactic: rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne'
      with ⟨m, rfl⟩
Cleared hypotheses: m, e
-- Lean 4 proof step from Mathlib.Data.Fin.Embedding (goal)
Goal:
n : ℕ
ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
⊢ n + 1 ≤ m.succ
have succ : Fin n ↪ Fin m
Tactic: refine Nat.succ_le_succ <| ihn ⟨?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Embedding (goal)
Goal:
n : ℕ
ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
⊢ Fin n ↪ Fin m
have succ : ∀ (i j : Fin n)
  (h :
    Eq (α := Fin m) ((fun (i : Fin n) ↦ pred ((e.setValue 0 0 : (a : Fin (n + 1)) → Fin m.succ) i.succ) sorry) i)
      ((fun (i : Fin n) ↦ pred ((e.setValue 0 0 : (a : Fin (n + 1)) → Fin m.succ) i.succ) sorry) j)),
  i = j
Tactic: refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero),
      fun i j h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Embedding (goal)
Goal:
n m : ℕ
h : Nonempty (Fin n ↪ Fin m)
⊢ n ≤ m
have zero : ∀ {m : ℕ} (h : Nonempty (Fin 0 ↪ Fin m)), 0 ≤ m
Tactic: induction n generalizing m with
  | zero => exact m.zero_le
  | succ n ihn =>
    obtain ⟨e⟩ := h
    rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne'
      with ⟨m, rfl⟩
    refine Nat.succ_le_succ <| ihn ⟨?_⟩
    refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero),
      fun i j h ↦ ?_⟩
    simpa only [pred_inj, EmbeddingLike.apply_eq_iff_eq, succ_inj] using h
Cleared hypotheses: n, m, h
-- Lean 4 proof step from Mathlib.Data.Fin.Embedding (goal)
Goal:
n m : ℕ
h : Nonempty (Fin n ↪ Fin m)
zero : ∀ {m : ℕ} (h : Nonempty (Fin 0 ↪ Fin m)), 0 ≤ m
⊢ n ≤ m
have succ : ∀ (n : ℕ) (ihn : ∀ {m : ℕ} (h : Nonempty (Fin n ↪ Fin m)), n ≤ m) {m : ℕ} (h : Nonempty (Fin (n + 1) ↪ Fin m)),
  n + 1 ≤ m
Tactic: induction n generalizing m with
  | zero => exact m.zero_le
  | succ n ihn =>
    obtain ⟨e⟩ := h
    rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne'
      with ⟨m, rfl⟩
    refine Nat.succ_le_succ <| ihn ⟨?_⟩
    refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero),
      fun i j h ↦ ?_⟩
    simpa only [pred_inj, EmbeddingLike.apply_eq_iff_eq, succ_inj] using h
Cleared hypotheses: n, m, h
-- Lean 4 proof step from Mathlib.Data.Fin.Embedding (goal)
Goal:
n m : ℕ
hmn : n ≤ m
⊢ Eq (α := Set (Fin m)) (Set.range (ι := Fin n) (⇑(natAdd_castLEEmb hmn) : (a : Fin n) → Fin m))
    {i : Fin m | m - n ≤ (↑i : ℕ)}
have simp : Eq (α := Set (Fin m))
  (Set.range (ι := Fin n) (⇑(Embedding.trans (addNatEmb (m - n)) (finCongr sorry).toEmbedding) : (a : Fin n) → Fin m))
  {i : Fin m | m ≤ (↑i : ℕ) + n}
Tactic: simp only [natAdd_castLEEmb, Nat.sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Data.Fin.Embedding (goal)
Goal:
n m : ℕ
hmn : n ≤ m
⊢ Eq (α := Set (Fin m))
    (Set.range (ι := Fin n) (⇑(Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding) : (a : Fin n) → Fin m))
    {i : Fin m | m ≤ (↑i : ℕ) + n}
have h : ∀ (y : Fin m),
  Membership.mem (γ := Set (Fin m))
      (Set.range (ι := Fin n) (⇑(Embedding.trans (addNatEmb (m - n)) (finCongr sorry).toEmbedding) : (a : Fin n) → Fin m))
      y ↔
    Membership.mem (γ := Set (Fin m)) {i : Fin m | m ≤ (↑i : ℕ) + n} y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Fin.Embedding (goal)
Goal:
n m : ℕ
hmn : n ≤ m
y : Fin m
h :
  Membership.mem (γ := Set (Fin m))
    (Set.range (ι := Fin n) (⇑(Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding) : (a : Fin n) → Fin m)) y
x : Fin n
hx : (Embedding.trans (addNatEmb (m - n)) (finCongr ⋯).toEmbedding : (a : Fin n) → Fin m) x = y
⊢ Membership.mem (γ := Set (Fin m)) {i : Fin m | m ≤ (↑i : ℕ) + n} y
have simp : m ≤ (↑x : ℕ) + (m - n) + n
Tactic: simp [← hx]
-- Lean 4 proof step from Mathlib.Data.Fin.Fin2 (goal)
Goal:
n : ℕ
⊢ Eq (α := Fin2 (n + 1)) (rev last) fz
have zero : Eq (α := Fin2 (HAdd.hAdd (α := ℕ) 0 1)) (rev last) fz
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fin.Fin2 (goal)
Goal:
n : ℕ
zero : Eq (α := Fin2 (HAdd.hAdd (α := ℕ) 0 1)) (rev last) fz
⊢ Eq (α := Fin2 (n + 1)) (rev last) fz
have succ : ∀ (n : ℕ), Eq (α := Fin2 (n + 1)) (rev last) fz → Eq (α := Fin2 (n + 1 + 1)) (rev last) fz
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fin.Fin2 (goal)
Goal:
n : ℕ
i : Fin2 n
⊢ i.castSucc.rev = i.rev.fs
have fz : ∀ {n : ℕ}, Eq (α := Fin2 (n + 1 + 1)) (rev (castSucc fz)) (fs (rev fz))
Tactic: induction i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Fin2 (goal)
Goal:
n : ℕ
i : Fin2 n
fz : ∀ {n : ℕ}, Eq (α := Fin2 (n + 1 + 1)) (rev (castSucc Fin2.fz)) (fs (rev Fin2.fz))
⊢ i.castSucc.rev = i.rev.fs
have fs : ∀ {n : ℕ} (a : Fin2 n), a.castSucc.rev = a.rev.fs → a.fs.castSucc.rev = a.fs.rev.fs
Tactic: induction i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Fin2 (goal)
Goal:
n : ℕ
i : Fin2 n
⊢ i.rev.rev = i
have fz : ∀ {n : ℕ}, Eq (α := Fin2 (n + 1)) (rev (rev fz)) fz
Tactic: induction i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Fin2 (goal)
Goal:
n : ℕ
i : Fin2 n
fz : ∀ {n : ℕ}, Eq (α := Fin2 (n + 1)) (rev (rev Fin2.fz)) Fin2.fz
⊢ i.rev.rev = i
have fs : ∀ {n : ℕ} (a : Fin2 n), a.rev.rev = a → a.fs.rev.rev = a.fs
Tactic: induction i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Fin2 (goal)
Goal:
n : ℕ
i : Fin2 n
⊢ ofFin i.toFin = i
have fz : ∀ {n : ℕ}, Eq (α := Fin2 (n + 1)) (ofFin (toFin fz)) fz
Tactic: induction i with
  | fz => rfl
  | fs _ ih => exact congrArg fs ih
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Fin2 (goal)
Goal:
n : ℕ
i : Fin2 n
fz : ∀ {n : ℕ}, Eq (α := Fin2 (n + 1)) (ofFin (toFin Fin2.fz)) Fin2.fz
⊢ ofFin i.toFin = i
have fs : ∀ {n : ℕ} (a : Fin2 n) (ih : ofFin a.toFin = a), ofFin a.fs.toFin = a.fs
Tactic: induction i with
  | fz => rfl
  | fs _ ih => exact congrArg fs ih
Cleared hypotheses: i