awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
heq : j = i
⊢ i.succ.succAbove ((i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j) =
    (swap 0 i.succ : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1)) j.succ
have succ : castSucc 0 < i.succ
Tactic: rw [heq, Fin.cycleRange_self, Fin.succAbove_of_castSucc_lt, swap_apply_right, Fin.castSucc_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
heq : j = i
⊢ castSucc 0 < i.succ
have succ : 0 < i.succ
Tactic: rw [Fin.castSucc_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hgt : i < j
⊢ i.succ.succAbove ((i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j) =
    (swap 0 i.succ : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1)) j.succ
have succ : j.succ ≠ 0
Tactic: rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_of_le_castSucc, swap_apply_of_ne_of_ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hgt : i < j
succ : j.succ ≠ 0
⊢ i.succ.succAbove ((i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j) =
    (swap 0 i.succ : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1)) j.succ
have succ₁ : j.succ ≠ i.succ
Tactic: rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_of_le_castSucc, swap_apply_of_ne_of_ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hgt : i < j
succ : j.succ ≠ 0
succ₁ : j.succ ≠ i.succ
⊢ i.succ.succAbove ((i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j) =
    (swap 0 i.succ : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1)) j.succ
have succ₂ : i.succ ≤ j.castSucc
Tactic: rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_of_le_castSucc, swap_apply_of_ne_of_ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ
have inl : ∀ (h : j.castSucc < i), (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ
Tactic: rcases lt_or_ge (castSucc j) i with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
inl : ∀ (h : j.castSucc < i), (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ
⊢ (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ
have inr : ∀ (h : i ≤ j.castSucc), (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ
Tactic: rcases lt_or_ge (castSucc j) i with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ
have inl : (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j.castSucc = j.succ
Tactic: rw [Fin.succAbove_of_castSucc_lt _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
inl : (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j.castSucc = j.succ
⊢ (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ
have inl₁ : j.castSucc + 1 = j.succ
Tactic: rw [Fin.succAbove_of_castSucc_lt _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
inl : (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j.castSucc = j.succ
inl₁ : j.castSucc + 1 = j.succ
⊢ (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ
have inl₂ : j.succ = j.succ
Tactic: rw [Fin.succAbove_of_castSucc_lt _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ
have inr : (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j.succ = j.succ
Tactic: rw [Fin.succAbove_of_le_castSucc _ _ h, Fin.cycleRange_of_gt (Fin.le_castSucc_iff.mp h)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
inr : (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j.succ = j.succ
⊢ (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ
have inr₁ : j.succ = j.succ
Tactic: rw [Fin.succAbove_of_le_castSucc _ _ h, Fin.cycleRange_of_gt (Fin.le_castSucc_iff.mp h)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
j : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := α)
    (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x ((Equiv.symm p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j) :
      α)
    (cons (α := fun (a : Fin (n + 1)) ↦ α) a x j : α)
have zero : Eq.{u_1 + 1} (α := α)
  (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x ((Equiv.symm p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) 0) : α)
  (cons (α := fun (a : Fin (n + 1)) ↦ α) a x 0)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
j : Fin (n + 1)
zero :
  Eq.{u_1 + 1} (α := α)
    (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x ((Equiv.symm p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) 0) :
      α)
    (cons (α := fun (a : Fin (n + 1)) ↦ α) a x 0)
⊢ Eq.{u_1 + 1} (α := α)
    (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x ((Equiv.symm p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j) :
      α)
    (cons (α := fun (a : Fin (n + 1)) ↦ α) a x j : α)
have succ : ∀ (i : Fin n),
  Eq.{u_1 + 1} (α := α)
    (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x
        ((Equiv.symm p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) i.succ) :
      α)
    (cons (α := fun (a : Fin (n + 1)) ↦ α) a x i.succ : α)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
⊢ Eq.{u_1 + 1} (α := Fin (n + 1) → α)
    (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x ∘ (⇑(Equiv.symm p.cycleRange) : (a : Fin (n + 1)) → Fin (n + 1)))
    (cons (α := fun (i : Fin (n + 1)) ↦ α) a x)
have h : ∀ (j : Fin (n + 1)),
  Eq.{u_1 + 1} (α := α)
    ((p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x ∘ (⇑(Equiv.symm p.cycleRange) : (a : Fin (n + 1)) → Fin (n + 1)))
        j :
      α)
    (cons (α := fun (i : Fin (n + 1)) ↦ α) a x j : α)
Tactic: ext j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
α : Type u_1
a : α
x : Fin n → α
p j : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := α)
    (cons (α := fun (a : Fin (n + 1)) ↦ α) a x ((p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j) : α)
    (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x j : α)
have rw : Eq.{u_1 + 1} (α := α)
  (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x
      ((Equiv.symm p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1))
        ((p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j)) :
    α)
  (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x j : α)
Tactic: rw [← insertNth_apply_cycleRange_symm, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
α : Type u_1
a : α
x : Fin n → α
p j : Fin (n + 1)
rw :
  Eq.{u_1 + 1} (α := α)
    (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x
        ((Equiv.symm p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1))
          ((p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j)) :
      α)
    (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x j : α)
p₁ : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := α)
    (cons (α := fun (a : Fin (n + 1)) ↦ α) a x ((p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j) : α)
    (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x j : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x j : α)
  (p.insertNth (α := fun (a : Fin (n + 1)) ↦ α) a x j)
Tactic: rw [← insertNth_apply_cycleRange_symm, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
α : Type u_1
a : α
x : Fin n → α
p : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := Fin (n + 1) → α)
    (Function.comp (β := Fin (n + 1)) (cons (α := fun (a : Fin (n + 1)) ↦ α) a x)
      (⇑p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)))
    (p.insertNth (α := fun (j : Fin (n + 1)) ↦ α) a x)
have h : ∀ (x_1 : Fin (n + 1)),
  Eq.{u_1 + 1} (α := α)
    (Function.comp (β := Fin (n + 1)) (cons (α := fun (a : Fin (n + 1)) ↦ α) a x)
        (⇑p.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) x_1 :
      α)
    (p.insertNth (α := fun (j : Fin (n + 1)) ↦ α) a x x_1 : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
inst : NeZero n
h0 : i ≠ 0
⊢ i.cycleRange.IsCycle
have obtain : ∀ (i : ℕ) (hi : i < n) (h0 : (⟨i, hi⟩ : Fin n) ≠ 0), (⟨i, hi⟩ : Fin n).cycleRange.IsCycle
Tactic: obtain ⟨i, hi⟩ := i
Cleared hypotheses: i, h0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
i : ℕ
hi : i < n
h0 : (⟨i, hi⟩ : Fin n) ≠ 0
⊢ (⟨i, hi⟩ : Fin n).cycleRange.IsCycle
have zero : ∀ (hi : 0 < n) (h0 : (⟨0, hi⟩ : Fin n) ≠ 0), (⟨0, hi⟩ : Fin n).cycleRange.IsCycle
Tactic: cases i
Cleared hypotheses: i, hi, h0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
i : ℕ
hi : i < n
h0 : (⟨i, hi⟩ : Fin n) ≠ 0
zero : ∀ (hi : 0 < n) (h0 : (⟨0, hi⟩ : Fin n) ≠ 0), (⟨0, hi⟩ : Fin n).cycleRange.IsCycle
⊢ (⟨i, hi⟩ : Fin n).cycleRange.IsCycle
have succ : ∀ (n_1 : ℕ) (hi : n_1 + 1 < n) (h0 : (⟨n_1 + 1, hi⟩ : Fin n) ≠ 0), (⟨n_1 + 1, hi⟩ : Fin n).cycleRange.IsCycle
Tactic: cases i
Cleared hypotheses: i, hi, h0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
inst : NeZero n
h0 : i ≠ 0
⊢ i.cycleRange.cycleType = {(↑i : ℕ) + 1}
have obtain : ∀ (i : ℕ) (hi : i < n) (h0 : (⟨i, hi⟩ : Fin n) ≠ 0),
  (⟨i, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨i, hi⟩ : Fin n) : ℕ) + 1}
Tactic: obtain ⟨i, hi⟩ := i
Cleared hypotheses: i, h0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
i : ℕ
hi : i < n
h0 : (⟨i, hi⟩ : Fin n) ≠ 0
⊢ (⟨i, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨i, hi⟩ : Fin n) : ℕ) + 1}
have zero : ∀ (hi : 0 < n) (h0 : (⟨0, hi⟩ : Fin n) ≠ 0), (⟨0, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨0, hi⟩ : Fin n) : ℕ) + 1}
Tactic: cases i
Cleared hypotheses: i, hi, h0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
i : ℕ
hi : i < n
h0 : (⟨i, hi⟩ : Fin n) ≠ 0
zero :
  ∀ (hi : 0 < n) (h0 : (⟨0, hi⟩ : Fin n) ≠ 0), (⟨0, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨0, hi⟩ : Fin n) : ℕ) + 1}
⊢ (⟨i, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨i, hi⟩ : Fin n) : ℕ) + 1}
have succ : ∀ (n_1 : ℕ) (hi : n_1 + 1 < n) (h0 : (⟨n_1 + 1, hi⟩ : Fin n) ≠ 0),
  (⟨n_1 + 1, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨n_1 + 1, hi⟩ : Fin n) : ℕ) + 1}
Tactic: cases i
Cleared hypotheses: i, hi, h0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
⊢ IsThreeCycle (α := Fin (n + 3)) (cycleRange 2)
have rw : Eq (α := Multiset ℕ) {(↑2 : ℕ) + 1} {3}
Tactic: rw [IsThreeCycle, cycleType_cycleRange two_ne_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : k < i
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k
have pos : ∀ (hij : i ≤ j), (i.cycleIcc j : (a : Fin n) → Fin n) k = k
Tactic: by_cases hij : i ≤ j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : k < i
pos : ∀ (hij : i ≤ j), (i.cycleIcc j : (a : Fin n) → Fin n) k = k
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k
have neg : ∀ (hij : ¬i ≤ j), (i.cycleIcc j : (a : Fin n) → Fin n) k = k
Tactic: by_cases hij : i ≤ j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : k < i
hij : i ≤ j
⊢ k ∉ Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)
have simp : (↑k : ℕ) + (n - (↑i : ℕ)) < n
Tactic: simp [range_natAdd_castLEEmb]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : j < k
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k
have pos : ∀ (hij : i ≤ j), (i.cycleIcc j : (a : Fin n) → Fin n) k = k
Tactic: by_cases hij : i ≤ j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : j < k
pos : ∀ (hij : i ≤ j), (i.cycleIcc j : (a : Fin n) → Fin n) k = k
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k
have neg : ∀ (hij : ¬i ≤ j), (i.cycleIcc j : (a : Fin n) → Fin n) k = k
Tactic: by_cases hij : i ≤ j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
have simp : n ≤ (↑k : ℕ) + (n - (↑i : ℕ))
Tactic: simp [range_natAdd_castLEEmb]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (hypothesis)
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k
have kin : Membership.mem (γ := Set (Fin n))
  (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb sorry) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
Tactic: have kin : k ∈ Set.range (natAdd_castLEEmb (Nat.sub_le n i)) := by
      simp [range_natAdd_castLEEmb]; lia
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
⊢ (↑i : ℕ) ≤ (↑(Fin.cast ⋯ k) : ℕ)
have simp : i ≤ k
Tactic: simp
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
⊢ (↑k : ℕ) = (↑(Fin.cast ⋯ ((subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯).addNat (n - (n - (↑i : ℕ))))) : ℕ)
have simp : (↑k : ℕ) = (↑k : ℕ) - (↑i : ℕ) + (n - (n - (↑i : ℕ)))
Tactic: simp
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (hypothesis)
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k
have this : (Equiv.symm
        (Function.Embedding.toEquivRange
          (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr sorry)))) :
      (a :
          (↑(Set.range
                (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr sorry).toEmbedding) :
                  (a : Fin (n - (↑i : ℕ))) → Fin n)) :
            Type)) →
        Fin (n - (↑i : ℕ)))
    (Subtype.mk (p := fun (x : Fin n) ↦
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (n - (↑i : ℕ)))
          (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr sorry))) :
            (a : Fin (n - (↑i : ℕ))) → Fin n))
        x)
      k kin) =
  subNat (↑i : ℕ) (Fin.cast sorry k) sorry
