awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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)
⊢ (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
have 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
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]
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
have 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 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)),
  ((insert i s).noncommProd k hs').cycleType = ∑ i ∈ insert 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]
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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)
⊢ (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
have 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
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]
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
have 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 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)),
  ((insert i s).noncommProd k hs').cycleType = ∑ i ∈ insert 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]
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ : Perm α
h : cycleType.{u_1} (α := α) 1 = τ.cycleType
⊢ IsConj 1 τ
have h₁ : τ = 1
Tactic: rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ : Perm α
h : τ = 1
⊢ IsConj 1 τ
have base_one : IsConj.{u_1} (α := Perm α) 1 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ IsConj σ τ
have hτ : σ.cycleType.card = 1
Tactic: have hτ := card_cycleType_eq_one.2 hσ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : σ.cycleType.card = 1
⊢ IsConj σ τ
have hτ₁ : τ.IsCycle
Tactic: rw [h, card_cycleType_eq_one] at hτ
Cleared hypotheses: hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : τ.IsCycle
⊢ IsConj σ τ
have base_cycles : #σ.support = #τ.support
Tactic: apply hσ.isConj hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : τ.IsCycle
⊢ #σ.support = #τ.support
have base_cycles : ∀ (h : {#σ.support} = τ.cycleType) (hτ : τ.IsCycle), #σ.support = #τ.support
Tactic: rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h
Cleared hypotheses: h, hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ #σ.support = #τ.support
have base_cycles₁ : ∀ (h : Eq (α := Multiset ℕ) {#σ.support} {#τ.support}) (hτ : τ.IsCycle), #σ.support = #τ.support
Tactic: rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h
Cleared hypotheses: h, hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ #σ.support = #τ.support
have base_cycles₂ : ∀ (h : #σ.support = #τ.support) (hτ : τ.IsCycle), #σ.support = #τ.support
Tactic: rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h
Cleared hypotheses: h, hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
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
⊢ IsConj (σ * π) τ
have h₁ : σ.cycleType + π.cycleType = τ.cycleType
Tactic: rw [hd.cycleType_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
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
⊢ IsConj (σ * π) τ
have h' : #σ.support ∈ τ.cycleType
Tactic: have h' : #σ.support ∈ τ.cycleType := by
      simp [← h, hc.cycleType]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ IsConj (σ * π) τ
have induction_disjoint : ∀ (σ' : Perm α) (hσ'l : σ' ∈ τ.cycleFactorsFinset.val) (hσ' : (Finset.card ∘ support) σ' = #σ.support), IsConj (σ * π) τ
Tactic: obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
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 (σ * π) τ
have key : IsConj (σ' * τ * σ'⁻¹) τ
Tactic: have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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 (σ * π) τ
have induction_disjoint : IsConj (σ * π) (σ' * τ * σ'⁻¹)
Tactic: refine IsConj.trans ?_ key
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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 (σ * π) (σ' * τ * σ'⁻¹)
have induction_disjoint : IsConj (σ * π) (σ' * (τ * σ'⁻¹))
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
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 (σ' * τ * σ'⁻¹) τ
⊢ σ.cycleType = σ'.cycleType
have hσ'l₁ : σ'.IsCycle ∧ ∀ a ∈ σ'.support, Eq (α := α) ((σ' : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
Tactic: rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
Cleared hypotheses: hσ'l, hσ', key
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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 : σ'.IsCycle ∧ ∀ a ∈ σ'.support, Eq (α := α) ((σ' : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ σ.cycleType = σ'.cycleType
have rw : Eq (α := Multiset ℕ) {(Finset.card ∘ support) σ'} {#σ'.support}
Tactic: rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
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 (σ * π) (σ' * (τ * σ'⁻¹))
have hs : σ.cycleType = σ'.cycleType
Tactic: have hs : σ.cycleType = σ'.cycleType := by
      rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
      rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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 (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))
have induction_disjoint : π.cycleType = (τ * σ'⁻¹).cycleType
Tactic: refine hd.isConj_mul (hσ hs) (hπ ?_) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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 (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
induction_disjoint : π.cycleType = (τ * σ'⁻¹).cycleType
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))
have induction_disjoint₁ : σ'.Disjoint (τ * σ'⁻¹)
Tactic: refine hd.isConj_mul (hσ hs) (hπ ?_) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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 (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ π.cycleType = (τ * σ'⁻¹).cycleType
have induction_disjoint : σ' ∈ τ.cycleFactorsFinset
Tactic: rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs,
        add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ IsConj σ τ
have base_one : ∀ {τ : Perm α} (h : cycleType.{u_1} (α := α) 1 = τ.cycleType), IsConj 1 τ
Tactic: induction σ using cycle_induction_on generalizing τ with
  | base_one =>
    rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
    rw [h]
  | base_cycles σ hσ =>
    have hτ := card_cycleType_eq_one.2 hσ
    rw [h, card_cycleType_eq_one] at hτ
    apply hσ.isConj hτ
    rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h
  | induction_disjoint σ π hd hc hσ hπ =>
    rw [hd.cycleType_mul] at h
    have h' : #σ.support ∈ τ.cycleType := by
      simp [← h, hc.cycleType]
    obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
    have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
    refine IsConj.trans ?_ key
    rw [mul_assoc]
    have hs : σ.cycleType = σ'.cycleType := by
      rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
      rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
    refine hd.isConj_mul (hσ hs) (hπ ?_) ?_
    · rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs,
        add_tsub_cancel_right]
      rwa [Finset.mem_def]
    · exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm
Cleared hypotheses: σ, τ, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
base_one : ∀ {τ : Perm α} (h : cycleType.{u_1} (α := α) 1 = τ.cycleType), IsConj 1 τ
⊢ IsConj σ τ
have base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle) {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
Tactic: induction σ using cycle_induction_on generalizing τ with
  | base_one =>
    rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
    rw [h]
  | base_cycles σ hσ =>
    have hτ := card_cycleType_eq_one.2 hσ
    rw [h, card_cycleType_eq_one] at hτ
    apply hσ.isConj hτ
    rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h
  | induction_disjoint σ π hd hc hσ hπ =>
    rw [hd.cycleType_mul] at h
    have h' : #σ.support ∈ τ.cycleType := by
      simp [← h, hc.cycleType]
    obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
    have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
    refine IsConj.trans ?_ key
    rw [mul_assoc]
    have hs : σ.cycleType = σ'.cycleType := by
      rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
      rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
    refine hd.isConj_mul (hσ hs) (hπ ?_) ?_
    · rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs,
        add_tsub_cancel_right]
      rwa [Finset.mem_def]
    · exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm
Cleared hypotheses: σ, τ, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
base_one : ∀ {τ : Perm α} (h : cycleType.{u_1} (α := α) 1 = τ.cycleType), IsConj 1 τ
base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle) {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
⊢ IsConj σ τ
have induction_disjoint : ∀ (σ π : Perm α) (hd : σ.Disjoint π) (hc : σ.IsCycle) (hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ)
  (hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ) {τ : Perm α} (h : (σ * π).cycleType = τ.cycleType),
  IsConj (σ * π) τ
Tactic: induction σ using cycle_induction_on generalizing τ with
  | base_one =>
    rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
    rw [h]
  | base_cycles σ hσ =>
    have hτ := card_cycleType_eq_one.2 hσ
    rw [h, card_cycleType_eq_one] at hτ
    apply hσ.isConj hτ
    rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h
  | induction_disjoint σ π hd hc hσ hπ =>
    rw [hd.cycleType_mul] at h
    have h' : #σ.support ∈ τ.cycleType := by
      simp [← h, hc.cycleType]
    obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
    have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
    refine IsConj.trans ?_ key
    rw [mul_assoc]
    have hs : σ.cycleType = σ'.cycleType := by
      rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
      rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
    refine hd.isConj_mul (hσ hs) (hπ ?_) ?_
    · rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs,
        add_tsub_cancel_right]
      rwa [Finset.mem_def]
    · exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm
Cleared hypotheses: σ, τ, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : IsConj σ τ
⊢ σ.cycleType = τ.cycleType
have obtain : ∀ (π : Perm α) (h : IsConj σ (π * σ * π⁻¹)), σ.cycleType = (π * σ * π⁻¹).cycleType
Tactic: obtain ⟨π, rfl⟩ := isConj_iff.1 h
Cleared hypotheses: τ, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
h : IsConj σ (π * σ * π⁻¹)
⊢ σ.cycleType = (π * σ * π⁻¹).cycleType
have rw : σ.cycleType = σ.cycleType
Tactic: rw [cycleType_conj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
β : Type u_2
inst_2 : Fintype β
inst_3 : DecidableEq β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
⊢ (extendDomain 1 (p := p) f).cycleType = cycleType.{u_1} (α := α) 1
have base_one : cycleType.{u_2} (α := β) 1 = cycleType.{u_1} (α := α) 1
Tactic: rw [extendDomain_one, cycleType_one, cycleType_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
β : Type u_2
inst_2 : Fintype β
inst_3 : DecidableEq β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
base_one : cycleType.{u_2} (α := β) 1 = cycleType.{u_1} (α := α) 1
⊢ (extendDomain 1 (p := p) f).cycleType = cycleType.{u_1} (α := α) 1
have base_one₁ : 0 = cycleType.{u_1} (α := α) 1
Tactic: rw [extendDomain_one, cycleType_one, cycleType_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
β : Type u_2
inst_2 : Fintype β
inst_3 : DecidableEq β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
base_one : cycleType.{u_2} (α := β) 1 = cycleType.{u_1} (α := α) 1
base_one₁ : 0 = cycleType.{u_1} (α := α) 1
⊢ (extendDomain 1 (p := p) f).cycleType = cycleType.{u_1} (α := α) 1
have base_one₂ : Eq (α := Multiset ℕ) 0 0
Tactic: rw [extendDomain_one, cycleType_one, cycleType_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
β : Type u_2
inst_2 : Fintype β
inst_3 : DecidableEq β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
σ : Perm α
hσ : σ.IsCycle
⊢ (σ.extendDomain (p := p) f).cycleType = σ.cycleType
have base_cycles : {#(σ.extendDomain (p := p) f).support} = σ.cycleType
Tactic: rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]