awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
h0 : i ≠ 0
obtain : ∀ (i : ℕ) (hi : i < n) (h0 : (⟨i, hi⟩ : Fin n) ≠ 0), (⟨i, hi⟩ : Fin n).cycleRange.IsCycle
⊢ i.cycleRange.IsCycle

Tactic:
obtain ⟨i, hi⟩ := i
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
i : ℕ
hi : i < n
h0 : (⟨i, hi⟩ : Fin n) ≠ 0
zero : ∀ (hi : 0 < n) (h0 : (⟨0, hi⟩ : Fin n) ≠ 0), (⟨0, hi⟩ : Fin n).cycleRange.IsCycle
succ : ∀ (n_1 : ℕ) (hi : n_1 + 1 < n) (h0 : (⟨n_1 + 1, hi⟩ : Fin n) ≠ 0), (⟨n_1 + 1, hi⟩ : Fin n).cycleRange.IsCycle
⊢ (⟨i, hi⟩ : Fin n).cycleRange.IsCycle

Tactic:
cases i
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
hi : 0 < n
h0 : (⟨0, hi⟩ : Fin n) ≠ 0
⊢ (⟨0, hi⟩ : Fin n).cycleRange.IsCycle

Tactic:
(h0 rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
hi : 0 < n
h0 : (⟨0, hi⟩ : Fin n) ≠ 0
⊢ (⟨0, hi⟩ : Fin n).cycleRange.IsCycle

Tactic:
exact (h0 rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
n_1 : ℕ
hi : n_1 + 1 < n
h0 : (⟨n_1 + 1, hi⟩ : Fin n) ≠ 0
⊢ (⟨n_1 + 1, hi⟩ : Fin n).cycleRange.IsCycle

Tactic:
isCycle_finRotate.extendDomain _

Premises used: Equiv.Perm.IsCycle.extendDomain, Fin.cycleRange, isCycle_finRotate
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
n_1 : ℕ
hi : n_1 + 1 < n
h0 : (⟨n_1 + 1, hi⟩ : Fin n) ≠ 0
⊢ (⟨n_1 + 1, hi⟩ : Fin n).cycleRange.IsCycle

Tactic:
exact isCycle_finRotate.extendDomain _

Premises used: Equiv.Perm.IsCycle.extendDomain, isCycle_finRotate
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
h0 : i ≠ 0
obtain :
  ∀ (i : ℕ) (hi : i < n) (h0 : (⟨i, hi⟩ : Fin n) ≠ 0),
    (⟨i, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨i, hi⟩ : Fin n) : ℕ) + 1}
⊢ i.cycleRange.cycleType = {(↑i : ℕ) + 1}

Tactic:
obtain ⟨i, hi⟩ := i
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
i : ℕ
hi : i < n
h0 : (⟨i, hi⟩ : Fin n) ≠ 0
zero :
  ∀ (hi : 0 < n) (h0 : (⟨0, hi⟩ : Fin n) ≠ 0), (⟨0, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨0, hi⟩ : Fin n) : ℕ) + 1}
succ :
  ∀ (n_1 : ℕ) (hi : n_1 + 1 < n) (h0 : (⟨n_1 + 1, hi⟩ : Fin n) ≠ 0),
    (⟨n_1 + 1, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨n_1 + 1, hi⟩ : Fin n) : ℕ) + 1}
⊢ (⟨i, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨i, hi⟩ : Fin n) : ℕ) + 1}

Tactic:
cases i
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
hi : 0 < n
h0 : (⟨0, hi⟩ : Fin n) ≠ 0
⊢ (⟨0, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨0, hi⟩ : Fin n) : ℕ) + 1}

Tactic:
(h0 rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
hi : 0 < n
h0 : (⟨0, hi⟩ : Fin n) ≠ 0
⊢ (⟨0, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨0, hi⟩ : Fin n) : ℕ) + 1}