Tactic: have : (((addNatEmb (n - (n - i.1))).trans (finCongr _).toEmbedding).toEquivRange.symm ⟨k, kin⟩)
      = subNat i.1 (k.cast (by lia)) (by simp; lia) := by
      simpa [symm_apply_eq] using eq_of_val_eq (by simp; lia)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k
have pos : Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) sorry
    (addNat
      ((((j - i).castLT sorry).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
        (subNat (↑i : ℕ) (Fin.cast sorry k) sorry))
      (n - (n - (↑i : ℕ)))) =
  k
Tactic: simp only [cycleIcc_to_cycleRange hij kin, natAdd_castLEEmb, this,
      Function.Embedding.trans_apply, addNatEmb_apply, coe_toEmbedding, finCongr_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) ⋯
      (addNat
        ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
          (subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯))
        (n - (n - (↑i : ℕ)))) =
    k
have pos : Fin.cast sorry ((subNat (↑i : ℕ) (Fin.cast sorry k) sorry).addNat (n - (n - (↑i : ℕ)))) = k
Tactic: rw [cycleRange_of_gt]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
pos : Fin.cast ⋯ ((subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯).addNat (n - (n - (↑i : ℕ)))) = k
⊢ Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) ⋯
      (addNat
        ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
          (subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯))
        (n - (n - (↑i : ℕ)))) =
    k
