awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : Fin n
rw : 0 < (↑a : ℕ) ↔ (↑0 : ℕ) < (↑a : ℕ)
⊢ 0 < (↑a : ℕ) ↔ 0 < a
have rw₁ : 0 < (↑a : ℕ) ↔ 0 < (↑a : ℕ)
Tactic: rw [← val_fin_lt, val_zero]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : Fin n
⊢ 0 < a ↔ a ≠ 0
have rw : 0 < (↑a : ℕ) ↔ a ≠ 0
Tactic: rw [← val_pos_iff, Nat.pos_iff_ne_zero, val_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : Fin n
rw : 0 < (↑a : ℕ) ↔ a ≠ 0
⊢ 0 < a ↔ a ≠ 0
have rw₁ : (↑a : ℕ) ≠ 0 ↔ a ≠ 0
Tactic: rw [← val_pos_iff, Nat.pos_iff_ne_zero, val_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : Fin n
rw : 0 < (↑a : ℕ) ↔ a ≠ 0
rw₁ : (↑a : ℕ) ≠ 0 ↔ a ≠ 0
⊢ 0 < a ↔ a ≠ 0
have rw₂ : a ≠ 0 ↔ a ≠ 0
Tactic: rw [← val_pos_iff, Nat.pos_iff_ne_zero, val_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ LT.lt (α := Fin (n + 1 + 1)) 1 (last (n + 1))
have rw : n ≠ 0
Tactic: rw [lt_def, val_one, val_last, Nat.lt_add_left_iff_pos, Nat.pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
⊢ (↑(↑(u - v) : ℕ) : ℤ) =
    if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
have rw : (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, sorry⟩ : Fin n) : ℕ) : ℤ) =
  if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
  else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
Tactic: rw [Fin.sub_def]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
⊢ (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
have isTrue : v ≤ u → (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, sorry⟩ : Fin n) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
isTrue :
  v ≤ u →
    (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
⊢ (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
have isFalse : ¬v ≤ u →
  (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, sorry⟩ : Fin n) : ℕ) : ℤ) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
⊢ (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
have isTrue : HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
isTrue :
  HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
⊢ (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
have isTrue₁ : 0 ≤ HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
isTrue :
  HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
isTrue₁ : 0 ≤ HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ)
⊢ (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
have isTrue₂ : HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ) < (↑n : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
⊢ (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
have isFalse : (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
isFalse : (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
⊢ (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
have isFalse₁ : LE.le (α := ℤ) 0 (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
isFalse : (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
isFalse₁ : LE.le (α := ℤ) 0 (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ)
⊢ (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
have isFalse₂ : LT.lt (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
⊢ (↑(↑(u - v) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
have rw : (if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
  else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)) =
  HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
Tactic: rw [coe_int_sub_eq_ite]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
⊢ (if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
have isTrue : v ≤ u →
  HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
isTrue :
  v ≤ u →
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
⊢ (if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
have isFalse : ¬v ≤ u →
  HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
⊢ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
have isTrue : 0 ≤ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
Tactic: rw [Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
isTrue : 0 ≤ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
have isTrue₁ : HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) < (↑n : ℤ)
Tactic: rw [Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
⊢ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
have isFalse : 0 ≤ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
Tactic: rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
isFalse : 0 ≤ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
have isFalse₁ : HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ) < (↑n : ℤ)
Tactic: rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
⊢ (↑(↑(u + v) : ℕ) : ℤ) =
    if (↑u : ℕ) + (↑v : ℕ) < n then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
have rw : (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, sorry⟩ : Fin n) : ℕ) : ℤ) =
  if (↑u : ℕ) + (↑v : ℕ) < n then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
  else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
Tactic: rw [Fin.add_def]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
⊢ (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    if (↑u : ℕ) + (↑v : ℕ) < n then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
have isTrue : (↑u : ℕ) + (↑v : ℕ) < n →
  (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, sorry⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
isTrue :
  (↑u : ℕ) + (↑v : ℕ) < n →
    (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
⊢ (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    if (↑u : ℕ) + (↑v : ℕ) < n then HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
have isFalse : ¬(↑u : ℕ) + (↑v : ℕ) < n →
  (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, sorry⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : (↑u : ℕ) + (↑v : ℕ) < n
⊢ (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
have isTrue : (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : (↑u : ℕ) + (↑v : ℕ) < n
isTrue : (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
⊢ (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
have isTrue₁ : LE.le (α := ℤ) 0 (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : (↑u : ℕ) + (↑v : ℕ) < n
isTrue : (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
isTrue₁ : LE.le (α := ℤ) 0 (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ)
⊢ (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
have isTrue₂ : LT.lt (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : ¬(↑u : ℕ) + (↑v : ℕ) < n
⊢ (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
have isFalse : HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : ¬(↑u : ℕ) + (↑v : ℕ) < n
isFalse :
  HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
⊢ (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
have isFalse₁ : 0 ≤ HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
u v : Fin n
h : ¬(↑u : ℕ) + (↑v : ℕ) < n
isFalse :
  HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
isFalse₁ : 0 ≤ HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ)
⊢ (↑(↑(⟨((↑u : ℕ) + (↑v : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) - (↑n : ℤ)
have isFalse₂ : HSub.hSub (α := ℤ) (↑((↑u : ℕ) + (↑v : ℕ)) : ℤ) (↑n : ℤ) < (↑n : ℤ)
Tactic: rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
⊢ Nontrivial (Fin n) ↔ 2 ≤ n
have simp : 1 < n ↔ 2 ≤ n
Tactic: simp [← not_subsingleton_iff_nontrivial, subsingleton_iff_le_one]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (hypothesis)
Goal:
n : ℕ
i j : Fin n
h : 2 < n
⊢ ∃ (k : Fin n), k ≠ i ∧ k ≠ j
have this : NeZero n
Tactic: have : NeZero n := ⟨by lia⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i j : Fin n
h : 2 < n
this : NeZero n
⊢ ∃ (k : Fin n), k ≠ i ∧ k ≠ j
have rcases : ∀ (i : ℕ) (hi : i < n), ∃ (k : Fin n), k ≠ ⟨i, hi⟩ ∧ k ≠ j
Tactic: rcases i with ⟨i, hi⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
j : Fin n
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
⊢ ∃ (k : Fin n), k ≠ ⟨i, hi⟩ ∧ k ≠ j
have rcases : ∀ (j : ℕ) (hj : j < n), ∃ (k : Fin n), k ≠ ⟨i, hi⟩ ∧ k ≠ ⟨j, hj⟩
Tactic: rcases j with ⟨j, hj⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ ∃ (k : Fin n), k ≠ ⟨i, hi⟩ ∧ k ≠ ⟨j, hj⟩
have simp_rw : ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
Tactic: simp_rw [← Fin.val_ne_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
have pos : ∀ (h0 : 0 ≠ i ∧ 0 ≠ j), ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
Tactic: by_cases h0 : 0 ≠ i ∧ 0 ≠ j
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
pos : ∀ (h0 : 0 ≠ i ∧ 0 ≠ j), ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
⊢ ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
have neg : ∀ (h0 : ¬(0 ≠ i ∧ 0 ≠ j)), ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
Tactic: by_cases h0 : 0 ≠ i ∧ 0 ≠ j
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
⊢ ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
have pos : ∀ (h1 : 1 ≠ i ∧ 1 ≠ j), ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
Tactic: by_cases h1 : 1 ≠ i ∧ 1 ≠ j
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
pos : ∀ (h1 : 1 ≠ i ∧ 1 ≠ j), ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
⊢ ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
have neg : ∀ (h1 : ¬(1 ≠ i ∧ 1 ≠ j)), ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
Tactic: by_cases h1 : 1 ≠ i ∧ 1 ≠ j
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ ∃ (k : Fin n), (↑k : ℕ) ≠ i ∧ (↑k : ℕ) ≠ j
have neg : (↑(⟨2, sorry⟩ : Fin n) : ℕ) ≠ i ∧ (↑(⟨2, sorry⟩ : Fin n) : ℕ) ≠ j
Tactic: refine ⟨⟨2, by lia⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n_1 m n : ℕ
⊢ NeZero (1 + n)
have rw : NeZero (n + 1)
Tactic: rw [Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
⊢ (↑(a + b) : ℕ) = if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
have rw : ((↑a : ℕ) + (↑b : ℕ)) % n = if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
Tactic: rw [Fin.val_add, Nat.add_mod_eq_ite, Nat.mod_eq_of_lt (show ↑a < n from a.2),
    Nat.mod_eq_of_lt (show ↑b < n from b.2)]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
rw : ((↑a : ℕ) + (↑b : ℕ)) % n = if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
⊢ (↑(a + b) : ℕ) = if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
have rw₁ : (if n ≤ (↑a : ℕ) % n + (↑b : ℕ) % n then (↑a : ℕ) % n + (↑b : ℕ) % n - n else (↑a : ℕ) % n + (↑b : ℕ) % n) =
  if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
Tactic: rw [Fin.val_add, Nat.add_mod_eq_ite, Nat.mod_eq_of_lt (show ↑a < n from a.2),
    Nat.mod_eq_of_lt (show ↑b < n from b.2)]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
rw : ((↑a : ℕ) + (↑b : ℕ)) % n = if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
rw₁ :
  (if n ≤ (↑a : ℕ) % n + (↑b : ℕ) % n then (↑a : ℕ) % n + (↑b : ℕ) % n - n else (↑a : ℕ) % n + (↑b : ℕ) % n) =
    if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
⊢ (↑(a + b) : ℕ) = if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
have rw₂ : (if n ≤ (↑a : ℕ) + (↑b : ℕ) % n then (↑a : ℕ) + (↑b : ℕ) % n - n else (↑a : ℕ) + (↑b : ℕ) % n) =
  if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
Tactic: rw [Fin.val_add, Nat.add_mod_eq_ite, Nat.mod_eq_of_lt (show ↑a < n from a.2),
    Nat.mod_eq_of_lt (show ↑b < n from b.2)]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
rw : ((↑a : ℕ) + (↑b : ℕ)) % n = if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
rw₁ :
  (if n ≤ (↑a : ℕ) % n + (↑b : ℕ) % n then (↑a : ℕ) % n + (↑b : ℕ) % n - n else (↑a : ℕ) % n + (↑b : ℕ) % n) =
    if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
rw₂ :
  (if n ≤ (↑a : ℕ) + (↑b : ℕ) % n then (↑a : ℕ) + (↑b : ℕ) % n - n else (↑a : ℕ) + (↑b : ℕ) % n) =
    if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
⊢ (↑(a + b) : ℕ) = if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
have rw₃ : (if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)) =
  if n ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - n else (↑a : ℕ) + (↑b : ℕ)
Tactic: rw [Fin.val_add, Nat.add_mod_eq_ite, Nat.mod_eq_of_lt (show ↑a < n from a.2),
    Nat.mod_eq_of_lt (show ↑b < n from b.2)]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
huv : (↑a : ℕ) + (↑b : ℕ) < n
⊢ (↑(a + b) : ℕ) = (↑a : ℕ) + (↑b : ℕ)
have rw : ((↑a : ℕ) + (↑b : ℕ)) % n = (↑a : ℕ) + (↑b : ℕ)
Tactic: rw [val_add]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
⊢ (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑(if b ≤ a then 0 else n) : ℤ)
have isTrue : b ≤ a → (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑0 : ℤ)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
isTrue : b ≤ a → (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑0 : ℤ)
⊢ (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑(if b ≤ a then 0 else n) : ℤ)
have isFalse : ¬b ≤ a → (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
h : b ≤ a
⊢ (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑0 : ℤ)
have isTrue : LE.le (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ) →
  (if LE.le (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ) then HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)) =
    HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑0 : ℤ)
Tactic: fin_omega
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
a b : Fin n
h : ¬b ≤ a
⊢ (↑(↑(a - b) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)
have isFalse : ¬LE.le (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ) →
  (if LE.le (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ) then HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)) =
    HSub.hSub (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) + (↑n : ℤ)
Tactic: fin_omega
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i j : Fin n
hij : i < j
⊢ (j - i).castLT ⋯ ≠ 0
have refine : (↑0 : ℕ) ≠ (↑((j - i).castLT sorry) : ℕ)
Tactic: refine Ne.symm (ne_of_val_ne ?_)
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i j : Fin n
hij : i < j
⊢ (↑0 : ℕ) ≠ (↑((j - i).castLT ⋯) : ℕ)
have simp : ¬0 = (↑j : ℕ) - (↑i : ℕ)
Tactic: simp [coe_sub_iff_le.mpr (Fin.le_of_lt hij)]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (hypothesis)
Goal:
n : ℕ
i : Fin n
⊢ ∀ (hi : i ≠ 0), (↑(i - 1) : ℕ) = (↑i : ℕ) - 1
have this : NeZero n
Tactic: have := i.neZero
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin n
this : NeZero n
hi : i ≠ 0
⊢ (↑(i - 1) : ℕ) = (↑i : ℕ) - 1
have obtain : ∀ (n : ℕ) {i : Fin n.succ} (this : NeZero n.succ) (hi : i ≠ 0), (↑(i - 1) : ℕ) = (↑i : ℕ) - 1
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)
Cleared hypotheses: n, i, this, hi
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin n.succ
this : NeZero n.succ
hi : i ≠ 0
⊢ (↑(i - 1) : ℕ) = (↑i : ℕ) - 1
have rw : (↑i : ℕ) - (↑1 : ℕ) = (↑i : ℕ) - 1
Tactic: rw [Fin.sub_val_of_le (one_le_of_ne_zero hi), Fin.val_one', Nat.mod_eq_of_lt
    (Nat.succ_le_iff.mpr (nontrivial_iff_two_le.mp <| nontrivial_of_ne i 0 hi))]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin n.succ
this : NeZero n.succ
hi : i ≠ 0
rw : (↑i : ℕ) - (↑1 : ℕ) = (↑i : ℕ) - 1
⊢ (↑(i - 1) : ℕ) = (↑i : ℕ) - 1
have rw₁ : (↑i : ℕ) - 1 % n.succ = (↑i : ℕ) - 1
Tactic: rw [Fin.sub_val_of_le (one_le_of_ne_zero hi), Fin.val_one', Nat.mod_eq_of_lt
    (Nat.succ_le_iff.mpr (nontrivial_iff_two_le.mp <| nontrivial_of_ne i 0 hi))]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin n.succ
this : NeZero n.succ
hi : i ≠ 0
rw : (↑i : ℕ) - (↑1 : ℕ) = (↑i : ℕ) - 1
rw₁ : (↑i : ℕ) - 1 % n.succ = (↑i : ℕ) - 1
⊢ (↑(i - 1) : ℕ) = (↑i : ℕ) - 1
have rw₂ : (↑i : ℕ) - 1 = (↑i : ℕ) - 1
Tactic: rw [Fin.sub_val_of_le (one_le_of_ne_zero hi), Fin.val_one', Nat.mod_eq_of_lt
    (Nat.succ_le_iff.mpr (nontrivial_iff_two_le.mp <| nontrivial_of_ne i 0 hi))]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin n) (↑n : Fin n) 0
have h : (↑(↑n : Fin n) : ℕ) = (↑0 : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
⊢ (↑n : Fin (n + 1)) = last n
have h : (↑(↑n : Fin (n + 1)) : ℕ) = (↑(last n) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ i ≤ (↑n : Fin (n + 1))
have rw : i ≤ last n
Tactic: rw [Fin.natCast_eq_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (hypothesis)
Goal:
n a b : ℕ
han : a ≤ n
hbn : b ≤ n
⊢ LE.le (α := Fin (n + 1)) (↑a : Fin (n + 1)) (↑b : Fin (n + 1)) ↔ a ≤ b
have han₁ : a < n.succ
Tactic: rw [← Nat.lt_succ_iff] at han hbn
Cleared hypotheses: han, hbn
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (hypothesis)
Goal:
n a b : ℕ
han : a ≤ n
hbn : b ≤ n
han₁ : a < n.succ
⊢ LE.le (α := Fin (n + 1)) (↑a : Fin (n + 1)) (↑b : Fin (n + 1)) ↔ a ≤ b
have hbn₁ : b < n.succ
Tactic: rw [← Nat.lt_succ_iff] at han hbn
Cleared hypotheses: han, hbn
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (hypothesis)
Goal:
n a b : ℕ
han : a ≤ n
hbn : b ≤ n
⊢ LT.lt (α := Fin (n + 1)) (↑a : Fin (n + 1)) (↑b : Fin (n + 1)) ↔ a < b
have han₁ : a < n.succ
Tactic: rw [← Nat.lt_succ_iff] at han hbn
Cleared hypotheses: han, hbn
-- Lean 4 proof step from Mathlib.Data.Fin.Basic (hypothesis)
Goal:
n a b : ℕ
han : a ≤ n
hbn : b ≤ n
han₁ : a < n.succ
⊢ LT.lt (α := Fin (n + 1)) (↑a : Fin (n + 1)) (↑b : Fin (n + 1)) ↔ a < b
have hbn₁ : b < n.succ
Tactic: rw [← Nat.lt_succ_iff] at han hbn
Cleared hypotheses: han, hbn