awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.map (Function.comp (β := Perm α) (Finset.card ∘ support) fun (l : List α) ↦ l.formPerm) p = m.toList
have h : List.map (Function.comp (β := Perm α) (Finset.card ∘ support) fun (l : List α) ↦ l.formPerm) p = List.map List.length p
Tactic: rw [← hp_length]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.map (Function.comp (β := Perm α) (Finset.card ∘ support) fun (l : List α) ↦ l.formPerm) p =
    List.map List.length p
have h : ∀ a ∈ p, Function.comp (β := Perm α) (Finset.card ∘ support) (fun (l : List α) ↦ l.formPerm) a = a.length
Tactic: apply List.map_congr_left
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ Function.comp (β := Perm α) (Finset.card ∘ support) (fun (l : List α) ↦ l.formPerm) x = x.length
have h : x.formPerm.support.card = x.length
Tactic: simp only [Function.comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ x.formPerm.support.card = x.length
have h : x.toFinset.card = x.length
Tactic: rw [List.support_formPerm_of_nodup x (hp_nodup x hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
h : x.toFinset.card = x.length
⊢ x.formPerm.support.card = x.length
have h₁ : ∀ (x_1 : α), x ≠ [x_1]
Tactic: rw [List.support_formPerm_of_nodup x (hp_nodup x hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ x.toFinset.card = x.length
have h : x.length = x.length
Tactic: rw [List.toFinset_card_of_nodup (hp_nodup x hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.Pairwise (α := Perm α) Disjoint (List.map (fun (l : List α) ↦ l.formPerm) p)
have h : List.Pairwise (fun (a b : List α) ↦ a.formPerm.Disjoint b.formPerm) p
Tactic: rw [List.pairwise_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.Pairwise (fun (a b : List α) ↦ a.formPerm.Disjoint b.formPerm) p
have apply : ∀ {a b : List α}, a ∈ p → b ∈ p → a.Disjoint b → a.formPerm.Disjoint b.formPerm
Tactic: apply List.Pairwise.imp_of_mem _ hp_disj
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s : Set (Perm α)).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val = Multiset.map (Finset.card ∘ support) s.val
have e_s : σ.cycleFactorsFinset = s
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s : Set (Perm α)).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ σ.cycleFactorsFinset = s
have e_s : (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s : Set (Perm α)).Pairwise Disjoint), s.noncommProd id sorry = σ
Tactic: rw [cycleFactorsFinset_eq_finset]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
⊢ σ.cycleType = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)
have hl : l.Nodup
Tactic: have hl : l.Nodup := nodup_of_pairwise_disjoint_cycles h1 h2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ σ.cycleType = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)
have rw : Multiset.map (Finset.card ∘ support) l.toFinset.val = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)
Tactic: rw [cycleType_eq' l.toFinset]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
rw : Multiset.map (Finset.card ∘ support) l.toFinset.val = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)
⊢ σ.cycleType = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)
have h1₁ : ∀ f ∈ l.toFinset, f.IsCycle
Tactic: rw [cycleType_eq' l.toFinset]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
rw : Multiset.map (Finset.card ∘ support) l.toFinset.val = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)
h1₁ : ∀ f ∈ l.toFinset, f.IsCycle
⊢ σ.cycleType = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)
have h2₁ : (↑l.toFinset : Set (Perm α)).Pairwise Disjoint
Tactic: rw [cycleType_eq' l.toFinset]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
rw : Multiset.map (Finset.card ∘ support) l.toFinset.val = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)
h1₁ : ∀ f ∈ l.toFinset, f.IsCycle
h2₁ : (↑l.toFinset : Set (Perm α)).Pairwise Disjoint
⊢ σ.cycleType = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)
have h0₁ : l.toFinset.noncommProd id sorry = σ
Tactic: rw [cycleType_eq' l.toFinset]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
⊢ Multiset.count n σ.cycleType = Fintype.card.{u_1} { c : ↥σ.cycleFactorsFinset // #(↑c : Perm α).support = n }
have rw : (Multiset.filter (fun (x : ℕ) ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
  Fintype.card.{u_1} { c : ↥σ.cycleFactorsFinset // #(↑c : Perm α).support = n }
Tactic: rw [cycleType, Multiset.count_eq_card_filter_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun (x : ℕ) ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    Fintype.card.{u_1} { c : ↥σ.cycleFactorsFinset // #(↑c : Perm α).support = n }
have rw : (Multiset.filter (fun (x : ℕ) ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
  #({x ∈ σ.cycleFactorsFinset |
      ∃ (h : x ∈ σ.cycleFactorsFinset),
        #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ σ.cycleFactorsFinset) x h) : Perm α).support = n})
Tactic: rw [Fintype.subtype_card, Finset.univ_eq_attach, Finset.filter_attach',
    Finset.card_map, Finset.card_attach]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun (x : ℕ) ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    #({x ∈ σ.cycleFactorsFinset |
        ∃ (h : x ∈ σ.cycleFactorsFinset),
          #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ σ.cycleFactorsFinset) x h) : Perm α).support = n})
have simp : (Multiset.filter (fun (x : Perm α) ↦ n = x.support.val.card) σ.cycleFactorsFinset.val).card =
  (Multiset.filter (fun (x : Perm α) ↦ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n)
      σ.cycleFactorsFinset.val).card
Tactic: simp only [Function.comp_apply, Finset.card, Finset.filter_val,
    Multiset.filter_map, Multiset.card_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun (x : Perm α) ↦ n = x.support.val.card) σ.cycleFactorsFinset.val).card =
    (Multiset.filter (fun (x : Perm α) ↦ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n)
        σ.cycleFactorsFinset.val).card
have e_a : Multiset.filter (fun (x : Perm α) ↦ n = x.support.val.card) σ.cycleFactorsFinset.val =
  Multiset.filter (fun (x : Perm α) ↦ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n) σ.cycleFactorsFinset.val
Tactic: congr 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
⊢ Multiset.filter (fun (x : Perm α) ↦ n = x.support.val.card) σ.cycleFactorsFinset.val =
    Multiset.filter (fun (x : Perm α) ↦ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n)
      σ.cycleFactorsFinset.val
have e_a : ∀ x ∈ σ.cycleFactorsFinset.val, n = x.support.val.card ↔ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n
Tactic: apply Multiset.filter_congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ σ.cycleType.card = 0 ↔ σ = 1
have rw : σ.cycleType = 0 ↔ σ = 1
Tactic: rw [card_eq_zero, cycleType_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : σ.cycleType = 0 ↔ σ = 1
⊢ σ.cycleType.card = 0 ↔ σ = 1
have rw₁ : σ = 1 ↔ σ = 1
Tactic: rw [card_eq_zero, cycleType_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ 2 ≤ n
have h₁ : ∃ (a : Perm α),
  (a.IsCycle ∧ ∀ a_1 ∈ a.support, Eq (α := α) ((a : (a : α) → α) a_1 : α) ((σ : (a : α) → α) a_1 : α)) ∧ #a.support = n
Tactic: simp only [cycleType_def, ← Finset.mem_def, Function.comp_apply, Multiset.mem_map,
    mem_cycleFactorsFinset_iff] 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 α
n : ℕ
h :
  ∃ (a : Perm α),
    (a.IsCycle ∧ ∀ a_1 ∈ a.support, Eq (α := α) ((a : (a : α) → α) a_1 : α) ((σ : (a : α) → α) a_1 : α)) ∧
      #a.support = n
⊢ 2 ≤ n
have obtain : ∀ (w : Perm α) (hc : w.IsCycle), 2 ≤ #w.support
Tactic: obtain ⟨_, ⟨hc, -⟩, rfl⟩ := h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ σ.cycleType.card = 1 ↔ σ.IsCycle
have rw : (∃ (a : ℕ), σ.cycleType = {a}) ↔ σ.IsCycle
Tactic: rw [card_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ (∃ (a : ℕ), σ.cycleType = {a}) ↔ σ.IsCycle
have simp_rw : (∃ (a : ℕ) (a_1 : Perm α), (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) ↔ σ.IsCycle
Tactic: simp_rw [cycleType_def, Multiset.map_eq_singleton, ← Finset.singleton_val, Finset.val_inj,
    cycleFactorsFinset_eq_singleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
⊢ (σ * τ).cycleType = σ.cycleType + τ.cycleType
have rw : _root_.Disjoint σ.cycleFactorsFinset.val τ.cycleFactorsFinset.val
Tactic: rw [cycleType_def, cycleType_def, cycleType_def, h.cycleFactorsFinset_mul_eq_union, ←
    Multiset.map_add, Finset.union_val, Multiset.add_eq_union_iff_disjoint.mpr _]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ σ : Perm α
hσ : σ.IsCycle
⊢ (τ * σ * τ⁻¹).cycleType = σ.cycleType
have base_cycles : (τ * σ * τ⁻¹).cycleType = {#σ.support}
Tactic: rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ σ : Perm α
hσ : σ.IsCycle
base_cycles : (τ * σ * τ⁻¹).cycleType = {#σ.support}
⊢ (τ * σ * τ⁻¹).cycleType = σ.cycleType
have base_cycles₁ : Eq (α := Multiset ℕ) {#(τ * σ * τ⁻¹).support} {#σ.support}
Tactic: rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ σ : Perm α
hσ : σ.IsCycle
base_cycles : (τ * σ * τ⁻¹).cycleType = {#σ.support}
base_cycles₁ : Eq (α := Multiset ℕ) {#(τ * σ * τ⁻¹).support} {#σ.support}
⊢ (τ * σ * τ⁻¹).cycleType = σ.cycleType
have base_cycles₂ : Eq (α := Multiset ℕ) {#σ.support} {#σ.support}
Tactic: rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ σ π : Perm α
hd : σ.Disjoint π
h : σ.IsCycle
hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType
hπ : (τ * π * τ⁻¹).cycleType = π.cycleType
⊢ (τ * (σ * π) * τ⁻¹).cycleType = (σ * π).cycleType
have induction_disjoint : (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = (σ * π).cycleType
Tactic: rw [← conj_mul, hd.cycleType_mul, (hd.conj _).cycleType_mul, hσ, hπ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ σ π : Perm α
hd : σ.Disjoint π
h : σ.IsCycle
hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType
hπ : (τ * π * τ⁻¹).cycleType = π.cycleType
induction_disjoint : (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = (σ * π).cycleType
⊢ (τ * (σ * π) * τ⁻¹).cycleType = (σ * π).cycleType
have induction_disjoint₁ : (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = σ.cycleType + π.cycleType
Tactic: rw [← conj_mul, hd.cycleType_mul, (hd.conj _).cycleType_mul, hσ, hπ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ σ π : Perm α
hd : σ.Disjoint π
h : σ.IsCycle
hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType
hπ : (τ * π * τ⁻¹).cycleType = π.cycleType
induction_disjoint : (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = (σ * π).cycleType
induction_disjoint₁ : (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = σ.cycleType + π.cycleType
⊢ (τ * (σ * π) * τ⁻¹).cycleType = (σ * π).cycleType
have induction_disjoint₂ : (τ * σ * τ⁻¹).cycleType + (τ * π * τ⁻¹).cycleType = σ.cycleType + π.cycleType
Tactic: rw [← conj_mul, hd.cycleType_mul, (hd.conj _).cycleType_mul, hσ, hπ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ σ π : Perm α
hd : σ.Disjoint π
h : σ.IsCycle
hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType
hπ : (τ * π * τ⁻¹).cycleType = π.cycleType
induction_disjoint : (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = (σ * π).cycleType
induction_disjoint₁ : (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = σ.cycleType + π.cycleType
induction_disjoint₂ : (τ * σ * τ⁻¹).cycleType + (τ * π * τ⁻¹).cycleType = σ.cycleType + π.cycleType
⊢ (τ * (σ * π) * τ⁻¹).cycleType = (σ * π).cycleType
have induction_disjoint₃ : σ.cycleType + (τ * π * τ⁻¹).cycleType = σ.cycleType + π.cycleType
Tactic: rw [← conj_mul, hd.cycleType_mul, (hd.conj _).cycleType_mul, hσ, hπ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ σ π : Perm α
hd : σ.Disjoint π
h : σ.IsCycle
hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType
hπ : (τ * π * τ⁻¹).cycleType = π.cycleType
induction_disjoint : (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = (σ * π).cycleType
induction_disjoint₁ : (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = σ.cycleType + π.cycleType
induction_disjoint₂ : (τ * σ * τ⁻¹).cycleType + (τ * π * τ⁻¹).cycleType = σ.cycleType + π.cycleType
induction_disjoint₃ : σ.cycleType + (τ * π * τ⁻¹).cycleType = σ.cycleType + π.cycleType
⊢ (τ * (σ * π) * τ⁻¹).cycleType = (σ * π).cycleType
have induction_disjoint₄ : σ.cycleType + π.cycleType = σ.cycleType + π.cycleType
Tactic: rw [← conj_mul, hd.cycleType_mul, (hd.conj _).cycleType_mul, hσ, hπ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
⊢ (τ * σ * τ⁻¹).cycleType = σ.cycleType
have base_one : (τ * 1 * τ⁻¹).cycleType = cycleType.{u_1} (α := α) 1
Tactic: induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
  | induction_disjoint σ π hd _ hσ hπ =>
    rw [← conj_mul, hd.cycleType_mul, (hd.conj _).cycleType_mul, hσ, hπ]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
base_one : (τ * 1 * τ⁻¹).cycleType = cycleType.{u_1} (α := α) 1
⊢ (τ * σ * τ⁻¹).cycleType = σ.cycleType
have base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), (τ * σ * τ⁻¹).cycleType = σ.cycleType
Tactic: induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
  | induction_disjoint σ π hd _ hσ hπ =>
    rw [← conj_mul, hd.cycleType_mul, (hd.conj _).cycleType_mul, hσ, hπ]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
base_one : (τ * 1 * τ⁻¹).cycleType = cycleType.{u_1} (α := α) 1
base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), (τ * σ * τ⁻¹).cycleType = σ.cycleType
⊢ (τ * σ * τ⁻¹).cycleType = σ.cycleType
have induction_disjoint : ∀ (σ π : Perm α) (hd : σ.Disjoint π),
  σ.IsCycle →
    ∀ (hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType) (hπ : (τ * π * τ⁻¹).cycleType = π.cycleType),
      (τ * (σ * π) * τ⁻¹).cycleType = (σ * π).cycleType
Tactic: induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
  | induction_disjoint σ π hd _ hσ hπ =>
    rw [← conj_mul, hd.cycleType_mul, (hd.conj _).cycleType_mul, hσ, hπ]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
⊢ σ.cycleType.sum = #σ.support
have base_cycles : Multiset.sum {#σ.support} = #σ.support
Tactic: rw [hσ.cycleType, Multiset.sum_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
base_cycles : Multiset.sum {#σ.support} = #σ.support
⊢ σ.cycleType.sum = #σ.support
have base_cycles₁ : #σ.support = #σ.support
Tactic: rw [hσ.cycleType, Multiset.sum_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : σ.cycleType.sum = #σ.support
hτ : τ.cycleType.sum = #τ.support
⊢ (σ * τ).cycleType.sum = #(σ * τ).support
have induction_disjoint : (σ.cycleType + τ.cycleType).sum = #(σ * τ).support
Tactic: rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : σ.cycleType.sum = #σ.support
hτ : τ.cycleType.sum = #τ.support
induction_disjoint : (σ.cycleType + τ.cycleType).sum = #(σ * τ).support
⊢ (σ * τ).cycleType.sum = #(σ * τ).support
have induction_disjoint₁ : σ.cycleType.sum + τ.cycleType.sum = #(σ * τ).support
Tactic: rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : σ.cycleType.sum = #σ.support
hτ : τ.cycleType.sum = #τ.support
induction_disjoint : (σ.cycleType + τ.cycleType).sum = #(σ * τ).support
induction_disjoint₁ : σ.cycleType.sum + τ.cycleType.sum = #(σ * τ).support
⊢ (σ * τ).cycleType.sum = #(σ * τ).support
have induction_disjoint₂ : #σ.support + τ.cycleType.sum = #(σ * τ).support
Tactic: rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : σ.cycleType.sum = #σ.support
hτ : τ.cycleType.sum = #τ.support
induction_disjoint : (σ.cycleType + τ.cycleType).sum = #(σ * τ).support
induction_disjoint₁ : σ.cycleType.sum + τ.cycleType.sum = #(σ * τ).support
induction_disjoint₂ : #σ.support + τ.cycleType.sum = #(σ * τ).support
⊢ (σ * τ).cycleType.sum = #(σ * τ).support
have induction_disjoint₃ : #σ.support + #τ.support = #(σ * τ).support
Tactic: rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : σ.cycleType.sum = #σ.support
hτ : τ.cycleType.sum = #τ.support
induction_disjoint : (σ.cycleType + τ.cycleType).sum = #(σ * τ).support
induction_disjoint₁ : σ.cycleType.sum + τ.cycleType.sum = #(σ * τ).support
induction_disjoint₂ : #σ.support + τ.cycleType.sum = #(σ * τ).support
induction_disjoint₃ : #σ.support + #τ.support = #(σ * τ).support
⊢ (σ * τ).cycleType.sum = #(σ * τ).support
have induction_disjoint₄ : #σ.support + #τ.support = #σ.support + #τ.support
Tactic: rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ σ.cycleType.sum = #σ.support
have base_one : (cycleType.{u_1} (α := α) 1).sum = Finset.card.{u_1} (α := α) (support 1)
Tactic: induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, Multiset.sum_singleton]
  | induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]
Cleared hypotheses: σ