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
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 : ((↑k : ℕ) - (↑i : ℕ) + 1) % (n - (↑i : ℕ)) + (n - (n - (↑i : ℕ))) = ((↑k : ℕ) + 1) % n
⊢ (↑(Fin.cast ⋯
          ((HAdd.hAdd (α := Fin (n - (↑i : ℕ))) (⟨(↑(Fin.cast ⋯ k) : ℕ) - (↑i : ℕ), ⋯⟩ : Fin (n - (↑i : ℕ))) 1).addNat
            (n - (n - (↑i : ℕ))))) :
      ℕ) =
    (↑(k + 1) : ℕ)

Tactic:
simp only [val_cast, add_def, val_one', Nat.add_mod_mod, addNat_mk, cast_mk]

Premises used: Fin.val_one', Fin.add_def, Fin.addNat_mk, Nat.add_mod_mod, Fin.val_cast, Fin.cast_mk
-- 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 ⋯
⊢ (↑k : ℕ) - (↑i : ℕ) + 1 < 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
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 ⋯
⊢ (↑k : ℕ) + 1 < n

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_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 : (↑k : ℕ) - (↑i : ℕ) + 1 + (n - (n - (↑i : ℕ))) = (↑k : ℕ) + 1
⊢ ((↑k : ℕ) - (↑i : ℕ) + 1) % (n - (↑i : ℕ)) + (n - (n - (↑i : ℕ))) = ((↑k : ℕ) + 1) % n

Tactic:
rw [Nat.mod_eq_of_lt (by lia), Nat.mod_eq_of_lt (by lia)]

Premises used: Nat.mod_eq_of_lt
-- 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 ⋯
⊢ (↑k : ℕ) - (↑i : ℕ) + 1 + (n - (n - (↑i : ℕ))) = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k < j
inst : NeZero n
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = k + 1

Tactic:
simp [cycleIcc_of_le_of_le hik (le_of_lt hkj), Fin.ne_of_lt hkj]

Premises used: Fin.ne_of_lt, le_of_lt, Fin.cycleIcc_of_le_of_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij : i ≤ j
inst : NeZero n
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) j = i

Tactic:
simp [cycleIcc_of_le_of_le hij (ge_of_eq rfl)]

Premises used: ge_of_eq, Fin.cycleIcc_of_le_of_le, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
H : ∀ (k : Fin n), (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑((1 : (a : Fin n) → Fin n) k) : ℕ)
⊢ i.cycleIcc i = 1

