awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
σ : (↑(vectorsProdEqOne G p) : Type u_3) ≃ (↑(vectorsProdEqOne G p) : Type u_3) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ HPow.hPow (β := ℕ) p 1 = 1
v₀ : (↑(vectorsProdEqOne G p) : Type u_3) :=
  Subtype.mk (p := fun (x : List.Vector G p) ↦ x ∈ vectorsProdEqOne G p) (List.Vector.replicate p 1) ⋯
hv₀ : (σ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v₀ = v₀
v : (↑(vectorsProdEqOne G p) : Type u_3)
hv1 : (σ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = v
hv2 : v ≠ v₀
g : G
hg : (↑(↑v : List.Vector G p) : List G) = List.replicate (↑(↑v : List.Vector G p) : List G).length g
hg' : g = 1
refine_2 : List.replicate p 1 = (↑(↑v₀ : List.Vector G p) : List G)
⊢ v = v₀

Tactic:
rw [Subtype.ext_iff, Subtype.ext_iff, hg, hg', v.1.2]

Premises used: Subtype.ext_iff, Subtype.val, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
σ : (↑(vectorsProdEqOne G p) : Type u_3) ≃ (↑(vectorsProdEqOne G p) : Type u_3) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ HPow.hPow (β := ℕ) p 1 = 1
v₀ : (↑(vectorsProdEqOne G p) : Type u_3) :=
  Subtype.mk (p := fun (x : List.Vector G p) ↦ x ∈ vectorsProdEqOne G p) (List.Vector.replicate p 1) ⋯
hv₀ : (σ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v₀ = v₀
v : (↑(vectorsProdEqOne G p) : Type u_3)
hv1 : (σ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = v
hv2 : v ≠ v₀
g : G
hg : (↑(↑v : List.Vector G p) : List G) = List.replicate (↑(↑v : List.Vector G p) : List G).length g
hg' : g = 1
⊢ List.replicate p 1 = (↑(↑v₀ : List.Vector G p) : List G)

Tactic:
simp only [v₀, List.Vector.replicate]

Premises used: List.Vector.replicate
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_3
inst : AddGroup G
inst_1 : Fintype G
p : ℕ
inst_2 : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ p ∣ Fintype.card G

Tactic:
hdvd
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_3
inst : AddGroup G
inst_1 : Fintype G
p : ℕ
inst_2 : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ p ∣ Fintype.card.{u_3} (Multiplicative G)

Tactic:
convert! hdvd
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Nat.card G
have : ∀ (this : Fintype G), ∃ (x : G), orderOf x = p
⊢ ∃ (x : G), orderOf x = p

Tactic:
have := Fintype.ofFinite G
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Nat.card G
this : Fintype G
⊢ p ∣ Fintype.card G

Tactic:
rw [Nat.card_eq_fintype_card] at hdvd

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
this : Fintype G
hdvd : p ∣ Fintype.card G
⊢ ∃ (x : G), orderOf x = p

Tactic:
exists_prime_orderOf_dvd_card p hdvd

Premises used: exists_prime_orderOf_dvd_card
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
this : Fintype G
hdvd : p ∣ Fintype.card G
⊢ ∃ (x : G), orderOf x = p

Tactic:
exact exists_prime_orderOf_dvd_card p hdvd

Premises used: exists_prime_orderOf_dvd_card
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
⊢ Fact (Nat.Prime (Fintype.card α))

Tactic:
haveI : Fact (Fintype.card α).Prime := ⟨h0⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
obtain : ∀ (σ : ↥H) (hσ : orderOf σ = Fintype.card α), H = ⊤
⊢ H = ⊤

Tactic:
obtain ⟨σ, hσ⟩ := exists_prime_orderOf_dvd_card (Fintype.card α) h1

Premises used: Fintype.card, exists_prime_orderOf_dvd_card
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
⊢ orderOf (↑σ : Perm α) = Fintype.card α

Tactic:
have hσ1 : orderOf (σ : Perm α) = Fintype.card α := (Subgroup.orderOf_coe σ).trans hσ
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf (↑σ : Perm α) = Fintype.card α
⊢ (↑σ : Perm α).IsCycle

Tactic:
have hσ2 : IsCycle ↑σ := isCycle_of_prime_order'' h0 hσ1
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf (↑σ : Perm α) = Fintype.card α
hσ2 : (↑σ : Perm α).IsCycle
⊢ (↑σ : Perm α).support = ⊤

Tactic:
have hσ3 : (σ : Perm α).support = ⊤ :=
    Finset.eq_univ_of_card (σ : Perm α).support (hσ2.orderOf.symm.trans hσ1)
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf (↑σ : Perm α) = Fintype.card α
hσ2 : (↑σ : Perm α).IsCycle
hσ3 : (↑σ : Perm α).support = ⊤
⊢ Eq (α := Subgroup (Perm α)) (Subgroup.closure {(↑σ : Perm α), τ}) ⊤

Tactic:
have hσ4 : Subgroup.closure {↑σ, τ} = ⊤ := closure_prime_cycle_swap h0 hσ2 hσ3 h3
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf (↑σ : Perm α) = Fintype.card α
hσ2 : (↑σ : Perm α).IsCycle
hσ3 : (↑σ : Perm α).support = ⊤
hσ4 : Eq (α := Subgroup (Perm α)) (Subgroup.closure {(↑σ : Perm α), τ}) ⊤
rw : (↑σ : Perm α) ∈ (↑H : Set (Perm α)) ∧ τ ∈ (↑H : Set (Perm α))
⊢ H = ⊤

Tactic:
rw [eq_top_iff, ← hσ4, Subgroup.closure_le, Set.insert_subset_iff, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, eq_top_iff, Subgroup.closure_le, Set.insert_subset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf (↑σ : Perm α) = Fintype.card α
hσ2 : (↑σ : Perm α).IsCycle
hσ3 : (↑σ : Perm α).support = ⊤
hσ4 : Eq (α := Subgroup (Perm α)) (Subgroup.closure {(↑σ : Perm α), τ}) ⊤
⊢ (↑σ : Perm α) ∈ (↑H : Set (Perm α)) ∧ τ ∈ (↑H : Set (Perm α))

Tactic:
⟨Subtype.mem σ, h2⟩

Premises used: And.intro, Subtype.mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf (↑σ : Perm α) = Fintype.card α
hσ2 : (↑σ : Perm α).IsCycle
hσ3 : (↑σ : Perm α).support = ⊤
hσ4 : Eq (α := Subgroup (Perm α)) (Subgroup.closure {(↑σ : Perm α), τ}) ⊤
⊢ (↑σ : Perm α) ∈ (↑H : Set (Perm α)) ∧ τ ∈ (↑H : Set (Perm α))

Tactic:
exact ⟨Subtype.mem σ, h2⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
inl : ∀ (hn : n ∈ σ.cycleType), 0 < n
inr : ∀ (hn : Membership.mem (γ := Multiset ℕ) (Multiset.replicate (Fintype.card α - #σ.support) 1) n), 0 < n
⊢ 0 < n

Tactic:
rcases mem_add.mp hn with hn | hn

Premises used: Multiset.mem_add, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn_1 : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
hn : n ∈ σ.cycleType
⊢ 0 < n

Tactic:
zero_lt_one.trans (one_lt_of_mem_cycleType hn)

Premises used: zero_lt_one, LT.lt.trans, Equiv.Perm.one_lt_of_mem_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn_1 : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
hn : n ∈ σ.cycleType
⊢ 0 < n

Tactic:
exact zero_lt_one.trans (one_lt_of_mem_cycleType hn)

Premises used: zero_lt_one, LT.lt.trans, Equiv.Perm.one_lt_of_mem_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn_1 : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
hn : Membership.mem (γ := Multiset ℕ) (Multiset.replicate (Fintype.card α - #σ.support) 1) n
⊢ 0 < n

Tactic:
lt_of_lt_of_le zero_lt_one (ge_of_eq (Multiset.eq_of_mem_replicate hn))

Premises used: ge_of_eq, zero_lt_one, Multiset.eq_of_mem_replicate, lt_of_lt_of_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn_1 : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
hn : Membership.mem (γ := Multiset ℕ) (Multiset.replicate (Fintype.card α - #σ.support) 1) n
⊢ 0 < n

Tactic:
exact lt_of_lt_of_le zero_lt_one (ge_of_eq (Multiset.eq_of_mem_replicate hn))

Premises used: ge_of_eq, zero_lt_one, Multiset.eq_of_mem_replicate, lt_of_lt_of_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : σ.cycleType.sum + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
rw₁ : #σ.support + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
rw₂ : #σ.support + HSMul.hSMul (β := ℕ) (Fintype.card α - #σ.support) 1 = Fintype.card α
rw₃ : #σ.support + HMul.hMul (α := ℕ) (↑(Fintype.card α - #σ.support) : ℕ) 1 = Fintype.card α
rw₄ : #σ.support + (Fintype.card α - #σ.support) * 1 = Fintype.card α
rw₅ : #σ.support + (Fintype.card α - #σ.support) = Fintype.card α
rw₆ rw₇ : Fintype.card α = Fintype.card α
⊢ (σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α

Tactic:
rw [sum_add, sum_cycleType, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_one,
      add_tsub_cancel_of_le σ.support.card_le_univ]

Premises used: Equiv.Perm.support, Nat.cast_id, Multiset.sum_add, Multiset.sum_replicate, Finset.card_le_univ, nsmul_eq_mul, mul_one, Equiv.Perm.sum_cycleType, add_tsub_cancel_of_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ Nat.Partition.parts (n := Fintype.card α) σ.partition =
    σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : ∀ (a : ℕ) (h : Membership.mem (γ := Multiset ℕ) (Multiset.replicate (Fintype.card α - #σ.support) 1) a), ¬2 ≤ a
⊢ Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) σ.partition) = σ.cycleType

Tactic:
rw [parts_partition, filter_add, Multiset.filter_eq_self.2 fun _ => two_le_of_mem_cycleType,
    Multiset.filter_eq_nil.2 fun a h => ?_, add_zero]

Premises used: Iff.mpr, Multiset.filter_eq_self, Multiset.filter_eq_nil, Equiv.Perm.two_le_of_mem_cycleType, Multiset.filter_add, Equiv.Perm.parts_partition, add_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
a : ℕ
h : Membership.mem (γ := Multiset ℕ) (Multiset.replicate (Fintype.card α - #σ.support) 1) a
rw : ¬LE.le (α := ℕ) 2 1
⊢ ¬2 ≤ a

Tactic:
rw [Multiset.eq_of_mem_replicate h]

Premises used: Multiset.eq_of_mem_replicate
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
a : ℕ
h : Membership.mem (γ := Multiset ℕ) (Multiset.replicate (Fintype.card α - #σ.support) 1) a
⊢ ¬LE.le (α := ℕ) 2 1

Tactic:
decide
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
rw : σ.cycleType = τ.cycleType ↔ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
⊢ IsConj σ τ ↔ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition

Tactic:
rw [isConj_iff_cycleType_eq]

Premises used: Equiv.Perm.isConj_iff_cycleType_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
⊢ σ.cycleType = τ.cycleType ↔ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
refine_1 : ∀ (h : σ.cycleType = τ.cycleType), Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
refine_2 : ∀ (h : Eq (α := (Fintype.card α).Partition) σ.partition τ.partition), σ.cycleType = τ.cycleType
⊢ σ.cycleType = τ.cycleType ↔ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
refine_1 : Nat.Partition.parts (n := Fintype.card α) σ.partition = Nat.Partition.parts (n := Fintype.card α) τ.partition
refine_1₁ :
  σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 =
    Nat.Partition.parts (n := Fintype.card α) τ.partition
refine_1₂ :
  σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 =
    τ.cycleType + Multiset.replicate (Fintype.card α - #τ.support) 1
refine_1₃ :
  σ.cycleType + Multiset.replicate (Fintype.card α - σ.cycleType.sum) 1 =
    τ.cycleType + Multiset.replicate (Fintype.card α - #τ.support) 1
refine_1₄ :
  σ.cycleType + Multiset.replicate (Fintype.card α - σ.cycleType.sum) 1 =
    τ.cycleType + Multiset.replicate (Fintype.card α - τ.cycleType.sum) 1
refine_1₅ refine_1₆ :
  τ.cycleType + Multiset.replicate (Fintype.card α - τ.cycleType.sum) 1 =
    τ.cycleType + Multiset.replicate (Fintype.card α - τ.cycleType.sum) 1
⊢ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition

Tactic:
rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
      h]

Premises used: Equiv.Perm.parts_partition, Nat.Partition.ext_iff, Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
refine_2 : Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) σ.partition) = τ.cycleType
refine_2₁ :
  Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) σ.partition) =
    Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) τ.partition)
refine_2₂ refine_2₃ :
  Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) τ.partition) =
    Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) τ.partition)
⊢ σ.cycleType = τ.cycleType

Tactic:
rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]

Premises used: Equiv.Perm.filter_parts_partition_eq_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
mp : σ.IsSwap → σ.cycleType = {2}
mpr : σ.cycleType = {2} → σ.IsSwap
⊢ σ.IsSwap ↔ σ.cycleType = {2}

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsSwap
⊢ σ.cycleType = {2}

Tactic:
simpa [h.isCycle.cycleType, card_support_eq_two] using h

Premises used: Equiv.Perm.IsCycle.cycleType, Equiv.Perm.IsSwap.isCycle, Equiv.Perm.card_support_eq_two
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.cycleType = {2}
⊢ σ.IsSwap

Tactic:
simp [← card_support_eq_two, ← sum_cycleType, h]

Premises used: Equiv.Perm.card_support_eq_two, Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
σ : Perm α
h : σ.IsSwap
have : ∀ (this : Fintype α), _root_.orderOf σ = 2
⊢ _root_.orderOf σ = 2

Tactic:
have := Fintype.ofFinite α
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
σ : Perm α
h : σ.IsSwap
this : Fintype α
rw : σ.cycleType.lcm = 2
rw₁ : Eq (α := ℕ) (Multiset.lcm {2}) 2
rw₂ : Eq (α := ℕ) ((normalize : (a : ℕ) → ℕ) 2 : ℕ) (2 : ℕ)
rw₃ rw₄ : Eq (α := ℕ) 2 2
⊢ _root_.orderOf σ = 2

Tactic:
rw [← lcm_cycleType, isSwap_iff_cycleType.mp h, Multiset.lcm_singleton, normalize_eq]

Premises used: Multiset.lcm_singleton, Equiv.Perm.lcm_cycleType, Iff.mp, Equiv.Perm.isSwap_iff_cycleType, normalize_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ.cycleType = {3}

Tactic:
h

Premises used: Equiv.Perm.IsThreeCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : IsThreeCycle.{u_1} (α := α) 1
⊢ False

Tactic:
simpa using h.cycleType

Premises used: Equiv.Perm.IsThreeCycle.cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
rw : σ.cycleType.sum = 3
rw₁ : Eq (α := ℕ) (Multiset.sum {3}) 3
rw₂ rw₃ : Eq (α := ℕ) 3 3
⊢ #σ.support = 3

Tactic:
rw [← sum_cycleType, h.cycleType, Multiset.sum_singleton]

Premises used: Multiset.sum_singleton, Equiv.Perm.IsThreeCycle.cycleType, Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ #σ.support = 3 ↔ σ.IsThreeCycle

Tactic:
⟨fun h => ?_, IsThreeCycle.card_support⟩

Premises used: Equiv.Perm.IsThreeCycle.card_support, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
refine : ∀ (h : #σ.support = 3), σ.IsThreeCycle
⊢ #σ.support = 3 ↔ σ.IsThreeCycle

Tactic:
refine ⟨fun h => ?_, IsThreeCycle.card_support⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
pos : ∀ (h0 : σ.cycleType = 0), σ.IsThreeCycle
neg : ∀ (h0 : ¬σ.cycleType = 0), σ.IsThreeCycle
⊢ σ.IsThreeCycle

Tactic:
by_cases h0 : σ.cycleType = 0

Premises used: Equiv.Perm.cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : σ.cycleType = 0
⊢ Eq (α := ℕ) 0 3

Tactic:
rw [← sum_cycleType, h0, sum_zero] at h

Premises used: Multiset.sum_zero, Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : σ.cycleType = 0
h₁ : Eq (α := ℕ) 0 3
⊢ σ.cycleType = 0

Tactic:
rw [← sum_cycleType, h0, sum_zero] at h

Premises used: Multiset.sum_zero, Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : Eq (α := ℕ) 0 3
h0 : σ.cycleType = 0
⊢ σ.IsThreeCycle

Tactic:
(ne_of_lt zero_lt_three h).elim

Premises used: zero_lt_three, False.elim, ne_of_lt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : Eq (α := ℕ) 0 3
h0 : σ.cycleType = 0
⊢ σ.IsThreeCycle

Tactic:
exact (ne_of_lt zero_lt_three h).elim

Premises used: zero_lt_three, False.elim, ne_of_lt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
neg : ∀ (n : ℕ) (hn : n ∈ σ.cycleType), σ.IsThreeCycle
⊢ σ.IsThreeCycle

Tactic:
obtain ⟨n, hn⟩ := exists_mem_of_ne_zero h0

Premises used: Multiset.exists_mem_of_ne_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
pos : ∀ (h1 : σ.cycleType.erase n = 0), σ.IsThreeCycle
neg : ∀ (h1 : ¬σ.cycleType.erase n = 0), σ.IsThreeCycle
⊢ σ.IsThreeCycle

Tactic:
by_cases h1 : σ.cycleType.erase n = 0

Premises used: Equiv.Perm.cycleType, Multiset.erase
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
pos :
  ∀ (h0 : ¬σ.cycleType = 0) (n : ℕ) (h : n = 3) (hn : n ∈ σ.cycleType) (h1 : σ.cycleType.erase n = 0), σ.IsThreeCycle
⊢ σ.IsThreeCycle

Tactic:
rw [← sum_cycleType, ← cons_erase hn, h1, cons_zero, Multiset.sum_singleton] at h

Premises used: Multiset.sum_singleton, Multiset.cons_erase, Equiv.Perm.sum_cycleType, Multiset.cons_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : n = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
pos : σ.cycleType = {3}
pos₁ : n ::ₘ σ.cycleType.erase n = {3}
pos₂ : n ::ₘ 0 = {3}
pos₃ : Eq (α := Multiset ℕ) (3 ::ₘ 0) {3}
pos₄ pos₅ : Eq (α := Multiset ℕ) (3 ::ₘ 0) (3 ::ₘ 0)
⊢ σ.IsThreeCycle

Tactic:
rw [IsThreeCycle, ← cons_erase hn, h1, h, ← cons_zero]

Premises used: Multiset.cons_erase, Equiv.Perm.IsThreeCycle, Multiset.cons_zero