awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
refine_1 : σ.cycleType.card = σ.cycleType.card - 1 + 1
refine_2 : ∀ (n : ℕ) (hn : n ∈ σ.cycleType), n = orderOf σ
⊢ ∃ (n : ℕ), σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)

Tactic:
refine ⟨Multiset.card σ.cycleType - 1, eq_replicate.2 ⟨?_, fun n hn ↦ ?_⟩⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
refine_1 : 1 ≤ σ.cycleType.card
⊢ σ.cycleType.card = σ.cycleType.card - 1 + 1

Tactic:
rw [tsub_add_cancel_of_le]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
refine_1 : ¬orderOf σ = 1
⊢ 1 ≤ σ.cycleType.card

Tactic:
rw [Nat.succ_le_iff, card_cycleType_pos, Ne, ← orderOf_eq_one_iff]

Premises used: Ne, Equiv.Perm.card_cycleType_pos, Nat.succ_le_iff, orderOf_eq_one_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ¬orderOf σ = 1

Tactic:
hσ.ne_one

Premises used: Nat.Prime.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ¬orderOf σ = 1

Tactic:
exact hσ.ne_one

Premises used: Nat.Prime.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ σ.cycleType
⊢ n = orderOf σ

Tactic:
(hσ.eq_one_or_self_of_dvd n (dvd_of_mem_cycleType hn)).resolve_left
      (one_lt_of_mem_cycleType hn).ne'

Premises used: Nat.Prime.eq_one_or_self_of_dvd, Or.resolve_left, LT.lt.ne', Equiv.Perm.dvd_of_mem_cycleType, Equiv.Perm.one_lt_of_mem_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ σ.cycleType
⊢ n = orderOf σ

Tactic:
exact (hσ.eq_one_or_self_of_dvd n (dvd_of_mem_cycleType hn)).resolve_left
      (one_lt_of_mem_cycleType hn).ne'

Premises used: Nat.Prime.eq_one_or_self_of_dvd, Or.resolve_left, LT.lt.ne', Equiv.Perm.dvd_of_mem_cycleType, Equiv.Perm.one_lt_of_mem_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
rw : (∀ b ∈ σ.cycleType, b ∣ p) ↔ ∀ c ∈ σ.cycleType, c = p
⊢ σ ^ p = 1 ↔ ∀ c ∈ σ.cycleType, c = p

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, ← lcm_cycleType, Multiset.lcm_dvd]

Premises used: Equiv.Perm.lcm_cycleType, Multiset.lcm_dvd, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
h : ∀ (a : ℕ), a ∈ σ.cycleType → a ∣ p ↔ a ∈ σ.cycleType → a = p
⊢ (∀ b ∈ σ.cycleType, b ∣ p) ↔ ∀ c ∈ σ.cycleType, c = p

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
c : ℕ
hc : c ∈ σ.cycleType → c = p
h : c ∈ σ.cycleType
rw rw₁ : p ∣ p
⊢ c ∣ p

Tactic:
rw [hc h]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (a : ℕ), a ∈ σ.cycleType → a ∣ p ↔ a ∈ σ.cycleType → a = p

Tactic:
exact fun c ↦ ⟨fun hc h ↦ Or.resolve_left (hp.elim.eq_one_or_self_of_dvd c (hc h))
       (Nat.ne_of_lt' (one_lt_of_mem_cycleType h)),
     fun hc h ↦ by rw [hc h]⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
p : ℕ
inst_2 : Fact (Nat.Prime p)
hσ : σ ^ p = 1
⊢ σ.cycleType = Multiset.replicate σ.cycleType.card p

Tactic:
Multiset.eq_replicate.mpr ⟨rfl, pow_prime_eq_one_iff.mp hσ⟩

Premises used: Iff.mpr, Multiset.eq_replicate, And.intro, Iff.mp, Equiv.Perm.pow_prime_eq_one_iff, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : #σ.support < 2 * orderOf σ
obtain : ∀ (n : ℕ) (hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)), σ.IsCycle
⊢ σ.IsCycle

Tactic:
obtain ⟨n, hn⟩ := cycleType_prime_order h1

Premises used: Equiv.Perm.cycleType_prime_order
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : #σ.support < 2 * orderOf σ
n : ℕ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
rw : ∀ (n : ℕ) (h2 : n = 0) (hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)), σ.IsCycle
⊢ σ.IsCycle