Tactic:
exact (h0 rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
inst : NeZero n
n_1 : ℕ
hi : n_1 + 1 < n
h0 : (⟨n_1 + 1, hi⟩ : Fin n) ≠ 0
⊢ (⟨n_1 + 1, hi⟩ : Fin n).cycleRange.cycleType = {(↑(⟨n_1 + 1, hi⟩ : Fin n) : ℕ) + 1}

Tactic:
simp [cycleRange]

Premises used: Fin.cycleRange
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
rw : Eq (α := Multiset ℕ) {(↑2 : ℕ) + 1} {3}
⊢ IsThreeCycle (α := Fin (n + 3)) (cycleRange 2)

Tactic:
rw [IsThreeCycle, cycleType_cycleRange two_ne_zero]

Premises used: Equiv.Perm.IsThreeCycle, Fin.cycleType_cycleRange
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
⊢ Eq (α := Multiset ℕ) {(↑2 : ℕ) + 1} {3}

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
⊢ 0 < n - (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij : i ≤ j
⊢ i.cycleIcc j =
    ((j - i).castLT ⋯).cycleRange.extendDomain (p := fun (x : Fin n) ↦
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) x)
      (Function.Embedding.toEquivRange (natAdd_castLEEmb ⋯))

Tactic:
simp [cycleIcc, hij]

Premises used: Fin.cycleIcc
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij : i < j
⊢ j.cycleIcc i = 1

Tactic:
simp [cycleIcc, hij]

Premises used: Fin.cycleIcc
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij : ¬j ≤ i
⊢ j.cycleIcc i = 1

Tactic:
simp [cycleIcc, hij]

Premises used: Fin.cycleIcc
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : k < i
pos : ∀ (hij : i ≤ j), (i.cycleIcc j : (a : Fin n) → Fin n) k = k
neg : ∀ (hij : ¬i ≤ j), (i.cycleIcc j : (a : Fin n) → Fin n) k = k
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k

Tactic:
by_cases hij : i ≤ j
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : k < i
hij : i ≤ j
simp : (↑k : ℕ) + (n - (↑i : ℕ)) < n
⊢ k ∉ Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)

Tactic:
simp [range_natAdd_castLEEmb]

Premises used: Fin.range_natAdd_castLEEmb
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : k < i
hij : i ≤ j
⊢ (↑k : ℕ) + (n - (↑i : ℕ)) < n

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : k < i
hij : i ≤ j
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k

Tactic:
simpa [hij] using Perm.extendDomain_apply_not_subtype _ _ (by
      simp [range_natAdd_castLEEmb]; lia)

Premises used: Equiv.Perm.extendDomain_apply_not_subtype
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : k < i
hij : ¬i ≤ j
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k