Tactic:
ext k
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
k : Fin n
H : (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
⊢ (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑((1 : (a : Fin n) → Fin n) k) : ℕ)

Tactic:
simp only [Perm.coe_one, id_eq]

Premises used: Equiv.Perm.coe_one, id_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
k : Fin n
H : ∀ (ch : k < i), (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
H₁ : ∀ (ch : k = i), (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
H₂ : ∀ (ch : i < k), (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
⊢ (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)

Tactic:
rcases lt_trichotomy k i with ch | ch | ch

Premises used: lt_trichotomy
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
k : Fin n
ch : k < i
⊢ (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)

Tactic:
simp [-cycleIcc_def_le, cycleIcc_of_lt, ch]

Premises used: Fin.cycleIcc_of_lt, Fin.cycleIcc_def_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
k : Fin n
ch : k = i
⊢ (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)

Tactic:
simp [-cycleIcc_def_le, ch]

Premises used: Fin.cycleIcc_def_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
k : Fin n
ch : i < k
⊢ (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)

Tactic:
simp [-cycleIcc_def_le, cycleIcc_of_gt, ch]

Premises used: Fin.cycleIcc_of_gt, Fin.cycleIcc_def_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij : i ≤ j
inst : NeZero n
inl : ∀ (hij : i < j), j.cycleIcc i = 1
inr : ∀ (hij : i = j), j.cycleIcc i = 1
⊢ j.cycleIcc i = 1

Tactic:
rcases Fin.lt_or_eq_of_le hij with hij | hij

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

Tactic:
simp [hij]
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij_1 : i ≤ j
inst : NeZero n
hij : i = j
inr : j.cycleIcc j = 1
inr₁ : j.cycleIcc j = j.cycleIcc j
rw : Fin n
inr₂ : j.cycleIcc j = j.cycleIcc j
rw₁ : Fin n
⊢ j.cycleIcc i = 1

Tactic:
rw [hij, ← cycleIcc_eq]

Premises used: Fin.cycleIcc_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij : i ≤ j
⊢ (Perm.sign : (a : Perm (Fin n)) → ℤˣ) (i.cycleIcc j) = HPow.hPow (α := ℤˣ) (-1) ((↑j : ℕ) - (↑i : ℕ))

Tactic:
simp [hij, sub_val_of_le hij]

Premises used: Fin.sub_val_of_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
rw : HPow.hPow (α := ℤˣ) (-1) ((↑i : ℕ) - (↑i : ℕ)) = 1
rw₁ : HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 0 = 1
rw₂ rw₃ : Eq (α := ℤˣ) 1 1
⊢ Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (i.cycleIcc i) : ℤˣ) (1 : ℤˣ)

Tactic:
rw [sign_cycleIcc_of_le (Fin.ge_of_eq rfl), tsub_self, pow_zero]

Premises used: Fin.ge_of_eq, tsub_self, Fin.sign_cycleIcc_of_le, pow_zero, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij : i ≤ j
inl : ∀ (hij : i < j), Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)
inr : ∀ (hij : i = j), Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)
⊢ Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)

Tactic:
rcases Fin.lt_or_eq_of_le hij with hij | hij

Premises used: Fin.lt_or_eq_of_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij_1 : i ≤ j
hij : i < j
⊢ Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)

Tactic:
simp [Fin.not_le.mpr hij]

Premises used: Iff.mpr, Fin.not_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij_1 : i ≤ j
hij : i = j
inr : Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc j) : ℤˣ) (1 : ℤˣ)
inr₁ inr₂ : Eq (α := ℤˣ) 1 1
⊢ Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)

Tactic:
rw [hij, sign_cycleIcc_of_eq]

Premises used: Fin.sign_cycleIcc_of_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij : i < j
⊢ (i.cycleIcc j).IsCycle

Tactic:
simpa [le_of_lt hij] using Equiv.Perm.IsCycle.extendDomain
    (natAdd_castLEEmb _).toEquivRange (isCycle_cycleRange (castLT_sub_nezero hij))

Premises used: Equiv.Perm.IsCycle.extendDomain, le_of_lt, Fin.natAdd_castLEEmb, Fin.isCycle_cycleRange, Function.Embedding.toEquivRange, Fin.castLT_sub_nezero
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij : i < j
⊢ (i.cycleIcc j).cycleType = {(↑j : ℕ) - (↑i : ℕ) + 1}

Tactic:
simpa [le_of_lt hij, cycleType_cycleRange (castLT_sub_nezero hij)] using sub_val_of_le
    (le_of_lt hij)

Premises used: Fin.sub_val_of_le, le_of_lt, Fin.castLT_sub_nezero, Fin.cycleType_cycleRange
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
hij : i ≤ j
inst : NeZero n
⊢ (j.cycleIcc i).cycleType = ∅

Tactic:
simpa using cycleIcc_ge hij

