awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Fin
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) : ℕ) = (↑(i.castLT ⋯) : ℕ) + 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)
-- Module: Mathlib.GroupTheory.Perm.Fin
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
hj2 : (↑(i.castLT ⋯ + 1) : ℕ) = (↑(i.castLT ⋯) : ℕ) + 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) : ℕ)

Tactic:
simp [← this, hj1, hj2]
-- Module: Mathlib.GroupTheory.Perm.Fin
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
hj2 : (↑(i.castLT ⋯ + 1) : ℕ) = (↑(i.castLT ⋯) : ℕ) + 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

Tactic:
exact eq_of_val_eq (by simp [← this, hj1, hj2])

Premises used: Fin.eq_of_val_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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
⊢ (↑((j.cycleRange : (a : Fin n) → Fin n) i) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1

Tactic:
rcases n with - | n
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
i j : Fin 0
h : i ≤ j
⊢ (↑((j.cycleRange : (a : Fin 0) → Fin 0) i) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1

Tactic:
absurd le_rfl j.pos.not_ge

Premises used: le_rfl, Fin.pos, absurd, LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
i j : Fin 0
h : i ≤ j
⊢ (↑((j.cycleRange : (a : Fin 0) → Fin 0) i) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1

Tactic:
exact absurd le_rfl j.pos.not_ge

Premises used: le_rfl, Fin.pos, absurd, LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
succ : (↑(if i = j then 0 else i + 1) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1
⊢ (↑((j.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1

Tactic:
rw [cycleRange_of_le h]

Premises used: Fin.cycleRange_of_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
pos : ∀ (h' : i = j), (↑0 : ℕ) = 0
neg : ∀ (h' : ¬i = j), (↑(i + 1) : ℕ) = (↑i : ℕ) + 1
⊢ (↑(if i = j then 0 else i + 1) : ℕ) = if i = j then 0 else (↑i : ℕ) + 1

Tactic:
split_ifs with h'
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
h' : i = j
⊢ (↑0 : ℕ) = 0

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
h' : ¬i = j
⊢ (↑(i + 1) : ℕ) = (↑i : ℕ) + 1

Tactic:
val_add_one_of_lt
      (calc
        (i : ℕ) < j := Fin.lt_def.mp (lt_of_le_of_ne h h')
        _ ≤ n := Nat.lt_succ_iff.mp j.2)

Premises used: Trans.trans, Fin.isLt, Fin.lt_def, Nat.lt_succ_iff, Fin.val_add_one_of_lt, Iff.mp, lt_of_le_of_ne
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
h' : ¬i = j
⊢ (↑(i + 1) : ℕ) = (↑i : ℕ) + 1

Tactic:
exact
    val_add_one_of_lt
      (calc
        (i : ℕ) < j := Fin.lt_def.mp (lt_of_le_of_ne h h')
        _ ≤ n := Nat.lt_succ_iff.mp j.2)

Premises used: Trans.trans, Fin.isLt, Fin.lt_def, Nat.lt_succ_iff, Fin.val_add_one_of_lt, Iff.mp, lt_of_le_of_ne
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i < j
rw : (if i = j then 0 else i + 1) = i + 1
rw₁ rw₂ : i + 1 = i + 1
⊢ (j.cycleRange : (a : Fin n) → Fin n) i = i + 1

Tactic:
rw [cycleRange_of_le h.le, if_neg h.ne]

Premises used: LT.lt.le, Fin.cycleRange_of_le, if_neg, LT.lt.ne
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
h : i < j
rw : (if i = j then 0 else (↑i : ℕ) + 1) = (↑i : ℕ) + 1
rw₁ rw₂ : (↑i : ℕ) + 1 = (↑i : ℕ) + 1
⊢ (↑((j.cycleRange : (a : Fin n) → Fin n) i) : ℕ) = (↑i : ℕ) + 1

Tactic:
rw [coe_cycleRange_of_le h.le, if_neg h.ne]

Premises used: Fin.coe_cycleRange_of_le, LT.lt.le, if_neg, LT.lt.ne
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i = j
rw : (if i = j then 0 else i + 1) = 0
rw₁ rw₂ : Eq (α := Fin n) 0 0
⊢ Eq (α := Fin n) ((j.cycleRange : (a : Fin n) → Fin n) i : Fin n) (0 : Fin n)

Tactic:
rw [cycleRange_of_le h.le, if_pos h]

Premises used: Eq.le, Fin.cycleRange_of_le, if_pos
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
i : Fin n
⊢ Eq (α := Fin n) ((i.cycleRange : (a : Fin n) → Fin n) i : Fin n) (0 : Fin n)

Tactic:
cycleRange_of_eq rfl

Premises used: Fin.cycleRange_of_eq, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
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)
neg : ∀ (h₁ : ¬j < i) (h₂ : ¬j = i), (i.cycleRange : (a : Fin n) → Fin n) j = j
⊢ (i.cycleRange : (a : Fin n) → Fin n) j = if j < i then j + 1 else if j = i then 0 else j

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
i j : Fin n
h₁ : j < i
⊢ (i.cycleRange : (a : Fin n) → Fin n) j = j + 1

Tactic:
cycleRange_of_lt h₁

Premises used: Fin.cycleRange_of_lt
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
i j : Fin n
h₁ : j < i
⊢ (i.cycleRange : (a : Fin n) → Fin n) j = j + 1

Tactic:
exact cycleRange_of_lt h₁

Premises used: Fin.cycleRange_of_lt
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
i j : Fin n
h₁ : ¬j < i
h₂ : j = i
⊢ Eq (α := Fin n) ((i.cycleRange : (a : Fin n) → Fin n) j : Fin n) (0 : Fin n)

Tactic:
cycleRange_of_eq h₂

Premises used: Fin.cycleRange_of_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
i j : Fin n
h₁ : ¬j < i
h₂ : j = i
⊢ Eq (α := Fin n) ((i.cycleRange : (a : Fin n) → Fin n) j : Fin n) (0 : Fin n)

Tactic:
exact cycleRange_of_eq h₂

Premises used: Fin.cycleRange_of_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
i j : Fin n
h₁ : ¬j < i
h₂ : ¬j = i
⊢ (i.cycleRange : (a : Fin n) → Fin n) j = j

Tactic:
cycleRange_of_gt (lt_of_le_of_ne (le_of_not_gt h₁) (Ne.symm h₂))

Premises used: le_of_not_gt, Ne.symm, Fin.cycleRange_of_gt, lt_of_le_of_ne
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
i j : Fin n
h₁ : ¬j < i
h₂ : ¬j = i
⊢ (i.cycleRange : (a : Fin n) → Fin n) j = j

Tactic:
exact cycleRange_of_gt (lt_of_le_of_ne (le_of_not_gt h₁) (Ne.symm h₂))

Premises used: le_of_not_gt, Ne.symm, Fin.cycleRange_of_gt, lt_of_le_of_ne
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
H : ∀ (j : Fin n), (↑((cycleRange 0 : (a : Fin n) → Fin n) j) : ℕ) = (↑((1 : (a : Fin n) → Fin n) j) : ℕ)
⊢ Eq (α := Perm (Fin n)) (cycleRange 0) 1

Tactic:
ext j
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
j : Fin n
H : (↑((cycleRange 0 : (a : Fin n) → Fin n) 0) : ℕ) = (↑((1 : (a : Fin n) → Fin n) 0) : ℕ)
H₁ : ∀ (hj : 0 < j), (↑((cycleRange 0 : (a : Fin n) → Fin n) j) : ℕ) = (↑((1 : (a : Fin n) → Fin n) 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

Premises used: LE.le.eq_or_lt, Fin.zero_le, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
⊢ (↑((cycleRange 0 : (a : Fin n) → Fin n) 0) : ℕ) = (↑((1 : (a : Fin n) → Fin n) 0) : ℕ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
j : Fin n
hj : 0 < j
H : (↑j : ℕ) = (↑((1 : (a : Fin n) → Fin n) j) : ℕ)
H₁ H₂ : (↑j : ℕ) = (↑j : ℕ)
⊢ (↑((cycleRange 0 : (a : Fin n) → Fin n) j) : ℕ) = (↑((1 : (a : Fin n) → Fin n) j) : ℕ)

Tactic:
rw [cycleRange_of_gt hj, one_apply]

Premises used: Equiv.Perm.one_apply, Fin.cycleRange_of_gt
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
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) : ℕ)
⊢ (last n).cycleRange = finRotate (n + 1)

Tactic:
ext i
-- Module: Mathlib.GroupTheory.Perm.Fin
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) : ℕ)
H₁ H₂ : (if i = last n then 0 else (↑i : ℕ) + 1) = if i = last n then 0 else (↑i : ℕ) + 1
⊢ (↑(((last n).cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ)

Tactic:
rw [coe_cycleRange_of_le (le_last _), coe_finRotate]

Premises used: Fin.coe_cycleRange_of_le, coe_finRotate, Fin.le_last
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
h : 0 < n
⊢ (⟨0, h⟩ : Fin n).cycleRange = 1

Tactic:
have : NeZero n := .of_pos h
  cycleRange_zero n

Premises used: Fin.cycleRange_zero, Fin.ofNat, NeZero.of_pos, Nat.mod
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) i.cycleRange = HPow.hPow (α := ℤˣ) (-1) (↑i : ℕ)

Tactic:
simp [cycleRange]

Premises used: Fin.cycleRange
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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
⊢ i.succ.succAbove ((i.cycleRange : (a : Fin n) → Fin n) j) = (swap 0 i.succ : (a : Fin (n + 1)) → Fin (n + 1)) j.succ

Tactic:
cases n
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
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:
rcases j with ⟨_, ⟨⟩⟩
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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
⊢ 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)

Premises used: lt_trichotomy
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
h : (↑(j + 1).castSucc : ℕ) = (↑j.succ : ℕ)
⊢ (j + 1).castSucc = j.succ

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
h : (↑(j + 1) : ℕ) = (↑j.succ : ℕ)
h₁ : (↑(j + 1) : ℕ) = (↑j : ℕ) + 1
h₂ h₃ : (↑j : ℕ) + 1 = (↑j : ℕ) + 1
⊢ (↑(j + 1).castSucc : ℕ) = (↑j.succ : ℕ)

Tactic:
rw [val_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]

Premises used: Fin.val_succ, Fin.val_add_one_of_lt, Fin.val_castSucc, lt_of_lt_of_le, Fin.le_last
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
⊢ (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)]
-- Module: Mathlib.GroupTheory.Perm.Fin
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
succ₂ : (j + 1).castSucc < 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

Tactic:
rw [Fin.cycleRange_of_lt hlt, Fin.succAbove_of_castSucc_lt, this, swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne, Fin.cycleRange_of_lt, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ ≠ 0

Tactic:
apply Fin.succ_ne_zero

Premises used: Fin.succ_ne_zero
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ ≠ i.succ

Tactic:
(Fin.succ_injective _).ne hlt.ne

Premises used: Function.Injective.ne, Fin.succ_injective, LT.lt.ne
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ ≠ i.succ

Tactic:
exact (Fin.succ_injective _).ne hlt.ne

Premises used: Function.Injective.ne, Fin.succ_injective, LT.lt.ne
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ (↑(j + 1).castSucc : ℕ) < (↑i.succ : ℕ)

Tactic:
simpa [this] using hlt
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
heq : j = i
succ : castSucc 0 < 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

Tactic:
rw [heq, Fin.cycleRange_self, Fin.succAbove_of_castSucc_lt, swap_apply_right, Fin.castSucc_zero]

Premises used: Fin.castSucc_zero, Fin.succAbove_of_castSucc_lt, Equiv.swap_apply_right, Fin.cycleRange_self
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
heq : j = i
succ : 0 < i.succ
⊢ castSucc 0 < i.succ

Tactic:
rw [Fin.castSucc_zero]

Premises used: Fin.castSucc_zero
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
heq : j = i
⊢ 0 < i.succ

Tactic:
apply Fin.succ_pos

Premises used: Fin.succ_pos
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hgt : i < j
succ : j.succ ≠ 0
succ₁ : j.succ ≠ i.succ
succ₂ : i.succ ≤ j.castSucc
⊢ 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:
rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_of_le_castSucc, swap_apply_of_ne_of_ne]

Premises used: Fin.succAbove_of_le_castSucc, Equiv.swap_apply_of_ne_of_ne, Fin.cycleRange_of_gt
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hgt : i < j
⊢ j.succ ≠ 0

Tactic:
apply Fin.succ_ne_zero

Premises used: Fin.succ_ne_zero
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hgt : i < j
⊢ j.succ ≠ i.succ

Tactic:
apply (Fin.succ_injective _).ne hgt.ne.symm

Premises used: Function.Injective.ne, Fin.succ_injective, Ne.symm, LT.lt.ne
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hgt : i < j
⊢ i.succ ≤ j.castSucc

Tactic:
simpa [Fin.le_iff_val_le_val] using hgt

Premises used: Fin.le_iff_val_le_val
-- Module: Mathlib.GroupTheory.Perm.Fin
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
inr : ∀ (h : i ≤ j.castSucc), (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

Tactic:
rcases lt_or_ge (castSucc j) i with h | h

Premises used: lt_or_ge, Fin.castSucc
-- Module: Mathlib.GroupTheory.Perm.Fin
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
inl₂ inl₃ : j.succ = j.succ
⊢ (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]

Premises used: Fin.cycleRange_of_lt, Fin.coeSucc_eq_succ, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.GroupTheory.Perm.Fin
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
inr₁ inr₂ : j.succ = j.succ
⊢ (i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) = j.succ

Tactic:
rw [Fin.succAbove_of_le_castSucc _ _ h, Fin.cycleRange_of_gt (Fin.le_castSucc_iff.mp h)]

Premises used: Fin.succAbove_of_le_castSucc, Iff.mp, Fin.le_castSucc_iff, Fin.cycleRange_of_gt
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
i : Fin n
⊢ Eq (α := Fin n) ((i.cycleRange : (a : Fin n) → Fin n) ((Equiv.symm i.cycleRange : (a : Fin n) → Fin n) 0) : Fin n)
    ((i.cycleRange : (a : Fin n) → Fin n) i : Fin n)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ Eq (α := Fin (n + 1))
    ((i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1))
        ((Equiv.symm i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) j.succ) :
      Fin (n + 1))
    ((i.cycleRange : (a : Fin (n + 1)) → Fin (n + 1)) (i.succAbove j) : Fin (n + 1))

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
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)
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 : α)
⊢ 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 : α)

Tactic:
cases j using Fin.cases
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : 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)) 0) :
      α)
    (cons (α := fun (a : Fin (n + 1)) ↦ α) a x 0)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
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:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
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 : α)
⊢ 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)

Tactic:
ext j
-- Module: Mathlib.GroupTheory.Perm.Fin
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 (i : Fin (n + 1)) ↦ α) a x j : α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
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)
rw₁ 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)
⊢ 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 : α)

Tactic:
rw [← insertNth_apply_cycleRange_symm, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, Fin.insertNth_apply_cycleRange_symm
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
α : Type u_1
a : α
x : Fin n → α
p : Fin (n + 1)
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 : α)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
α : Type u_1
a : α
x : Fin n → α
p 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:
simp