awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
h : ¬i = Fin.last n
neg :
  (↑i : ℕ) + 1 + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
⊢ (↑i.succ : ℕ) + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
have neg₁ : (↑i : ℕ) + 1 + 1 =
  (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) (↑(Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)) : ℕ)
Tactic: rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
      if_neg h, Fin.val_zero, Fin.val_one,
      swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
h : ¬i = Fin.last n
neg :
  (↑i : ℕ) + 1 + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
neg₁ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) (↑(Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)) : ℕ)
⊢ (↑i.succ : ℕ) + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
have neg₂ : (↑i : ℕ) + 1 + 1 =
  (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) + 1)
Tactic: rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
      if_neg h, Fin.val_zero, Fin.val_one,
      swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
h : ¬i = Fin.last n
neg :
  (↑i : ℕ) + 1 + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
neg₁ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) (↑(Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)) : ℕ)
neg₂ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) + 1)
⊢ (↑i.succ : ℕ) + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
have neg₃ : (↑i : ℕ) + 1 + 1 = (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((if i = Fin.last n then 0 else (↑i : ℕ) + 1) + 1)
Tactic: rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
      if_neg h, Fin.val_zero, Fin.val_one,
      swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
h : ¬i = Fin.last n
neg :
  (↑i : ℕ) + 1 + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
neg₁ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) (↑(Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)) : ℕ)
neg₂ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) + 1)
neg₃ : (↑i : ℕ) + 1 + 1 = (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((if i = Fin.last n then 0 else (↑i : ℕ) + 1) + 1)
⊢ (↑i.succ : ℕ) + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
have neg₄ : (↑i : ℕ) + 1 + 1 = (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
Tactic: rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
      if_neg h, Fin.val_zero, Fin.val_one,
      swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
h : ¬i = Fin.last n
neg :
  (↑i : ℕ) + 1 + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
neg₁ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) (↑(Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)) : ℕ)
neg₂ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) + 1)
neg₃ : (↑i : ℕ) + 1 + 1 = (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((if i = Fin.last n then 0 else (↑i : ℕ) + 1) + 1)
neg₄ : (↑i : ℕ) + 1 + 1 = (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
⊢ (↑i.succ : ℕ) + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
have neg₅ : (↑i : ℕ) + 1 + 1 = (swap 0 (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
Tactic: rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
      if_neg h, Fin.val_zero, Fin.val_one,
      swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
h : ¬i = Fin.last n
neg :
  (↑i : ℕ) + 1 + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
neg₁ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) (↑(Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)) : ℕ)
neg₂ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) + 1)
neg₃ : (↑i : ℕ) + 1 + 1 = (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((if i = Fin.last n then 0 else (↑i : ℕ) + 1) + 1)
neg₄ : (↑i : ℕ) + 1 + 1 = (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
neg₅ : (↑i : ℕ) + 1 + 1 = (swap 0 (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
⊢ (↑i.succ : ℕ) + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
have neg₆ : (↑i : ℕ) + 1 + 1 = (swap 0 1 : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
Tactic: rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
      if_neg h, Fin.val_zero, Fin.val_one,
      swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
h : ¬i = Fin.last n
neg :
  (↑i : ℕ) + 1 + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
neg₁ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) (↑(Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)) : ℕ)
neg₂ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) + 1)
neg₃ : (↑i : ℕ) + 1 + 1 = (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((if i = Fin.last n then 0 else (↑i : ℕ) + 1) + 1)
neg₄ : (↑i : ℕ) + 1 + 1 = (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
neg₅ : (↑i : ℕ) + 1 + 1 = (swap 0 (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
neg₆ : (↑i : ℕ) + 1 + 1 = (swap 0 1 : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
⊢ (↑i.succ : ℕ) + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
have neg₇ : (↑i : ℕ) + 1 + 1 = ((↑i : ℕ) + 1).succ
Tactic: rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
      if_neg h, Fin.val_zero, Fin.val_one,
      swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
ih : (sign : (a : Perm (Fin (n + 1))) → ℤˣ) (finRotate (n + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 - 1)
⊢ (sign : (a : Perm (Fin (n + 1 + 1))) → ℤˣ) (finRotate (n + 1 + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 + 1 - 1)
have succ : (sign : (a : Perm (Fin (n + 1 + 1))) → ℤˣ)
    ((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ))
      (1, finRotate (n + 1))) =
  HPow.hPow (α := ℤˣ) (-1) (n + 1 + 1 - 1)
Tactic: rw [finRotate_succ_eq_decomposeFin]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
⊢ (sign : (a : Perm (Fin (n + 1))) → ℤˣ) (finRotate (n + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 - 1)
have succ : (sign : (a : Perm (Fin (0 + 1))) → ℤˣ) (finRotate (HAdd.hAdd (α := ℕ) 0 1)) =
  HPow.hPow (α := ℤˣ) (-1) (HAdd.hAdd (α := ℕ) 0 1 - 1)
Tactic: induction n with
    | zero => simp
    | succ n ih =>
      rw [finRotate_succ_eq_decomposeFin]
      simp [ih, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
succ :
  (sign : (a : Perm (Fin (0 + 1))) → ℤˣ) (finRotate (HAdd.hAdd (α := ℕ) 0 1)) =
    HPow.hPow (α := ℤˣ) (-1) (HAdd.hAdd (α := ℕ) 0 1 - 1)
⊢ (sign : (a : Perm (Fin (n + 1))) → ℤˣ) (finRotate (n + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 - 1)
have succ₁ : ∀ (n : ℕ) (ih : (sign : (a : Perm (Fin (n + 1))) → ℤˣ) (finRotate (n + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 - 1)),
  (sign : (a : Perm (Fin (n + 1 + 1))) → ℤˣ) (finRotate (n + 1 + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 + 1 - 1)
Tactic: induction n with
    | zero => simp
    | succ n ih =>
      rw [finRotate_succ_eq_decomposeFin]
      simp [ih, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) (finRotate n) = HPow.hPow (α := ℤˣ) (-1) (n - 1)
have zero : (sign : (a : Perm (Fin 0)) → ℤˣ) (finRotate 0) = HPow.hPow (α := ℤˣ) (-1) (HSub.hSub (α := ℕ) 0 1)
Tactic: cases n with
  | zero => simp
  | succ n =>
    induction n with
    | zero => simp
    | succ n ih =>
      rw [finRotate_succ_eq_decomposeFin]
      simp [ih, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
zero : (sign : (a : Perm (Fin 0)) → ℤˣ) (finRotate 0) = HPow.hPow (α := ℤˣ) (-1) (HSub.hSub (α := ℕ) 0 1)
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) (finRotate n) = HPow.hPow (α := ℤˣ) (-1) (n - 1)
have succ : ∀ (n : ℕ), (sign : (a : Perm (Fin (n + 1))) → ℤˣ) (finRotate (n + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 - 1)
Tactic: cases n with
  | zero => simp
  | succ n =>
    induction n with
    | zero => simp
    | succ n ih =>
      rw [finRotate_succ_eq_decomposeFin]
      simp [ih, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
⊢ Eq (α := Finset (Fin (n + 2))) (support (finRotate (n + 2))) Finset.univ
have h : ∀ (a : Fin (n + 2)),
  Membership.mem (γ := Finset (Fin (n + 2))) (support (finRotate (n + 2))) a ↔
    Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ a
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
h : 2 ≤ n
⊢ (finRotate n).support = Finset.univ
have obtain : ∀ (m : ℕ) (h : 2 ≤ 2 + m), Eq (α := Finset (Fin (2 + m))) (support (finRotate (2 + m))) Finset.univ
Tactic: obtain ⟨m, rfl⟩ := exists_add_of_le h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
m : ℕ
h : 2 ≤ 2 + m
⊢ Eq (α := Finset (Fin (2 + m))) (support (finRotate (2 + m))) Finset.univ
have rw : Eq (α := Finset (Fin (m + 2))) (support (finRotate (m + 2))) Finset.univ
Tactic: rw [add_comm, support_finRotate]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
m : ℕ
h : 2 ≤ 2 + m
rw : Eq (α := Finset (Fin (m + 2))) (support (finRotate (m + 2))) Finset.univ
⊢ Eq (α := Finset (Fin (2 + m))) (support (finRotate (2 + m))) Finset.univ
have rw₁ : Eq (α := Finset (Fin (m + 2))) Finset.univ Finset.univ
Tactic: rw [add_comm, support_finRotate]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
⊢ IsCycle (α := Fin (n + 2)) (finRotate (n + 2))
have refine : ∀ (x : Fin (n + 2)) (hx' : (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) x ≠ x),
  (HPow.hPow (α := Perm (Fin (n + 2))) (β := ℤ) (finRotate (n + 2)) (↑(↑x : ℕ) : ℤ) : (a : Fin (n + 2)) → Fin (n + 2))
      0 =
    x
Tactic: refine ⟨0, by simp, fun x hx' => ⟨x, ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
x : Fin (n + 2)
⊢ (HPow.hPow (α := Perm (Fin (n + 2))) (β := ℤ) (finRotate (n + 2)) (↑(↑x : ℕ) : ℤ) : (a : Fin (n + 2)) → Fin (n + 2))
      0 =
    x
have obtain : ∀ (x : ℕ) (hx : x < n + 2),
  (HPow.hPow (α := Perm (Fin (n + 2))) (β := ℤ) (finRotate (n + 2)) (↑(↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ) : ℤ) :
        (a : Fin (n + 2)) → Fin (n + 2))
      0 =
    (⟨x, hx⟩ : Fin (n + 2))
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n x : ℕ
hx : x < n + 2
⊢ (HPow.hPow (α := Perm (Fin (n + 2))) (β := ℤ) (finRotate (n + 2)) (↑(↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ) : ℤ) :
        (a : Fin (n + 2)) → Fin (n + 2))
      0 =
    (⟨x, hx⟩ : Fin (n + 2))
have rw : (↑((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ) :
          (a : Fin (n + 2)) → Fin (n + 2))
        0) :
    ℕ) =
  (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ)
Tactic: rw [zpow_natCast, Fin.ext_iff, Fin.val_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n x : ℕ
ih :
  ∀ (hx : x < n + 2),
    (↑((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ) :
              (a : Fin (n + 2)) → Fin (n + 2))
            0) :
        ℕ) =
      (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ)
hx : x + 1 < n + 2
⊢ (↑((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) (↑(⟨x + 1, hx⟩ : Fin (n + 2)) : ℕ) :
            (a : Fin (n + 2)) → Fin (n + 2))
          0) :
      ℕ) =
    (↑(⟨x + 1, hx⟩ : Fin (n + 2)) : ℕ)
have succ : Ne (α := Fin (n + 1).succ)
  ((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) x : (a : Fin (n + 2)) → Fin (n + 2)) 0) (Fin.last (n + 1))
Tactic: rw [pow_succ', Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n x : ℕ
ih :
  ∀ (hx : x < n + 2),
    (↑((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ) :
              (a : Fin (n + 2)) → Fin (n + 2))
            0) :
        ℕ) =
      (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ)
hx : x + 1 < n + 2
⊢ Ne (α := Fin (n + 1).succ)
    ((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) x : (a : Fin (n + 2)) → Fin (n + 2)) 0) (Fin.last (n + 1))
have succ : ¬(↑(⟨x, sorry⟩ : Fin (n + 2)) : ℕ) = n + 1
Tactic: rw [Ne, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n x : ℕ
hx : x < n + 2
⊢ (↑((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ) :
            (a : Fin (n + 2)) → Fin (n + 2))
          0) :
      ℕ) =
    (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ)
have zero : ∀ (hx : 0 < n + 2),
  (↑((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) (↑(⟨0, hx⟩ : Fin (n + 2)) : ℕ) :
            (a : Fin (n + 2)) → Fin (n + 2))
          0) :
      ℕ) =
    (↑(⟨0, hx⟩ : Fin (n + 2)) : ℕ)
Tactic: induction x with
  | zero => rfl
  | succ x ih =>
    rw [pow_succ', Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]
    rw [Ne, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]
    exact ne_of_lt (Nat.lt_of_succ_lt_succ hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n x : ℕ
hx : x < n + 2
zero :
  ∀ (hx : 0 < n + 2),
    (↑((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) (↑(⟨0, hx⟩ : Fin (n + 2)) : ℕ) :
              (a : Fin (n + 2)) → Fin (n + 2))
            0) :
        ℕ) =
      (↑(⟨0, hx⟩ : Fin (n + 2)) : ℕ)
⊢ (↑((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ) :
            (a : Fin (n + 2)) → Fin (n + 2))
          0) :
      ℕ) =
    (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ)
have succ : ∀ (x : ℕ)
  (ih :
    ∀ (hx : x < n + 2),
      (↑((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ) :
                (a : Fin (n + 2)) → Fin (n + 2))
              0) :
          ℕ) =
        (↑(⟨x, hx⟩ : Fin (n + 2)) : ℕ))
  (hx : x + 1 < n + 2),
  (↑((HPow.hPow (α := Perm (Fin (n + 2))) (finRotate (n + 2)) (↑(⟨x + 1, hx⟩ : Fin (n + 2)) : ℕ) :
            (a : Fin (n + 2)) → Fin (n + 2))
          0) :
      ℕ) =
    (↑(⟨x + 1, hx⟩ : Fin (n + 2)) : ℕ)
Tactic: induction x with
  | zero => rfl
  | succ x ih =>
    rw [pow_succ', Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]
    rw [Ne, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]
    exact ne_of_lt (Nat.lt_of_succ_lt_succ hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
h : 2 ≤ n
⊢ (finRotate n).IsCycle
have obtain : ∀ (m : ℕ) (h : 2 ≤ 2 + m), IsCycle (α := Fin (2 + m)) (finRotate (2 + m))
Tactic: obtain ⟨m, rfl⟩ := exists_add_of_le h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
m : ℕ
h : 2 ≤ 2 + m
⊢ IsCycle (α := Fin (2 + m)) (finRotate (2 + m))
have rw : IsCycle (α := Fin (m + 2)) (finRotate (m + 2))
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
⊢ cycleType (α := Fin (n + 2)) (finRotate (n + 2)) = {n + 2}
have rw : Eq (α := Multiset ℕ) {Finset.card (α := Fin (n + 2)) (support (finRotate (n + 2)))} {n + 2}
Tactic: rw [isCycle_finRotate.cycleType, support_finRotate, ← Fintype.card, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
rw : Eq (α := Multiset ℕ) {Finset.card (α := Fin (n + 2)) (support (finRotate (n + 2)))} {n + 2}
⊢ cycleType (α := Fin (n + 2)) (finRotate (n + 2)) = {n + 2}
have rw₁ : Eq (α := Multiset ℕ) {Finset.card (α := Fin (n + 2)) Finset.univ} {n + 2}
Tactic: rw [isCycle_finRotate.cycleType, support_finRotate, ← Fintype.card, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
rw : Eq (α := Multiset ℕ) {Finset.card (α := Fin (n + 2)) (support (finRotate (n + 2)))} {n + 2}
rw₁ : Eq (α := Multiset ℕ) {Finset.card (α := Fin (n + 2)) Finset.univ} {n + 2}
⊢ cycleType (α := Fin (n + 2)) (finRotate (n + 2)) = {n + 2}
have rw₂ : Eq (α := Multiset ℕ) {Fintype.card (Fin (n + 2))} {n + 2}
Tactic: rw [isCycle_finRotate.cycleType, support_finRotate, ← Fintype.card, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
rw : Eq (α := Multiset ℕ) {Finset.card (α := Fin (n + 2)) (support (finRotate (n + 2)))} {n + 2}
rw₁ : Eq (α := Multiset ℕ) {Finset.card (α := Fin (n + 2)) Finset.univ} {n + 2}
rw₂ : Eq (α := Multiset ℕ) {Fintype.card (Fin (n + 2))} {n + 2}
⊢ cycleType (α := Fin (n + 2)) (finRotate (n + 2)) = {n + 2}
have rw₃ : Eq (α := Multiset ℕ) {n + 2} {n + 2}
Tactic: rw [isCycle_finRotate.cycleType, support_finRotate, ← Fintype.card, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
h : 2 ≤ n
⊢ (finRotate n).cycleType = {n}
have obtain : ∀ (m : ℕ) (h : 2 ≤ 2 + m), cycleType (α := Fin (2 + m)) (finRotate (2 + m)) = {2 + m}
Tactic: obtain ⟨m, rfl⟩ := exists_add_of_le h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
m : ℕ
h : 2 ≤ 2 + m
⊢ cycleType (α := Fin (2 + m)) (finRotate (2 + m)) = {2 + m}
have rw : cycleType (α := Fin (m + 2)) (finRotate (m + 2)) = {m + 2}
Tactic: rw [add_comm, cycleType_finRotate]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
m : ℕ
h : 2 ≤ 2 + m
rw : cycleType (α := Fin (m + 2)) (finRotate (m + 2)) = {m + 2}
⊢ cycleType (α := Fin (2 + m)) (finRotate (2 + m)) = {2 + m}
have rw₁ : Eq (α := Multiset ℕ) {m + 2} {m + 2}
Tactic: rw [add_comm, cycleType_finRotate]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
h : i < j
⊢ (i.cycleRange : (a : Fin n) → Fin n) j = j
have h₁ : j ∉ Set.range (ι := Fin ((↑i : ℕ) + 1)) (⇑(castLEEmb sorry) : (a : Fin ((↑i : ℕ) + 1)) → Fin n)
Tactic: rw [cycleRange, Perm.extendDomain_apply_not_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (hypothesis)
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i ≤ j
⊢ (j.cycleRange : (a : Fin n) → Fin n) i = if i = j then 0 else i + 1
have iin : Membership.mem (γ := Set (Fin n))
  (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb sorry) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) i
Tactic: have iin : i ∈ Set.range (castLEEmb (n := j + 1) (by lia)) := by
    simp; lia
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (hypothesis)
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i ≤ j
iin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) i
⊢ (j.cycleRange : (a : Fin n) → Fin n) i = if i = j then 0 else i + 1
have this : ((castLEEmb sorry).toEquivRange :
      (a : Fin ((↑j : ℕ) + 1)) → (↑(Set.range (⇑(castLEEmb sorry) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) : Type))
    (i.castLT sorry) =
  Subtype.mk (p := fun (x : Fin n) ↦
    Membership.mem (γ := Set (Fin n))
      (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb sorry) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
    i iin
Tactic: have : (castLEEmb (by lia)).toEquivRange (castLT i (by lia)) = ⟨i, iin⟩ := by
    simp [coe_castLEEmb]; rfl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i ≤ j
iin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) i
this :
  ((castLEEmb ⋯).toEquivRange :
        (a : Fin ((↑j : ℕ) + 1)) → (↑(Set.range (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) : Type))
      (i.castLT ⋯) =
    Subtype.mk (p := fun (x : Fin n) ↦
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
      i iin
⊢ (j.cycleRange : (a : Fin n) → Fin n) i = if i = j then 0 else i + 1
have rw : (↑(Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb sorry) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
        ((castLEEmb sorry : (a : Fin ((↑j : ℕ) + 1)) → Fin n)
          ((finRotate ((↑j : ℕ) + 1) : (a : Fin ((↑j : ℕ) + 1)) → Fin ((↑j : ℕ) + 1))
            (((castLEEmb sorry).toEquivRange.symm :
                (a : { x : Fin n // x ∈ Set.range (⇑(castLEEmb sorry) : (a : Fin ((↑j : ℕ) + 1)) → Fin n) }) →
                  Fin ((↑j : ℕ) + 1))
              (Subtype.mk (p := fun (x : Fin n) ↦
                Membership.mem (γ := Set (Fin n))
                  (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb sorry) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
                i iin))))
        sorry) :
    Fin n) =
  if i = j then 0 else i + 1
Tactic: rw [cycleRange,
    (finRotate (j + 1)).extendDomain_apply_subtype (castLEEmb (by lia)).toEquivRange iin,
    Function.Embedding.toEquivRange_apply]