have pos₁ : (j - i).castLT sorry < subNat (↑i : ℕ) (Fin.cast sorry k) sorry
Tactic: rw [cycleRange_of_gt]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ (↑(Fin.cast ⋯ ((subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯).addNat (n - (n - (↑i : ℕ))))) : ℕ) = (↑k : ℕ)
have simp : (↑k : ℕ) - (↑i : ℕ) + (n - (n - (↑i : ℕ))) = (↑k : ℕ)
Tactic: simp
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ (↑((j - i).castLT ⋯) : ℕ) < (↑(subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯) : ℕ)
have simp : (↑j : ℕ) - (↑i : ℕ) < (↑k : ℕ) - (↑i : ℕ)
Tactic: simp [sub_val_of_le hij]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (hypothesis)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = if k = j then i else k + 1
have hij : i ≤ j
Tactic: have hij : i ≤ j := le_trans hik hkj
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
have simp : n ≤ (↑k : ℕ) + (n - (↑i : ℕ))
Tactic: simp [range_natAdd_castLEEmb]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (hypothesis)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = if k = j then i else k + 1
have kin : Membership.mem (γ := Set (Fin n))
  (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb sorry) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
Tactic: have kin : k ∈ Set.range (natAdd_castLEEmb (Nat.sub_le n i)) := by
    simp [range_natAdd_castLEEmb]; lia
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
⊢ (↑k : ℕ) = (↑(Fin.cast ⋯ ((subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯).addNat (n - (n - (↑i : ℕ))))) : ℕ)
have simp : (↑k : ℕ) = (↑k : ℕ) - (↑i : ℕ) + (n - (n - (↑i : ℕ)))
Tactic: simp