awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
a : ℤ
simp_rw simp_rw₁ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(↑(Fin.ofNat n (a.natMod (↑n : ℤ))) : ℕ) : ℤ) = a
simp_rw₂ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(a.natMod (↑n : ℤ) % n) : ℤ) = a
simp_rw₃ : a / (↑n : ℤ) * (↑n : ℤ) + HMod.hMod (α := ℤ) (↑(a.natMod (↑n : ℤ)) : ℤ) (↑n : ℤ) = a
simp_rw₄ : a / (↑n : ℤ) * (↑n : ℤ) + HMod.hMod (α := ℤ) (↑(a % (↑n : ℤ)).toNat : ℤ) (↑n : ℤ) = a
simp_rw₅ : a / (↑n : ℤ) * (↑n : ℤ) + a % (↑n : ℤ) % (↑n : ℤ) = a
⊢ (fun (p : ℤ × Fin n) ↦ p.1 * (↑n : ℤ) + (↑(↑p.2 : ℕ) : ℤ))
      ((fun (a : ℤ) ↦ (a / (↑n : ℤ), Fin.ofNat n (a.natMod (↑n : ℤ)))) a) =
    a
have simp_rw₆ : a / (↑n : ℤ) * (↑n : ℤ) + a % (↑n : ℤ) = a
Tactic: simp_rw [Fin.val_ofNat, natCast_mod, natMod,
      toNat_of_nonneg (emod_nonneg _ <| natCast_eq_zero.not.2 (NeZero.ne n)), emod_emod,
      ediv_mul_add_emod]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
x : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
⊢ (fun (a : ℤ) ↦ (a / (↑n : ℤ), Fin.ofNat n (a.natMod (↑n : ℤ))))
      ((fun (p : ℤ × Fin n) ↦ p.1 * (↑n : ℤ) + (↑(↑p.2 : ℕ) : ℤ)) (q, ⟨r, hrn⟩)) =
    (q, (⟨r, hrn⟩ : Fin n))
have simp : (q * (↑n : ℤ) + (↑r : ℤ)) / (↑n : ℤ) = q ∧ (↑(Fin.ofNat n ((q * (↑n : ℤ) + (↑r : ℤ)).natMod (↑n : ℤ))) : ℕ) = r
Tactic: simp only [Prod.mk_inj, Fin.ext_iff]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (hypothesis)
Goal:
m n_1 n : ℕ
inst : NeZero n
x : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
⊢ (q * (↑n : ℤ) + (↑r : ℤ)) / (↑n : ℤ) = q ∧ (↑(Fin.ofNat n ((q * (↑n : ℤ) + (↑r : ℤ)).natMod (↑n : ℤ))) : ℕ) = r
have h1 : LE.le (α := ℤ) 0 (↑r : ℤ)
Tactic: obtain ⟨h1, h2⟩ := Int.natCast_nonneg r, Int.ofNat_lt.2 hrn
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (hypothesis)
Goal:
m n_1 n : ℕ
inst : NeZero n
x : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : LE.le (α := ℤ) 0 (↑r : ℤ)
⊢ (q * (↑n : ℤ) + (↑r : ℤ)) / (↑n : ℤ) = q ∧ (↑(Fin.ofNat n ((q * (↑n : ℤ) + (↑r : ℤ)).natMod (↑n : ℤ))) : ℕ) = r
have h2 : LT.lt (α := ℤ) (↑r : ℤ) (↑n : ℤ)
Tactic: obtain ⟨h1, h2⟩ := Int.natCast_nonneg r, Int.ofNat_lt.2 hrn
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
x : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : LE.le (α := ℤ) 0 (↑r : ℤ)
h2 : LT.lt (α := ℤ) (↑r : ℤ) (↑n : ℤ)
⊢ (q * (↑n : ℤ) + (↑r : ℤ)) / (↑n : ℤ) = q ∧ (↑(Fin.ofNat n ((q * (↑n : ℤ) + (↑r : ℤ)).natMod (↑n : ℤ))) : ℕ) = r
have rw : 0 + q = q ∧ (↑(Fin.ofNat n r) : ℕ) = r
Tactic: rw [Int.add_comm, add_mul_ediv_right _ _ (natCast_eq_zero.not.2 (NeZero.ne n)),
      ediv_eq_zero_of_lt h1 h2, natMod, add_mul_emod_self_right, emod_eq_of_lt h1 h2, toNat_natCast]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n k : ℕ