Tactic:
rw [← σ.sum_cycleType, hn, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id,
    mul_lt_mul_iff_left₀ (orderOf_pos σ), Nat.succ_lt_succ_iff, Nat.lt_succ_iff, Nat.le_zero] at h2

Premises used: Nat.succ_lt_succ_iff, Nat.cast_id, Nat.le_zero, Multiset.sum_replicate, Nat.lt_succ_iff, nsmul_eq_mul, Equiv.Perm.sum_cycleType, orderOf_pos, mul_lt_mul_iff_left₀
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
rw : σ.cycleType.card = 1
rw₁ : (Multiset.replicate (n + 1) (orderOf σ)).card = 1
rw₂ : n + 1 = 1
rw₃ rw₄ : HAdd.hAdd (α := ℕ) 0 1 = 1
⊢ σ.IsCycle

Tactic:
rw [← card_cycleType_eq_one, hn, card_replicate, h2]

Premises used: Multiset.card_replicate, Equiv.Perm.card_cycleType_eq_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
⊢ f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
have hf' := mem_cycleFactorsFinset_iff.1 hf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
rw :
  Multiset.map (α := Perm α) (Finset.card ∘ support) (Finset.val {f}) ≤
    Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val
⊢ f.cycleType ≤ g.cycleType

Tactic:
rw [cycleType_def, cycleType_def, hf'.left.cycleFactorsFinset_eq_singleton]

Premises used: Equiv.Perm.IsCycle.cycleFactorsFinset_eq_singleton, And.left, Equiv.Perm.cycleType_def
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ Multiset.map (α := Perm α) (Finset.card ∘ support) (Finset.val {f}) ≤
    Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val

Tactic:
map_le_map ?_

Premises used: Multiset.map_le_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
refine : Finset.val {f} ≤ g.cycleFactorsFinset.val
⊢ Multiset.map (α := Perm α) (Finset.card ∘ support) (Finset.val {f}) ≤
    Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val

Tactic:
refine map_le_map ?_

Premises used: Multiset.map_le_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ Finset.val {f} ≤ g.cycleFactorsFinset.val

Tactic:
simpa only [Finset.singleton_val, singleton_le, Finset.mem_val] using hf

Premises used: Finset.singleton_val, Multiset.singleton_le, Finset.mem_val
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
⊢ (Finset.noncommProd ∅ k hs').cycleType = ∑ i ∈ ∅, (k i).cycleType

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
⊢ (↑s : Set ι) ⊆ (↑(insert i s) : Set ι)

Tactic:
simp only [Finset.coe_insert, Set.subset_insert]

Premises used: Finset.coe_insert, Set.subset_insert
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
⊢ (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)

Tactic:
have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs'_1 : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
insert : (k i * s.noncommProd k ⋯).cycleType = (k i).cycleType + ∑ x ∈ s, (k x).cycleType
⊢ ((Insert.insert i s).noncommProd k hs'_1).cycleType = ∑ i ∈ Insert.insert i s, (k i).cycleType

Tactic:
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.sum_insert hi]

Premises used: Finset.sum_insert, Finset.noncommProd_insert_of_notMem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs'_1 : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
insert : (k i).Disjoint (s.noncommProd k ⋯)
⊢ (k i * s.noncommProd k ⋯).cycleType = (k i).cycleType + ∑ x ∈ s, (k x).cycleType

Tactic:
rw [Disjoint.cycleType_mul, hrec hs']

Premises used: Equiv.Perm.Disjoint.cycleType_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs'_1 : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
insert : ∀ i_1 ∈ s, (k i).Disjoint (k i_1)
⊢ (k i).Disjoint (s.noncommProd k ⋯)

Tactic:
apply disjoint_noncommProd_right

Premises used: Equiv.Perm.disjoint_noncommProd_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs'_1 : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
apply : i ∈ (↑(insert i s) : Set ι)
apply₁ : j ∈ (↑(insert i s) : Set ι)
⊢ (k i).Disjoint (k j)

Tactic:
apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm

Premises used: Ne.symm, ne_of_mem_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs'_1 : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ i ∈ (↑(insert i s) : Set ι)

Tactic:
simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

Premises used: true_or, Set.mem_insert_iff, Finset.coe_insert, or_true, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs'_1 : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ j ∈ (↑(insert i s) : Set ι)

Tactic:
simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

Premises used: true_or, Set.mem_insert_iff, Finset.coe_insert, or_true, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
empty :
  ∀ (hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (Finset.noncommProd ∅ k hs').cycleType = ∑ i ∈ ∅, (k i).cycleType
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (hrec :
      ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
        (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
        (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType)
    (hs : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    ((Insert.insert i s).noncommProd k hs').cycleType = ∑ i ∈ Insert.insert i s, (k i).cycleType
⊢ (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi hrec =>
    have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.sum_insert hi]
    rw [Disjoint.cycleType_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

Premises used: true_or, Insert.insert, Equiv.Perm.Disjoint.cycleType_mul, Set.mem_insert_iff, Finset.coe_insert, or_true, Equiv.Perm.disjoint_noncommProd_right, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
empty :
  ∀ (hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (Finset.noncommProd ∅ k hs').cycleType = ∑ i ∈ ∅, (k i).cycleType
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (hrec :
      ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
        (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
        (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType)
    (hs : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    ((Insert.insert i s).noncommProd k hs').cycleType = ∑ i ∈ Insert.insert i s, (k i).cycleType
⊢ (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi hrec =>
    have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.sum_insert hi]
    rw [Disjoint.cycleType_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

Premises used: true_or, Insert.insert, Equiv.Perm.Disjoint.cycleType_mul, Set.mem_insert_iff, Finset.coe_insert, or_true, Equiv.Perm.disjoint_noncommProd_right, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ : Perm α
h : cycleType.{u_1} (α := α) 1 = τ.cycleType
⊢ τ = 1

Tactic:
rw [cycleType_one, eq_comm, cycleType_eq_zero] at h

Premises used: eq_comm, Equiv.Perm.cycleType_eq_zero, Equiv.Perm.cycleType_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ : Perm α
h : τ = 1
base_one base_one₁ : IsConj.{u_1} (α := Perm α) 1 1
⊢ IsConj 1 τ

Tactic:
rw [h]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ σ.cycleType.card = 1

Tactic:
have hτ := card_cycleType_eq_one.2 hσ
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : σ.cycleType.card = 1
⊢ τ.IsCycle

Tactic:
rw [h, card_cycleType_eq_one] at hτ

Premises used: Equiv.Perm.card_cycleType_eq_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : τ.IsCycle
base_cycles : #σ.support = #τ.support
⊢ IsConj σ τ

Tactic:
apply hσ.isConj hτ

Premises used: Equiv.Perm.IsCycle.isConj
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : τ.IsCycle
base_cycles : ∀ (h : {#σ.support} = τ.cycleType) (hτ : τ.IsCycle), #σ.support = #τ.support
base_cycles₁ : ∀ (h : Eq (α := Multiset ℕ) {#σ.support} {#τ.support}) (hτ : τ.IsCycle), #σ.support = #τ.support
base_cycles₂ base_cycles₃ base_cycles₄ base_cycles₅ :
  ∀ (h : #σ.support = #τ.support) (hτ : τ.IsCycle), #σ.support = #τ.support
⊢ #σ.support = #τ.support

Tactic:
rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h

Premises used: Multiset.singleton_inj, Equiv.Perm.IsCycle.cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : (σ * π).cycleType = τ.cycleType
⊢ σ.cycleType + π.cycleType = τ.cycleType

Tactic:
rw [hd.cycleType_mul] at h

Premises used: Equiv.Perm.Disjoint.cycleType_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
⊢ #σ.support ∈ τ.cycleType

Tactic:
simp [← h, hc.cycleType]

Premises used: Equiv.Perm.IsCycle.cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
⊢ #σ.support ∈ τ.cycleType

Tactic:
have h' : #σ.support ∈ τ.cycleType := by
      simp [← h, hc.cycleType]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
induction_disjoint :
  ∀ (σ' : Perm α) (hσ'l : σ' ∈ τ.cycleFactorsFinset.val) (hσ' : (Finset.card ∘ support) σ' = #σ.support),
    IsConj (σ * π) τ
⊢ IsConj (σ * π) τ

Tactic:
obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'

Premises used: Multiset.mem_map, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
⊢ IsConj (σ' * τ * σ'⁻¹) τ

Tactic:
have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) τ

Tactic:
IsConj.trans ?_ key

Premises used: IsConj.trans
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
induction_disjoint : IsConj (σ * π) (σ' * τ * σ'⁻¹)
⊢ IsConj (σ * π) τ

Tactic:
refine IsConj.trans ?_ key

Premises used: IsConj.trans