Tactic:
simp [hij]
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
⊢ Eq (α := Fin n) ((i.cycleIcc j : (a : Fin n) → Fin n) k : Fin n)
    ((natAdd_castLEEmb ⋯ : (a : Fin (n - (↑i : ℕ))) → Fin n)
        ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
          ((Equiv.symm (Function.Embedding.toEquivRange (natAdd_castLEEmb ⋯)) :
              (a : (↑(Set.range (⇑(natAdd_castLEEmb ⋯) : (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 : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) x)
              k kin))) :
      Fin n)

Tactic:
simp [hij, ((j - i).castLT (sub_val_lt_sub hij)).cycleRange.extendDomain_apply_subtype
    (natAdd_castLEEmb _).toEquivRange kin]

Premises used: Equiv.Perm.extendDomain_apply_subtype, HSub.hSub, Fin.natAdd_castLEEmb, Fin.cycleRange, Function.Embedding.toEquivRange, Fin.sub_val_lt_sub, Fin.castLT
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
pos : ∀ (hij : i ≤ j), (i.cycleIcc j : (a : Fin n) → Fin n) k = k
neg : ∀ (hij : ¬i ≤ j), (i.cycleIcc j : (a : Fin n) → Fin n) k = k
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k

Tactic:
by_cases hij : i ≤ j
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
simp : n ≤ (↑k : ℕ) + (n - (↑i : ℕ))
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k

Tactic:
simp [range_natAdd_castLEEmb]

Premises used: Fin.range_natAdd_castLEEmb
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
⊢ n ≤ (↑k : ℕ) + (n - (↑i : ℕ))

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k

Tactic:
have kin : k ∈ Set.range (natAdd_castLEEmb (Nat.sub_le n i)) := by
      simp [range_natAdd_castLEEmb]; lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
⊢ n = n - (↑i : ℕ) + (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
simp : i ≤ k
⊢ (↑i : ℕ) ≤ (↑(Fin.cast ⋯ k) : ℕ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
⊢ i ≤ k

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
simp : (↑k : ℕ) = (↑k : ℕ) - (↑i : ℕ) + (n - (n - (↑i : ℕ)))
⊢ (↑k : ℕ) = (↑(Fin.cast ⋯ ((subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯).addNat (n - (n - (↑i : ℕ))))) : ℕ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
⊢ (↑k : ℕ) = (↑k : ℕ) - (↑i : ℕ) + (n - (n - (↑i : ℕ)))

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
⊢ (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
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
⊢ (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
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
pos :
  Fin.cast (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
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k

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
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
pos : Fin.cast ⋯ ((subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯).addNat (n - (n - (↑i : ℕ)))) = k
pos₁ : (j - i).castLT ⋯ < subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) ⋯
      (addNat
        ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
          (subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯))
        (n - (n - (↑i : ℕ)))) =
    k

Tactic:
rw [cycleRange_of_gt]

Premises used: Fin.cycleRange_of_gt
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
simp : (↑k : ℕ) - (↑i : ℕ) + (n - (n - (↑i : ℕ))) = (↑k : ℕ)
⊢ (↑(Fin.cast ⋯ ((subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯).addNat (n - (n - (↑i : ℕ))))) : ℕ) = (↑k : ℕ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ (↑k : ℕ) - (↑i : ℕ) + (n - (n - (↑i : ℕ))) = (↑k : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ Fin.cast ⋯ ((subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯).addNat (n - (n - (↑i : ℕ)))) = k

Tactic:
exact eq_of_val_eq (by simp; lia)

Premises used: Fin.eq_of_val_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
simp : (↑j : ℕ) - (↑i : ℕ) < (↑k : ℕ) - (↑i : ℕ)
⊢ (↑((j - i).castLT ⋯) : ℕ) < (↑(subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯) : ℕ)

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
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ (↑j : ℕ) - (↑i : ℕ) < (↑k : ℕ) - (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ (j - i).castLT ⋯ < subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯

Tactic:
exact lt_def.mpr (by simp [sub_val_of_le hij]; lia)

Premises used: Iff.mpr, Fin.lt_def
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
h : j < k
hij : ¬i ≤ j
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k

Tactic:
simp [hij]
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
⊢ i ≤ j

Tactic:
have hij : i ≤ j := le_trans hik hkj
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
simp : n ≤ (↑k : ℕ) + (n - (↑i : ℕ))
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k

Tactic:
simp [range_natAdd_castLEEmb]

Premises used: Fin.range_natAdd_castLEEmb
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
⊢ n ≤ (↑k : ℕ) + (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
⊢ Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k

Tactic:
have kin : k ∈ Set.range (natAdd_castLEEmb (Nat.sub_le n i)) := by
    simp [range_natAdd_castLEEmb]; lia
-- 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
⊢ 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
simp : i ≤ k
⊢ (↑i : ℕ) ≤ (↑(Fin.cast ⋯ k) : ℕ)

Tactic:
simp
-- 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
⊢ i ≤ k

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
simp : (↑k : ℕ) = (↑k : ℕ) - (↑i : ℕ) + (n - (n - (↑i : ℕ)))
⊢ (↑k : ℕ) = (↑(Fin.cast ⋯ ((subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯).addNat (n - (n - (↑i : ℕ))))) : ℕ)

Tactic:
simp