awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
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
⊢ IsCycle (α := Fin (n + 2)) (finRotate (n + 2))

Tactic:
refine ⟨0, by simp, fun x hx' => ⟨x, ?_⟩⟩
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
x : Fin (n + 2)
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))
⊢ (HPow.hPow (α := Perm (Fin (n + 2))) (β := ℤ) (finRotate (n + 2)) (↑(↑x : ℕ) : ℤ) : (a : Fin (n + 2)) → Fin (n + 2))
      0 =
    x

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n x : ℕ
hx : x < n + 2
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)) : ℕ)
⊢ (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]

Premises used: zpow_natCast, Fin.ext_iff, Fin.val_mk
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
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:
rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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))
⊢ (↑((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:
rw [pow_succ', Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]

Premises used: lt_trans, Nat.lt_succ_self, coe_finRotate_of_ne_last, Equiv.Perm.mul_apply, pow_succ'
-- Module: Mathlib.GroupTheory.Perm.Fin
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
succ : ¬(↑(⟨x, ⋯⟩ : Fin (n + 2)) : ℕ) = n + 1
⊢ 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 [Ne, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]

Premises used: Fin.ext_iff, lt_trans, Nat.lt_succ_self, Ne, Fin.val_last
-- Module: Mathlib.GroupTheory.Perm.Fin
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
⊢ ¬(↑(⟨x, ⋯⟩ : Fin (n + 2)) : ℕ) = n + 1

Tactic:
ne_of_lt (Nat.lt_of_succ_lt_succ hx)

Premises used: ne_of_lt, Nat.lt_of_succ_lt_succ
-- Module: Mathlib.GroupTheory.Perm.Fin
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
⊢ ¬(↑(⟨x, ⋯⟩ : Fin (n + 2)) : ℕ) = n + 1

Tactic:
exact ne_of_lt (Nat.lt_of_succ_lt_succ hx)

Premises used: ne_of_lt, Nat.lt_of_succ_lt_succ
-- Module: Mathlib.GroupTheory.Perm.Fin
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)) : ℕ)
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)) : ℕ)
⊢ (↑((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:
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)

Premises used: Fin.ext_iff, Ne, coe_finRotate_of_ne_last, Equiv.Perm.mul_apply, pow_succ', Fin.val_last
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
h : 2 ≤ n
obtain : ∀ (m : ℕ) (h : 2 ≤ 2 + m), IsCycle (α := Fin (2 + m)) (finRotate (2 + m))
⊢ (finRotate n).IsCycle

Tactic:
obtain ⟨m, rfl⟩ := exists_add_of_le h

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
m : ℕ
h : 2 ≤ 2 + m
rw : IsCycle (α := Fin (m + 2)) (finRotate (m + 2))
⊢ IsCycle (α := Fin (2 + m)) (finRotate (2 + m))

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
m : ℕ
h : 2 ≤ 2 + m
⊢ IsCycle (α := Fin (m + 2)) (finRotate (m + 2))

Tactic:
isCycle_finRotate

Premises used: isCycle_finRotate
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
m : ℕ
h : 2 ≤ 2 + m
⊢ IsCycle (α := Fin (m + 2)) (finRotate (m + 2))

Tactic:
exact isCycle_finRotate

Premises used: isCycle_finRotate
-- Module: Mathlib.GroupTheory.Perm.Fin
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}
rw₃ rw₄ : Eq (α := Multiset ℕ) {n + 2} {n + 2}
⊢ cycleType (α := Fin (n + 2)) (finRotate (n + 2)) = {n + 2}

Tactic:
rw [isCycle_finRotate.cycleType, support_finRotate, ← Fintype.card, Fintype.card_fin]

Premises used: Fintype.card_fin, Fintype.card, Equiv.Perm.IsCycle.cycleType, support_finRotate, isCycle_finRotate
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
h : 2 ≤ n
obtain : ∀ (m : ℕ) (h : 2 ≤ 2 + m), cycleType (α := Fin (2 + m)) (finRotate (2 + m)) = {2 + m}
⊢ (finRotate n).cycleType = {n}

Tactic:
obtain ⟨m, rfl⟩ := exists_add_of_le h

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
m : ℕ
h : 2 ≤ 2 + m
rw : cycleType (α := Fin (m + 2)) (finRotate (m + 2)) = {m + 2}
rw₁ rw₂ : Eq (α := Multiset ℕ) {m + 2} {m + 2}
⊢ cycleType (α := Fin (2 + m)) (finRotate (2 + m)) = {2 + m}

Tactic:
rw [add_comm, cycleType_finRotate]

Premises used: add_comm, cycleType_finRotate
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n_1 : ℕ
i_1 j : Fin n_1
n : ℕ
i : Fin n
⊢ (↑i : ℕ) + 1 ≤ n

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
h : i < j
h₁ : j ∉ Set.range (ι := Fin ((↑i : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑i : ℕ) + 1)) → Fin n)
⊢ (i.cycleRange : (a : Fin n) → Fin n) j = j

