awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (↑(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)
          ((castLEEmb ⋯ : (a : Fin ((↑j : ℕ) + 1)) → Fin n)
            ((finRotate ((↑j : ℕ) + 1) : (a : Fin ((↑j : ℕ) + 1)) → Fin ((↑j : ℕ) + 1))
              (((castLEEmb ⋯).toEquivRange.symm :
                  (a : { x : Fin n // x ∈ Set.range (⇑(castLEEmb ⋯) : (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 ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
                  i iin))))
          ⋯) :
      Fin n) =
    if i = j then 0 else i + 1
have pos : ∀ (ch : i = j),
  Eq (α := Fin n)
    ((↑(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) :
      Fin n)
    (0 : Fin n)
Tactic: split_ifs with ch
-- 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
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
ch : i = j
⊢ Eq (α := Fin n)
    ((↑(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)
            ((castLEEmb ⋯ : (a : Fin ((↑j : ℕ) + 1)) → Fin n)
              ((finRotate ((↑j : ℕ) + 1) : (a : Fin ((↑j : ℕ) + 1)) → Fin ((↑j : ℕ) + 1))
                (((castLEEmb ⋯).toEquivRange.symm :
                    (a : { x : Fin n // x ∈ Set.range (⇑(castLEEmb ⋯) : (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 ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
                    i iin))))
            ⋯) :
        Fin n) :
      Fin n)
    (0 : Fin n)
have this₁ : Eq (α := Fin ((↑j : ℕ) + 1))
  (((castLEEmb sorry).toEquivRange.symm :
        (a : (↑(Set.range (⇑(castLEEmb sorry) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) : Type)) → 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) :
    Fin ((↑j : ℕ) + 1))
  (last (↑j : ℕ) : Fin ((↑j : ℕ) + 1))
Tactic: have : ((castLEEmb (by lia)).toEquivRange.symm ⟨i, iin⟩) = last j := by
      simpa only [coe_castLEEmb, ← this, symm_apply_apply] using eq_of_val_eq (by simp [ch])
-- 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_1 :
  ((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
ch : i = j
this :
  Eq (α := Fin ((↑j : ℕ) + 1))
    (((castLEEmb ⋯).toEquivRange.symm :
          (a : (↑(Set.range (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) : Type)) → Fin ((↑j : ℕ) + 1))
        (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) :
      Fin ((↑j : ℕ) + 1))
    (last (↑j : ℕ) : Fin ((↑j : ℕ) + 1))
⊢ Eq (α := Fin n)
    ((↑(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)
            ((castLEEmb ⋯ : (a : Fin ((↑j : ℕ) + 1)) → Fin n)
              ((finRotate ((↑j : ℕ) + 1) : (a : Fin ((↑j : ℕ) + 1)) → Fin ((↑j : ℕ) + 1))
                (((castLEEmb ⋯).toEquivRange.symm :
                    (a : { x : Fin n // x ∈ Set.range (⇑(castLEEmb ⋯) : (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 ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
                    i iin))))
            ⋯) :
        Fin n) :
      Fin n)
    (0 : Fin n)
have pos : Eq (α := Fin n)
  (↑(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) 0) sorry) :
    Fin n)
  0
Tactic: rw [this, finRotate_last]
-- 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
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
ch : ¬i = j
⊢ (↑(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)
          ((castLEEmb ⋯ : (a : Fin ((↑j : ℕ) + 1)) → Fin n)
            ((finRotate ((↑j : ℕ) + 1) : (a : Fin ((↑j : ℕ) + 1)) → Fin ((↑j : ℕ) + 1))
              (((castLEEmb ⋯).toEquivRange.symm :
                  (a : { x : Fin n // x ∈ Set.range (⇑(castLEEmb ⋯) : (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 ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
                  i iin))))
          ⋯) :
      Fin n) =
    i + 1
have hj1 : (↑(i + 1) : ℕ) = (↑i : ℕ) + 1
Tactic: have hj1 : (i + 1).1 = i.1 + 1 := val_add_one_of_lt' (by lia)
-- 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
ch : ¬i = j
hj1 : (↑(i + 1) : ℕ) = (↑i : ℕ) + 1
⊢ (↑(i.castLT ⋯) : ℕ) + 1 < (↑j : ℕ) + 1
have simp : i < j
Tactic: simp
-- 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
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
ch : ¬i = j
hj1 : (↑(i + 1) : ℕ) = (↑i : ℕ) + 1
⊢ (↑(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)
          ((castLEEmb ⋯ : (a : Fin ((↑j : ℕ) + 1)) → Fin n)
            ((finRotate ((↑j : ℕ) + 1) : (a : Fin ((↑j : ℕ) + 1)) → Fin ((↑j : ℕ) + 1))
              (((castLEEmb ⋯).toEquivRange.symm :
                  (a : { x : Fin n // x ∈ Set.range (⇑(castLEEmb ⋯) : (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 ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
                  i iin))))
          ⋯) :
      Fin n) =
    i + 1
have hj2 : (↑(i.castLT sorry + 1) : ℕ) = (↑(i.castLT sorry) : ℕ) + 1
Tactic: have hj2 : (i.castLT (by lia) + 1 : Fin (j + 1)).1 =
      (i.castLT (by lia) : Fin (j + 1)) + 1 := val_add_one_of_lt' (by simp; lia)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≤ j
⊢ (↑((j.cycleRange : (a : Fin n) → Fin n) i) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1
have zero : ∀ {i j : Fin 0} (h : i ≤ j), (↑((j.cycleRange : (a : Fin 0) → Fin 0) i) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1
Tactic: rcases n with - | n
Cleared hypotheses: n, i, j, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≤ j
zero : ∀ {i j : Fin 0} (h : i ≤ j), (↑((j.cycleRange : (a : Fin 0) → Fin 0) i) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1
⊢ (↑((j.cycleRange : (a : Fin n) → Fin n) i) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1
have succ : ∀ (n : ℕ) {i j : Fin (n + 1)} (h : i ≤ j),
  (↑((j.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1
Tactic: rcases n with - | n
Cleared hypotheses: n, i, j, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
⊢ (↑((j.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1
have succ : (↑(if i = j then 0 else i + 1) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1
Tactic: rw [cycleRange_of_le h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
⊢ (↑(if i = j then 0 else i + 1) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1
have pos : ∀ (h' : i = j), (↑0 : ℕ) = 0
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
pos : ∀ (h' : i = j), (↑0 : ℕ) = 0
⊢ (↑(if i = j then 0 else i + 1) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1
have neg : ∀ (h' : ¬i = j), (↑(i + 1) : ℕ) = (↑i : ℕ) + 1
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i < j
⊢ (j.cycleRange : (a : Fin n) → Fin n) i = i + 1
have rw : (if i = j then 0 else i + 1) = i + 1
Tactic: rw [cycleRange_of_le h.le, if_neg h.ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i < j
rw : (if i = j then 0 else i + 1) = i + 1
⊢ (j.cycleRange : (a : Fin n) → Fin n) i = i + 1
have rw₁ : i + 1 = i + 1
Tactic: rw [cycleRange_of_le h.le, if_neg h.ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
h : i < j
⊢ (↑((j.cycleRange : (a : Fin n) → Fin n) i) : ℕ) = (↑i : ℕ) + 1
have rw : (if i = j then 0 else (↑i : ℕ) + 1) = (↑i : ℕ) + 1
Tactic: rw [coe_cycleRange_of_le h.le, if_neg h.ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
h : i < j
rw : (if i = j then 0 else (↑i : ℕ) + 1) = (↑i : ℕ) + 1
⊢ (↑((j.cycleRange : (a : Fin n) → Fin n) i) : ℕ) = (↑i : ℕ) + 1
have rw₁ : (↑i : ℕ) + 1 = (↑i : ℕ) + 1
Tactic: rw [coe_cycleRange_of_le h.le, if_neg h.ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i = j
⊢ Eq (α := Fin n) ((j.cycleRange : (a : Fin n) → Fin n) i : Fin n) (0 : Fin n)
have rw : (if i = j then 0 else i + 1) = 0
Tactic: rw [cycleRange_of_le h.le, if_pos h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i = j
rw : (if i = j then 0 else i + 1) = 0
⊢ Eq (α := Fin n) ((j.cycleRange : (a : Fin n) → Fin n) i : Fin n) (0 : Fin n)
have rw₁ : Eq (α := Fin n) 0 0
Tactic: rw [cycleRange_of_le h.le, if_pos h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
i j : Fin n
⊢ (i.cycleRange : (a : Fin n) → Fin n) j = if j < i then j + 1 else if j = i then 0 else j
have pos : ∀ (h₁ : j < i), (i.cycleRange : (a : Fin n) → Fin n) j = j + 1
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
i j : Fin n
pos : ∀ (h₁ : j < i), (i.cycleRange : (a : Fin n) → Fin n) j = j + 1
⊢ (i.cycleRange : (a : Fin n) → Fin n) j = if j < i then j + 1 else if j = i then 0 else j
have pos₁ : ∀ (h₁ : ¬j < i) (h₂ : j = i), Eq (α := Fin n) ((i.cycleRange : (a : Fin n) → Fin n) j : Fin n) (0 : Fin n)
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
i j : Fin n
pos : ∀ (h₁ : j < i), (i.cycleRange : (a : Fin n) → Fin n) j = j + 1
pos₁ : ∀ (h₁ : ¬j < i) (h₂ : j = i), Eq (α := Fin n) ((i.cycleRange : (a : Fin n) → Fin n) j : Fin n) (0 : Fin n)
⊢ (i.cycleRange : (a : Fin n) → Fin n) j = if j < i then j + 1 else if j = i then 0 else j
have neg : ∀ (h₁ : ¬j < i) (h₂ : ¬j = i), (i.cycleRange : (a : Fin n) → Fin n) j = j
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Perm (Fin n)) (cycleRange 0) 1
have H : ∀ (j : Fin n), (↑((cycleRange 0 : (a : Fin n) → Fin n) j) : ℕ) = (↑((1 : (a : Fin n) → Fin n) j) : ℕ)
Tactic: ext j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
j : Fin n
⊢ (↑((cycleRange 0 : (a : Fin n) → Fin n) j) : ℕ) = (↑((1 : (a : Fin n) → Fin n) j) : ℕ)
have H : (↑((cycleRange 0 : (a : Fin n) → Fin n) 0) : ℕ) = (↑((1 : (a : Fin n) → Fin n) 0) : ℕ)
Tactic: rcases (Fin.zero_le j).eq_or_lt with rfl | hj
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
j : Fin n
H : (↑((cycleRange 0 : (a : Fin n) → Fin n) 0) : ℕ) = (↑((1 : (a : Fin n) → Fin n) 0) : ℕ)
⊢ (↑((cycleRange 0 : (a : Fin n) → Fin n) j) : ℕ) = (↑((1 : (a : Fin n) → Fin n) j) : ℕ)
have H₁ : ∀ (hj : 0 < j), (↑((cycleRange 0 : (a : Fin n) → Fin n) j) : ℕ) = (↑((1 : (a : Fin n) → Fin n) j) : ℕ)
Tactic: rcases (Fin.zero_le j).eq_or_lt with rfl | hj
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
j : Fin n
hj : 0 < j
⊢ (↑((cycleRange 0 : (a : Fin n) → Fin n) j) : ℕ) = (↑((1 : (a : Fin n) → Fin n) j) : ℕ)
have H : (↑j : ℕ) = (↑((1 : (a : Fin n) → Fin n) j) : ℕ)
Tactic: rw [cycleRange_of_gt hj, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
inst : NeZero n
j : Fin n
hj : 0 < j
H : (↑j : ℕ) = (↑((1 : (a : Fin n) → Fin n) j) : ℕ)
⊢ (↑((cycleRange 0 : (a : Fin n) → Fin n) j) : ℕ) = (↑((1 : (a : Fin n) → Fin n) j) : ℕ)
have H₁ : (↑j : ℕ) = (↑j : ℕ)
Tactic: rw [cycleRange_of_gt hj, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
⊢ (last n).cycleRange = finRotate (n + 1)
have H : ∀ (i : Fin (n + 1)),
  (↑(((last n).cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ (↑(((last n).cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ)
have H : (if i = last n then 0 else (↑i : ℕ) + 1) = (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ)
Tactic: rw [coe_cycleRange_of_le (le_last _), coe_finRotate]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin (n + 1)
H : (if i = last n then 0 else (↑i : ℕ) + 1) = (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ)
⊢ (↑(((last n).cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ)
have H₁ : (if i = last n then 0 else (↑i : ℕ) + 1) = if i = last n then 0 else (↑i : ℕ) + 1
Tactic: rw [coe_cycleRange_of_le (le_last _), coe_finRotate]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
⊢ i.succ.succAbove ((i.cycleRange : (a : Fin n) → Fin n) j) = (swap 0 i.succ : (a : Fin (n + 1)) → Fin (n + 1)) j.succ
have zero : ∀ (i j : Fin 0),
  i.succ.succAbove ((i.cycleRange : (a : Fin 0) → Fin 0) j) = (swap 0 i.succ : (a : Fin (0 + 1)) → Fin (0 + 1)) j.succ
Tactic: cases n
Cleared hypotheses: n, i, j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
zero :
  ∀ (i j : Fin 0),
    i.succ.succAbove ((i.cycleRange : (a : Fin 0) → Fin 0) j) = (swap 0 i.succ : (a : Fin (0 + 1)) → Fin (0 + 1)) j.succ
⊢ i.succ.succAbove ((i.cycleRange : (a : Fin n) → Fin n) j) = (swap 0 i.succ : (a : Fin (n + 1)) → Fin (n + 1)) j.succ
have succ : ∀ (n : ℕ) (i j : Fin (n + 1)),
  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
Tactic: cases n
Cleared hypotheses: n, i, j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
⊢ 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 : ∀ (hlt : 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
Tactic: rcases lt_trichotomy j i with (hlt | heq | hgt)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
succ :
  ∀ (hlt : 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
⊢ 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₁ : ∀ (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
Tactic: rcases lt_trichotomy j i with (hlt | heq | hgt)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
succ :
  ∀ (hlt : 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
succ₁ :
  ∀ (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
⊢ 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₂ : ∀ (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
Tactic: rcases lt_trichotomy j i with (hlt | heq | hgt)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
⊢ (j + 1).castSucc = j.succ
have h : (↑(j + 1).castSucc : ℕ) = (↑j.succ : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
⊢ (↑(j + 1).castSucc : ℕ) = (↑j.succ : ℕ)
have h : (↑(j + 1) : ℕ) = (↑j.succ : ℕ)
Tactic: rw [val_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
h : (↑(j + 1) : ℕ) = (↑j.succ : ℕ)
⊢ (↑(j + 1).castSucc : ℕ) = (↑j.succ : ℕ)
have h₁ : (↑(j + 1) : ℕ) = (↑j : ℕ) + 1
Tactic: rw [val_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
h : (↑(j + 1) : ℕ) = (↑j.succ : ℕ)
h₁ : (↑(j + 1) : ℕ) = (↑j : ℕ) + 1
⊢ (↑(j + 1).castSucc : ℕ) = (↑j.succ : ℕ)
have h₂ : (↑j : ℕ) + 1 = (↑j : ℕ) + 1
Tactic: rw [val_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (hypothesis)
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : 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 this : (j + 1).castSucc = j.succ
Tactic: have : castSucc (j + 1) = j.succ := by
      ext
      rw [val_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
this : (j + 1).castSucc = j.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 : j.succ ≠ 0
Tactic: rw [Fin.cycleRange_of_lt hlt, Fin.succAbove_of_castSucc_lt, this, swap_apply_of_ne_of_ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
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_lt hlt, Fin.succAbove_of_castSucc_lt, this, swap_apply_of_ne_of_ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
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₂ : (j + 1).castSucc < i.succ
Tactic: rw [Fin.cycleRange_of_lt hlt, Fin.succAbove_of_castSucc_lt, this, swap_apply_of_ne_of_ne]