h : k < n
⊢ (finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨k, ⋯⟩ = (⟨k + 1, ⋯⟩ : Fin (n + 1))
have h₁ : (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) (⟨k, sorry⟩ : Fin (n + 1))) : ℕ) =
  (↑(⟨k + 1, sorry⟩ : Fin (n + 1)) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n k : ℕ
h : k < n
⊢ (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) (⟨k, ⋯⟩ : Fin (n + 1))) : ℕ) =
    (↑(⟨k + 1, ⋯⟩ : Fin (n + 1)) : ℕ)
have h₁ : (↑((finAddFlip : (a : Fin (n + 1)) → Fin (1 + n)) (⟨k, sorry⟩ : Fin (n + 1))) : ℕ) = k + 1
Tactic: dsimp [finRotate_succ]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
⊢ Eq (α := Fin (n + 1)) (Fin.cast ⋯ ((finAddFlip : (a : Fin (n + 1)) → Fin (1 + n)) ⟨n, ⋯⟩)) 0
have rw : Fin.cast sorry (⟨n - n, sorry⟩ : Fin (1 + n)) = 0
Tactic: rw [finAddFlip_apply_mk_right le_rfl]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
⊢ Eq.{u_1 + 1} (α := (i : Fin (n + 1)) → α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a) fun (i : Fin (n + 1)) ↦
    cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)
have h : ∀ (i : ℕ) (h : i < n + 1),
  Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