Tactic:
rw [cycleRange, Perm.extendDomain_apply_not_subtype]

Premises used: Equiv.Perm.extendDomain_apply_not_subtype, Fin.cycleRange
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
h : i < j
⊢ j ∉ Set.range (ι := Fin ((↑i : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑i : ℕ) + 1)) → Fin n)

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i ≤ j
⊢ (↑j : ℕ) + 1 ≤ n

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h simp : i ≤ j
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) i

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i ≤ j
⊢ i ≤ j

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i ≤ j
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) i

Tactic:
have iin : i ∈ Set.range (castLEEmb (n := j + 1) (by lia)) := 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
⊢ (↑j : ℕ) + 1 ≤ n

Tactic:
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
⊢ (↑i : ℕ) < (↑j : ℕ) + 1

Tactic:
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
⊢ ((castLEEmb ⋯).toEquivRange : (a : Fin ((↑j : ℕ) + 1)) → (↑(Set.range (castLE ⋯)) : Type)) (i.castLT ⋯) =
    Subtype.mk (p := fun (x : Fin n) ↦ x ∈ Set.range (castLE ⋯)) i iin

Tactic:
rfl
-- 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
⊢ ((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

Tactic:
have : (castLEEmb (by lia)).toEquivRange (castLT i (by lia)) = ⟨i, iin⟩ := by
    simp [coe_castLEEmb]; rfl
-- 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
⊢ (↑j : ℕ) + 1 ≤ n

Tactic:
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
rw :
  (↑(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
⊢ (j.cycleRange : (a : Fin n) → Fin n) i = 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]

Premises used: Equiv.Perm.extendDomain_apply_subtype, Fin.castLEEmb, Fin.val, finRotate, Fin.cycleRange, Function.Embedding.toEquivRange, HAdd.hAdd, OfNat.ofNat, Function.Embedding.toEquivRange_apply
-- 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
⊢ (↑j : ℕ) + 1 ≤ n

Tactic:
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
⊢ (↑(i.castLT ⋯) : ℕ) = (↑(last (↑j : ℕ)) : ℕ)

Tactic:
simp [ch]
-- 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
⊢ 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))

Tactic:
simpa only [coe_castLEEmb, ← this, symm_apply_apply] using eq_of_val_eq (by simp [ch])

Premises used: Equiv.symm_apply_apply, Fin.eq_of_val_eq, Fin.coe_castLEEmb
-- 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
⊢ 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))

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])
-- 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_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))
pos :
  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) 0) ⋯) :
      Fin n)
    0
⊢ 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)

Tactic:
rw [this, finRotate_last]

Premises used: finRotate_last
-- 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_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) 0) ⋯) :
      Fin n)
    0

Tactic:
rfl
-- 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
⊢ (↑i : ℕ) + 1 < n

Tactic:
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
⊢ (↑(i + 1) : ℕ) = (↑i : ℕ) + 1

Tactic:
have hj1 : (i + 1).1 = i.1 + 1 := val_add_one_of_lt' (by 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
⊢ (↑i : ℕ) < (↑j : ℕ) + 1

Tactic:
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
simp : i < j
⊢ (↑(i.castLT ⋯) : ℕ) + 1 < (↑j : ℕ) + 1

Tactic:
simp
-- 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 < j

Tactic:
lia