Premises used: Fin.cycleIcc_ge
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
H : ∀ (x : Fin n), (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
⊢ cycleIcc 0 i = i.cycleRange

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
x : Fin n
H : ∀ (ch : x < i), (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
H₁ : ∀ (ch : x = i), (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
H₂ : ∀ (ch : i < x), (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
⊢ (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
rcases lt_trichotomy x i with ch | ch | ch

Premises used: lt_trichotomy
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
x : Fin n
ch : x < i
⊢ (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
simp [-cycleIcc_def_le, cycleIcc_of_ge_of_lt (zero_le x) ch, cycleRange_of_lt ch]

Premises used: Fin.zero_le, Fin.cycleIcc_of_ge_of_lt, Fin.cycleRange_of_lt, Fin.cycleIcc_def_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
x : Fin n
ch : x = i
⊢ (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
simp [-cycleIcc_def_le, ch]

Premises used: Fin.cycleIcc_def_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n
inst : NeZero n
x : Fin n
ch : i < x
⊢ (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
simp [-cycleIcc_def_le, cycleIcc_of_gt ch, cycleRange_of_gt ch]

Premises used: Fin.cycleIcc_of_gt, Fin.cycleRange_of_gt, Fin.cycleIcc_def_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
⊢ (⇑(i.cycleIcc j) : (a : Fin (n + 1)) → Fin (n + 1)) ∘ j.succAbove = i.succAbove

Tactic:
grind [cycleIcc_of_lt, succAbove_of_castSucc_lt, cycleIcc_of_ge_of_lt,
    succAbove_of_le_castSucc, coeSucc_eq_succ, cycleIcc_of_gt]

Premises used: Fin.succAbove_of_le_castSucc, Fin.cycleIcc_of_gt, Fin.cycleIcc_of_ge_of_lt, Fin.coeSucc_eq_succ, Fin.succAbove_of_castSucc_lt, Fin.cycleIcc_of_lt
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
h :
  ∀ (x : Fin n),
    (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
        ℕ) =
      (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
⊢ Eq (α := Fin n → Fin n)
    (Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n))
    (⇑(i.cycleIcc k) : (a : Fin n) → Fin n)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
h :
  ∀ (ch : x < i),
    (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
        ℕ) =
      (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
h₁ :
  ∀ (ch : i ≤ x),
    (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
        ℕ) =
      (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
rcases lt_or_ge x i with ch | ch

Premises used: lt_or_ge
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : x < i
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
simp [cycleIcc_of_lt (lt_of_lt_of_le ch hij), cycleIcc_of_lt ch]

Premises used: Fin.cycleIcc_of_lt, lt_of_lt_of_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
h :
  ∀ (ch : k < x),
    (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
        ℕ) =
      (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
h₁ :
  ∀ (ch1 : x ≤ k),
    (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
        ℕ) =
      (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
rcases lt_or_ge k x with ch | ch1

Premises used: lt_or_ge
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch_1 : i ≤ x
ch : k < x
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
simp [cycleIcc_of_gt (lt_of_le_of_lt hjk ch), cycleIcc_of_gt ch]

Premises used: lt_of_le_of_lt, Fin.cycleIcc_of_gt
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
h :
  ∀ (ch2 : x < j),
    (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
        ℕ) =
      (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
h₁ :
  ∀ (ch2 : j ≤ x),
    (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
        ℕ) =
      (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
rcases lt_or_ge x j with ch2 | ch2

Premises used: lt_or_ge
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
h : (↑(if x = j then i else x + 1) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
simp [cycleIcc_of_lt ch2, cycleIcc_of_le_of_le ch ch1, cycleIcc_of_le_of_le ch (le_of_lt ch2)]

Premises used: le_of_lt, Fin.cycleIcc_of_lt, Fin.cycleIcc_of_le_of_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
pos : x = j → x = k → (↑i : ℕ) = (↑i : ℕ)
neg : x = j → ¬x = k → (↑i : ℕ) = (↑(x + 1) : ℕ)
pos₁ : ¬x = j → x = k → (↑(x + 1) : ℕ) = (↑i : ℕ)
neg₁ : ¬x = j → ¬x = k → (↑(x + 1) : ℕ) = (↑(x + 1) : ℕ)
⊢ (↑(if x = j then i else x + 1) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)

Tactic:
split_ifs
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
h : x = j
h_1 : x = k
⊢ (↑i : ℕ) = (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
h : x = j
h_1 : ¬x = k
⊢ (↑i : ℕ) = (↑(x + 1) : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
h : ¬x = j
h_1 : x = k
⊢ (↑(x + 1) : ℕ) = (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
h : ¬x = j
h_1 : ¬x = k
⊢ (↑(x + 1) : ℕ) = (↑(x + 1) : ℕ)

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
h : x = j
h_1 : x = k
⊢ (↑i : ℕ) = (↑i : ℕ)

Tactic:
repeat lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
h : (↑((i.cycleIcc j : (a : Fin n) → Fin n) (if x = k then j else x + 1)) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
simp only [Function.comp_apply, cycleIcc_of_le_of_le ch2 ch1, cycleIcc_of_le_of_le ch ch1]

Premises used: Function.comp_apply, Fin.cycleIcc_of_le_of_le
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
pos : ∀ (h : x = k), (↑((i.cycleIcc j : (a : Fin n) → Fin n) j) : ℕ) = (↑i : ℕ)
neg : ∀ (h : ¬x = k), (↑((i.cycleIcc j : (a : Fin n) → Fin n) (x + 1)) : ℕ) = (↑(x + 1) : ℕ)
⊢ (↑((i.cycleIcc j : (a : Fin n) → Fin n) (if x = k then j else x + 1)) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)

Tactic:
split_ifs with h
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
h : x = k
⊢ (↑((i.cycleIcc j : (a : Fin n) → Fin n) j) : ℕ) = (↑i : ℕ)

Tactic:
val_eq_of_eq (cycleIcc_of_last hij)

Premises used: Fin.cycleIcc_of_last, Fin.val_eq_of_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
h : x = k
⊢ (↑((i.cycleIcc j : (a : Fin n) → Fin n) j) : ℕ) = (↑i : ℕ)

Tactic:
exact val_eq_of_eq (cycleIcc_of_last hij)

Premises used: Fin.cycleIcc_of_last, Fin.val_eq_of_eq
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
h : ¬x = k
⊢ (↑x : ℕ) + 1 < n

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
h : ¬x = k
⊢ (↑((i.cycleIcc j : (a : Fin n) → Fin n) (x + 1)) : ℕ) = (↑(x + 1) : ℕ)

Tactic:
simp [cycleIcc_of_gt (lt_of_le_of_lt ch2 (lt_add_one_of_succ_lt (by lia)))]

Premises used: lt_of_le_of_lt, Fin.cycleIcc_of_gt, Fin.lt_add_one_of_succ_lt
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
⊢ Eq (α := Fin n → Fin n)
    (Function.comp (β := Fin n) (⇑(j.cycleIcc i) : (a : Fin n) → Fin n) (⇑(i.cycleIcc k) : (a : Fin n) → Fin n))
    (⇑(i.cycleIcc k) : (a : Fin n) → Fin n)

Tactic:
simp [hij]
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hjk : j ≤ k
⊢ Eq (α := Fin n → Fin n)
    (Function.comp (β := Fin n) (⇑(i.cycleIcc k) : (a : Fin n) → Fin n) (⇑(k.cycleIcc j) : (a : Fin n) → Fin n))
    (⇑(i.cycleIcc k) : (a : Fin n) → Fin n)

Tactic:
simp [hjk]
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
σ : Perm (Fin n)
h : (sign : (a : Perm (Fin n)) → ℤˣ) σ = σ.signAux
rw :
  Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    (∏ x ∈ Finset.sigma (α := fun (a : Fin n) ↦ Fin n) Finset.univ Finset.Iio,
      if
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
            ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
        1
      else -1)
⊢ Eq (α := ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ)
    (∏ j : Fin n,
        ∏ i ∈ Finset.Iio j,
          if LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n) then 1
          else -1 :
      ℤˣ)

Tactic:
rw [h, Finset.prod_sigma', Equiv.Perm.signAux]

Premises used: Equiv.Perm.signAux, Finset.prod_sigma'