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

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
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
⊢ (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) ⋯

Tactic:
simpa [symm_apply_eq] using eq_of_val_eq (by simp; lia)

Premises used: Fin.eq_of_val_eq, Equiv.symm_apply_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
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
⊢ (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) ⋯

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)
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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) ⋯
simp :
  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 : ℕ)))) =
    if k = j then i else k + 1
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = if k = j then i else k + 1

Tactic:
simp only [cycleIcc_to_cycleRange hij kin, natAdd_castLEEmb, this, Function.Embedding.trans_apply,
    addNatEmb_apply, coe_toEmbedding, finCongr_apply]

Premises used: finCongr_apply, Equiv.coe_toEmbedding, Fin.cycleIcc_to_cycleRange, Function.Embedding.trans_apply, Fin.natAdd_castLEEmb, Fin.addNatEmb_apply
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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 : ℕ)))) =
    if k = j then i else k + 1

Tactic:
eq_of_val_eq ?_

Premises used: Fin.eq_of_val_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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) ⋯
refine :
  (↑(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 : ℕ))))) :
      ℕ) =
    (↑(if k = j then i else k + 1) : ℕ)
⊢ 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 : ℕ)))) =
    if k = j then i else k + 1

Tactic:
refine eq_of_val_eq ?_

Premises used: Fin.eq_of_val_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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 :
  ∀ (ch : k = j),
    (↑(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 : ℕ))))) :
        ℕ) =
      (↑i : ℕ)
neg :
  ∀ (ch : ¬k = j),
    (↑(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 + 1) : ℕ)
⊢ (↑(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 : ℕ))))) :
      ℕ) =
    (↑(if k = j then i else k + 1) : ℕ)

Tactic:
split_ifs with ch
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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) ⋯
ch : k = j
⊢ n = n - (↑i : ℕ) + (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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) ⋯
ch : k = j
⊢ (↑i : ℕ) ≤ (↑(Fin.cast ⋯ j) : ℕ)

Tactic:
simp [hij]
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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) ⋯
ch : k = j
⊢ (↑(subNat (↑i : ℕ) (Fin.cast ⋯ j) ⋯) : ℕ) = (↑((j - i).castLT ⋯) : ℕ)

Tactic:
simp [sub_val_of_le hij]

Premises used: Fin.sub_val_of_le
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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) ⋯
ch : k = j
⊢ subNat (↑i : ℕ) (Fin.cast ⋯ j) ⋯ = (j - i).castLT ⋯

Tactic:
have : subNat i.1 (j.cast (by lia)) (by simp [hij]) = (j - i).castLT (sub_val_lt_sub hij) :=
      eq_of_val_eq (by simp [sub_val_of_le hij])
-- Module: Mathlib.GroupTheory.Perm.Fin
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
this_1 :
  (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) ⋯
ch : k = j
this : subNat (↑i : ℕ) (Fin.cast ⋯ j) ⋯ = (j - i).castLT ⋯
pos : n - (n - (↑i : ℕ)) = (↑i : ℕ)
⊢ (↑(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 : ℕ))))) :
      ℕ) =
    (↑i : ℕ)

Tactic:
simp [ch, cycleRange_of_eq this]

Premises used: Fin.cycleRange_of_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
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
this_1 :
  (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) ⋯
ch : k = j
this : subNat (↑i : ℕ) (Fin.cast ⋯ j) ⋯ = (j - i).castLT ⋯
⊢ n - (n - (↑i : ℕ)) = (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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) ⋯
ch : ¬k = j
⊢ n = n - (↑i : ℕ) + (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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) ⋯
ch : ¬k = j
⊢ (↑i : ℕ) ≤ (↑(Fin.cast ⋯ k) : ℕ)

Tactic:
simp [hik]
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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) ⋯
ch : ¬k = j
simp : (↑k : ℕ) - (↑i : ℕ) < (↑j : ℕ) - (↑i : ℕ)
⊢ subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯

Tactic:
simp [lt_def, sub_val_of_le hij]

Premises used: Fin.sub_val_of_le, Fin.lt_def
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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) ⋯
ch : ¬k = j
⊢ (↑k : ℕ) - (↑i : ℕ) < (↑j : ℕ) - (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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) ⋯
ch : ¬k = j
⊢ subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯

Tactic:
have : subNat i.1 (k.cast (by lia)) (by simp [hik]) < (j - i).castLT (sub_val_lt_sub hij) := by
      simp [lt_def, sub_val_of_le hij]; lia
-- Module: Mathlib.GroupTheory.Perm.Fin
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
this_1 :
  (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) ⋯
ch : ¬k = j
this : subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
neg :
  (↑(Fin.cast ⋯
          ((HAdd.hAdd (α := Fin (n - (↑i : ℕ))) (⟨(↑(Fin.cast ⋯ k) : ℕ) - (↑i : ℕ), ⋯⟩ : Fin (n - (↑i : ℕ))) 1).addNat
            (n - (n - (↑i : ℕ))))) :
      ℕ) =
    (↑(k + 1) : ℕ)
⊢ (↑(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 + 1) : ℕ)

Tactic:
rw [cycleRange_of_lt this, subNat]

Premises used: Fin.cycleRange_of_lt, Fin.subNat