Tactic: ext ⟨i, h⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
⊢ Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
have pos : ∀ (h' : i < n),
  Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
Tactic: by_cases h' : i < n
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
pos :
  ∀ (h' : i < n),
    Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
      (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
⊢ Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
have neg : ∀ (h' : ¬i < n),
  Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
Tactic: by_cases h' : i < n
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
have pos : Eq.{u_1 + 1} (α := α) (cast sorry (v ((⟨i, h⟩ : Fin (n + 1)).castLT h')) : α)
  (cases (motive := fun (x : Fin (n + 1)) ↦ α) a v (⟨i + 1, sorry⟩ : Fin (n + 1)) : α)
Tactic: rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (hypothesis)
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ n = i
have h'₁ : n ≤ i
Tactic: simp only [not_lt] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (hypothesis)
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
have h'' : n = i
Tactic: have h'' : n = i := by
      simp only [not_lt] at h'
      exact (Nat.eq_of_le_of_lt_succ h' h).symm
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
h'' : n = i
⊢ Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
have neg : ∀ (h : n < n + 1) (h' : ¬n < n),
  Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨n, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨n, h⟩) : α)
Tactic: subst h''
Cleared hypotheses: i, h, h', h''
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨n, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨n, h⟩) : α)
have neg : Eq.{u_1 + 1} (α := α) (cast sorry a : α) (cases (motive := fun (x : Fin (n + 1)) ↦ α) a v (⟨0, sorry⟩ : Fin (n + 1)) : α)
Tactic: rw [finRotate_last', Fin.snoc, Fin.cons, dif_neg (lt_irrefl _)]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 2)
⊢ (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) i = i + 1
have inl : (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) (Fin.last (n + 1)) =
  HAdd.hAdd (α := Fin (n + 2)) (Fin.last (n + 1)) 1
Tactic: obtain rfl | h := Fin.eq_or_lt_of_le i.le_last
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 2)
inl :
  (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) (Fin.last (n + 1)) =
    HAdd.hAdd (α := Fin (n + 2)) (Fin.last (n + 1)) 1
⊢ (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) i = i + 1
have inr : ∀ (h : i < Fin.last (n + 1)), (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) i = i + 1
Tactic: obtain rfl | h := Fin.eq_or_lt_of_le i.le_last
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 2)
h : i < Fin.last (n + 1)
⊢ (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) i = i + 1
have inr : ∀ (val : ℕ) (isLt : val < n + 2) (h : (⟨val, isLt⟩ : Fin (n + 2)) < Fin.last (n + 1)),
  (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) ⟨val, isLt⟩ = (⟨val, isLt⟩ : Fin (n + 2)) + 1
Tactic: cases i
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (hypothesis)
Goal:
n_1 n val : ℕ
isLt : val < n + 2
h : (⟨val, isLt⟩ : Fin (n + 2)) < Fin.last (n + 1)
⊢ (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) ⟨val, isLt⟩ = (⟨val, isLt⟩ : Fin (n + 2)) + 1
have h₁ : val < n + 1
Tactic: simp only [Fin.lt_def, Fin.val_last] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) = (↑i : ℕ) + 1
have rw : (↑(i + 1) : ℕ) = (↑i : ℕ) + 1
Tactic: rw [finRotate_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (hypothesis)
Goal:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ (↑(i + 1) : ℕ) = (↑i : ℕ) + 1
have this : (↑i : ℕ) < n
Tactic: have : (i : ℕ) < n := Fin.val_lt_last h
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
i : Fin n.succ
⊢ (↑((finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i) : ℕ) = if i = Fin.last n then 0 else (↑i : ℕ) + 1
have rw : (↑(i + 1) : ℕ) = if i = Fin.last n then 0 else (↑i : ℕ) + 1
Tactic: rw [finRotate_apply, Fin.val_add_one i]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
i : Fin n.succ
rw : (↑(i + 1) : ℕ) = if i = Fin.last n then 0 else (↑i : ℕ) + 1
⊢ (↑((finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i) : ℕ) = if i = Fin.last n then 0 else (↑i : ℕ) + 1
have rw₁ : (if i = Fin.last n then 0 else (↑i : ℕ) + 1) = if i = Fin.last n then 0 else (↑i : ℕ) + 1
Tactic: rw [finRotate_apply, Fin.val_add_one i]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin n
⊢ i < (finRotate n : (a : Fin n) → Fin n) i ↔ i ≠ -1
have obtain : ∀ (n : ℕ) [inst : NeZero n.succ] (i : Fin n.succ), i < (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i ↔ i ≠ -1
Tactic: obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
Cleared hypotheses: n, inst, i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
⊢ i < (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i ↔ i ≠ -1
have rw : i ≠ Fin.last n ↔ i ≠ -1
Tactic: rw [lt_finRotate_iff_ne_last, ne_eq, not_iff_not, ← Fin.neg_last, neg_neg]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
rw : i ≠ Fin.last n ↔ i ≠ -1
⊢ i < (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i ↔ i ≠ -1
have rw₁ : ¬i = Fin.last n ↔ i ≠ -1
Tactic: rw [lt_finRotate_iff_ne_last, ne_eq, not_iff_not, ← Fin.neg_last, neg_neg]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
rw : i ≠ Fin.last n ↔ i ≠ -1
rw₁ : ¬i = Fin.last n ↔ i ≠ -1
⊢ i < (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i ↔ i ≠ -1
have rw₂ : i = Fin.last n ↔ i = -1
Tactic: rw [lt_finRotate_iff_ne_last, ne_eq, not_iff_not, ← Fin.neg_last, neg_neg]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
rw : i ≠ Fin.last n ↔ i ≠ -1
rw₁ : ¬i = Fin.last n ↔ i ≠ -1
rw₂ : i = Fin.last n ↔ i = -1
⊢ i < (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i ↔ i ≠ -1
have rw₃ : i = Fin.last n ↔ i = - -Fin.last n
Tactic: rw [lt_finRotate_iff_ne_last, ne_eq, not_iff_not, ← Fin.neg_last, neg_neg]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
rw : i ≠ Fin.last n ↔ i ≠ -1
rw₁ : ¬i = Fin.last n ↔ i ≠ -1
rw₂ : i = Fin.last n ↔ i = -1
rw₃ : i = Fin.last n ↔ i = - -Fin.last n
⊢ i < (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i ↔ i ≠ -1
have rw₄ : i = Fin.last n ↔ i = Fin.last n
Tactic: rw [lt_finRotate_iff_ne_last, ne_eq, not_iff_not, ← Fin.neg_last, neg_neg]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
i : Fin n
⊢ (Equiv.symm (finRotate n) : (a : Fin n) → Fin n) i = i - 1
have obtain : ∀ (n : ℕ) (i : Fin n.succ), (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i = i - 1
Tactic: obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero i.pos.ne'
Cleared hypotheses: n, i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
i : Fin n.succ
⊢ (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i = i - 1
have apply : i = (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) (i - 1)
Tactic: apply (finRotate n.succ).symm_apply_eq.mpr
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
i : Fin n.succ
⊢ i = (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) (i - 1)
have rw : i = i - 1 + 1
Tactic: rw [finRotate_apply, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
i : Fin n.succ
rw : i = i - 1 + 1
⊢ i = (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) (i - 1)
have rw₁ : i = i
Tactic: rw [finRotate_apply, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin n
hi : i ≠ 0
⊢ (↑((Equiv.symm (finRotate n) : (a : Fin n) → Fin n) i) : ℕ) = (↑i : ℕ) - 1
have rwa : (↑(i - 1) : ℕ) = (↑i : ℕ) - 1
Tactic: rwa [finRotate_symm_apply, Fin.val_sub_one_of_ne_zero]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin n
hi : i ≠ 0
rwa : (↑(i - 1) : ℕ) = (↑i : ℕ) - 1
⊢ (↑((Equiv.symm (finRotate n) : (a : Fin n) → Fin n) i) : ℕ) = (↑i : ℕ) - 1
have rwa₁ : (↑i : ℕ) - 1 = (↑i : ℕ) - 1
Tactic: rwa [finRotate_symm_apply, Fin.val_sub_one_of_ne_zero]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin n
⊢ (Equiv.symm (finRotate n) : (a : Fin n) → Fin n) i < i ↔ i ≠ 0
have obtain : ∀ (n : ℕ) [inst : NeZero n.succ] (i : Fin n.succ),
  (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i < i ↔ i ≠ 0
Tactic: obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
Cleared hypotheses: n, inst, i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
⊢ (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i < i ↔ i ≠ 0
have refine : ∀ (hi : i ≠ 0), (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i < i
Tactic: refine ⟨ne_zero_of_lt, fun hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
hi : i ≠ 0
⊢ (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i < i
have rw : (↑i : ℕ) - 1 < (↑i : ℕ)
Tactic: rw [Fin.lt_def, coe_finRotate_symm_of_ne_zero hi]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (hypothesis)
Goal:
n : ℕ
k i : Fin n
⊢ (fun (i : Fin n) ↦ i - k) ((fun (i : Fin n) ↦ i + k) i) = i
have this : NeZero n
Tactic: haveI := NeZero.of_pos k.pos
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (hypothesis)
Goal:
n : ℕ
k i : Fin n
⊢ (fun (i : Fin n) ↦ i + k) ((fun (i : Fin n) ↦ i - k) i) = i
have this : NeZero n
Tactic: haveI := NeZero.of_pos k.pos
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
k : Fin (n + 1)
⊢ Eq (α := (a : Fin (n + 1)) → Fin (n + 1)) (⇑(finCycle k) : (a : Fin (n + 1)) → Fin (n + 1))
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)]
have h : ∀ (i : Fin (n + 1)),
  (↑((finCycle k : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i) : ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (hypothesis)
Goal:
n_1 n : ℕ
i : Fin (n + 1)
k : Fin n
ih :
  (↑((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.castSucc : ℕ)] i) : ℕ)
⊢ (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.succ : ℕ)] i) : ℕ)
have ih₁ : (finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i =
  (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i
Tactic: rw [Fin.val_eq_val, Fin.val_castSucc] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 1)
k : Fin n
ih :
  (finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i =
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i
⊢ (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.succ : ℕ)] i) : ℕ)
have h : (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
  (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ) + 1] i) : ℕ)
Tactic: rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 1)
k : Fin n
ih :
  (finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i =
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i
h :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ) + 1] i) : ℕ)
⊢ (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.succ : ℕ)] i) : ℕ)
have h₁ : (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
  (↑(((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1)) ∘
          (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)])
        i) :
    ℕ)
Tactic: rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 1)
k : Fin n
ih :
  (finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i =
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i
h :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ) + 1] i) : ℕ)
h₁ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑(((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1)) ∘
            (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)])
          i) :
      ℕ)
⊢ (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.succ : ℕ)] i) : ℕ)
have h₂ : (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
  (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
        ((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i)) :
    ℕ)
Tactic: rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 1)
k : Fin n
ih :
  (finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i =
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i
h :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ) + 1] i) : ℕ)
h₁ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑(((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1)) ∘
            (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)])
          i) :
      ℕ)
h₂ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
          ((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i)) :
      ℕ)
⊢ (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.succ : ℕ)] i) : ℕ)
have h₃ : (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
  (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
        ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i)) :
    ℕ)
Tactic: rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 1)
k : Fin n
ih :
  (finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i =
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i
h :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ) + 1] i) : ℕ)
h₁ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑(((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1)) ∘
            (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)])
          i) :
      ℕ)
h₂ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
          ((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i)) :
      ℕ)
h₃ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i)) :
      ℕ)
⊢ (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.succ : ℕ)] i) : ℕ)
have h₄ : (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
  (↑(HAdd.hAdd (α := Fin (n + 1)) (β := Fin (n + 1))
        ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i : Fin (n + 1)) (1 : Fin (n + 1))) :
    ℕ)
Tactic: rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]