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
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
base_cycles : {#(σ.extendDomain (p := p) f).support} = σ.cycleType
⊢ (σ.extendDomain (p := p) f).cycleType = σ.cycleType
have base_cycles₁ : Eq (α := Multiset ℕ) {#(σ.extendDomain (p := p) f).support} {#σ.support}
Tactic: rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
-- 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
base_cycles : {#(σ.extendDomain (p := p) f).support} = σ.cycleType
base_cycles₁ : Eq (α := Multiset ℕ) {#(σ.extendDomain (p := p) f).support} {#σ.support}
⊢ (σ.extendDomain (p := p) f).cycleType = σ.cycleType
have base_cycles₂ : Eq (α := Multiset ℕ) {#σ.support} {#σ.support}
Tactic: rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
-- 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 α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : (σ.extendDomain (p := p) f).cycleType = σ.cycleType
hτ : (τ.extendDomain (p := p) f).cycleType = τ.cycleType
⊢ ((σ * τ).extendDomain (p := p) f).cycleType = (σ * τ).cycleType
have induction_disjoint : ((σ * τ).extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
Tactic: rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]
-- 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 α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : (σ.extendDomain (p := p) f).cycleType = σ.cycleType
hτ : (τ.extendDomain (p := p) f).cycleType = τ.cycleType
induction_disjoint : ((σ * τ).extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
⊢ ((σ * τ).extendDomain (p := p) f).cycleType = (σ * τ).cycleType
have induction_disjoint₁ : (σ.extendDomain (p := p) f * τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
Tactic: rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]
-- 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 α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : (σ.extendDomain (p := p) f).cycleType = σ.cycleType
hτ : (τ.extendDomain (p := p) f).cycleType = τ.cycleType
induction_disjoint : ((σ * τ).extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
induction_disjoint₁ : (σ.extendDomain (p := p) f * τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
⊢ ((σ * τ).extendDomain (p := p) f).cycleType = (σ * τ).cycleType
have induction_disjoint₂ : (σ.extendDomain (p := p) f).cycleType + (τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
Tactic: rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]
-- 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 α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : (σ.extendDomain (p := p) f).cycleType = σ.cycleType
hτ : (τ.extendDomain (p := p) f).cycleType = τ.cycleType
induction_disjoint : ((σ * τ).extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
induction_disjoint₁ : (σ.extendDomain (p := p) f * τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
induction_disjoint₂ :
  (σ.extendDomain (p := p) f).cycleType + (τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
⊢ ((σ * τ).extendDomain (p := p) f).cycleType = (σ * τ).cycleType
have induction_disjoint₃ : σ.cycleType + (τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
Tactic: rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]
-- 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 α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : (σ.extendDomain (p := p) f).cycleType = σ.cycleType
hτ : (τ.extendDomain (p := p) f).cycleType = τ.cycleType
induction_disjoint : ((σ * τ).extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
induction_disjoint₁ : (σ.extendDomain (p := p) f * τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
induction_disjoint₂ :
  (σ.extendDomain (p := p) f).cycleType + (τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
induction_disjoint₃ : σ.cycleType + (τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
⊢ ((σ * τ).extendDomain (p := p) f).cycleType = (σ * τ).cycleType
have induction_disjoint₄ : σ.cycleType + τ.cycleType = σ.cycleType + τ.cycleType
Tactic: rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]
-- 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)
g : Perm α
⊢ (g.extendDomain (p := p) f).cycleType = g.cycleType
have base_one : (extendDomain 1 (p := p) f).cycleType = cycleType.{u_1} (α := α) 1
Tactic: induction g using cycle_induction_on with
  | base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
  | base_cycles σ hσ =>
    rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
  | induction_disjoint σ τ hd _ hσ hτ =>
    rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]
Cleared hypotheses: g
-- 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)
g : Perm α
base_one : (extendDomain 1 (p := p) f).cycleType = cycleType.{u_1} (α := α) 1
⊢ (g.extendDomain (p := p) f).cycleType = g.cycleType
have base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), (σ.extendDomain (p := p) f).cycleType = σ.cycleType
Tactic: induction g using cycle_induction_on with
  | base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
  | base_cycles σ hσ =>
    rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
  | induction_disjoint σ τ hd _ hσ hτ =>
    rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]
Cleared hypotheses: g
-- 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)
g : Perm α
base_one : (extendDomain 1 (p := p) f).cycleType = cycleType.{u_1} (α := α) 1
base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), (σ.extendDomain (p := p) f).cycleType = σ.cycleType
⊢ (g.extendDomain (p := p) f).cycleType = g.cycleType
have induction_disjoint : ∀ (σ τ : Perm α) (hd : σ.Disjoint τ),
  σ.IsCycle →
    ∀ (hσ : (σ.extendDomain (p := p) f).cycleType = σ.cycleType)
      (hτ : (τ.extendDomain (p := p) f).cycleType = τ.cycleType),
      ((σ * τ).extendDomain (p := p) f).cycleType = (σ * τ).cycleType
Tactic: induction g using cycle_induction_on with
  | base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
  | base_cycles σ hσ =>
    rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
  | induction_disjoint σ τ hd _ hσ hτ =>
    rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
σ : Perm α
⊢ n ∈ σ.cycleType ↔ ∃ (c : Perm α) (τ : Perm α), σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
have mp : n ∈ σ.cycleType → ∃ (c : Perm α) (τ : Perm α), σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
σ : Perm α
mp : n ∈ σ.cycleType → ∃ (c : Perm α) (τ : Perm α), σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
⊢ n ∈ σ.cycleType ↔ ∃ (c : Perm α) (τ : Perm α), σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
have mpr : (∃ (c : Perm α) (τ : Perm α), σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n) → n ∈ σ.cycleType
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
σ : Perm α
h : n ∈ σ.cycleType
⊢ ∃ (c : Perm α) (τ : Perm α), σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
have mp : ∀ (l : List (Perm α)) (h : n ∈ l.prod.cycleType)
  (x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 })
  (hlc : ∀ g ∈ l, g.IsCycle) (hld : List.Pairwise Disjoint l),
  ∃ (c : Perm α) (τ : Perm α), l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
Tactic: obtain ⟨l, rfl, hlc, hld⟩ := truncCycleFactors σ
Cleared hypotheses: σ, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
l : List (Perm α)
h : n ∈ l.prod.cycleType
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ (c : Perm α) (τ : Perm α), l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
have mp : ∀ (h : ∃ a ∈ l, (Finset.card ∘ support) a = n)
  (x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 })
  (hlc : ∀ g ∈ l, g.IsCycle) (hld : List.Pairwise Disjoint l),
  ∃ (c : Perm α) (τ : Perm α), l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
Tactic: rw [cycleType_eq _ rfl hlc hld, Multiset.mem_coe, List.mem_map] at h
Cleared hypotheses: h, x, hlc, hld
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
l : List (Perm α)
h : ∃ a ∈ l, (Finset.card ∘ support) a = n
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ (c : Perm α) (τ : Perm α), l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
have mp : ∀ (c : Perm α) (cl : c ∈ l),
  ∃ (c_1 : Perm α) (τ : Perm α),
    l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ #c_1.support = (Finset.card ∘ support) c
Tactic: obtain ⟨c, cl, rfl⟩ := h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
c : Perm α
cl : c ∈ l
⊢ ∃ (c_1 : Perm α) (τ : Perm α),
    l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ #c_1.support = (Finset.card ∘ support) c
have hld₁ : List.Pairwise Disjoint (c :: l.erase c)
Tactic: rw [(List.perm_cons_erase cl).pairwise_iff @(Disjoint.symmetric)] at hld
Cleared hypotheses: hld, cl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ ∃ (c_1 : Perm α) (τ : Perm α),
    l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ #c_1.support = (Finset.card ∘ support) c
have mp : l.prod = c * (l.erase c).prod
Tactic: refine ⟨c, (l.erase c).prod, ?_, ?_, hlc _ cl, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
mp : l.prod = c * (l.erase c).prod
⊢ ∃ (c_1 : Perm α) (τ : Perm α),
    l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ #c_1.support = (Finset.card ∘ support) c
have mp₁ : c.Disjoint (l.erase c).prod
Tactic: refine ⟨c, (l.erase c).prod, ?_, ?_, hlc _ cl, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ l.prod = c * (l.erase c).prod
have mp : l.prod = (c :: l.erase c).prod
Tactic: rw [← List.prod_cons, (List.perm_cons_erase cl).symm.prod_eq' (hld.imp Disjoint.commute)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
mp : l.prod = (c :: l.erase c).prod
⊢ l.prod = c * (l.erase c).prod
have mp₁ : l.prod = l.prod
Tactic: rw [← List.prod_cons, (List.perm_cons_erase cl).symm.prod_eq' (hld.imp Disjoint.commute)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
g : Perm α
hn2 : Fintype.card α < n + 2
hng : n ∈ g.cycleType
⊢ g.cycleType = {n}
have obtain : ∀ (c g' : Perm α) (hd : c.Disjoint g') (hc : c.IsCycle) (hn2 : Fintype.card α < #c.support + 2)
  (hng : #c.support ∈ (c * g').cycleType), (c * g').cycleType = {#c.support}
Tactic: obtain ⟨c, g', rfl, hd, hc, rfl⟩ := mem_cycleType_iff.1 hng
Cleared hypotheses: n, g, hn2, hng
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
g'1 : g' = 1
⊢ (c * g').cycleType = {#c.support}
have rw : c.cycleType + g'.cycleType = {#c.support}
Tactic: rw [hd.cycleType_mul, hc.cycleType, g'1, cycleType_one, add_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
g'1 : g' = 1
rw : c.cycleType + g'.cycleType = {#c.support}
⊢ (c * g').cycleType = {#c.support}
have rw₁ : {#c.support} + g'.cycleType = {#c.support}
Tactic: rw [hd.cycleType_mul, hc.cycleType, g'1, cycleType_one, add_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
g'1 : g' = 1
rw : c.cycleType + g'.cycleType = {#c.support}
rw₁ : {#c.support} + g'.cycleType = {#c.support}
⊢ (c * g').cycleType = {#c.support}
have rw₂ : {#c.support} + cycleType.{u_1} (α := α) 1 = {#c.support}
Tactic: rw [hd.cycleType_mul, hc.cycleType, g'1, cycleType_one, add_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
g'1 : g' = 1
rw : c.cycleType + g'.cycleType = {#c.support}
rw₁ : {#c.support} + g'.cycleType = {#c.support}
rw₂ : {#c.support} + cycleType.{u_1} (α := α) 1 = {#c.support}
⊢ (c * g').cycleType = {#c.support}
have rw₃ : HAdd.hAdd (α := Multiset ℕ) {#c.support} 0 = {#c.support}
Tactic: rw [hd.cycleType_mul, hc.cycleType, g'1, cycleType_one, add_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
g'1 : g' = 1
rw : c.cycleType + g'.cycleType = {#c.support}
rw₁ : {#c.support} + g'.cycleType = {#c.support}
rw₂ : {#c.support} + cycleType.{u_1} (α := α) 1 = {#c.support}
rw₃ : HAdd.hAdd (α := Multiset ℕ) {#c.support} 0 = {#c.support}
⊢ (c * g').cycleType = {#c.support}
have rw₄ : Eq (α := Multiset ℕ) {#c.support} {#c.support}
Tactic: rw [hd.cycleType_mul, hc.cycleType, g'1, cycleType_one, add_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
⊢ (c * g').cycleType = {#c.support}
have suffices : g' = 1
Tactic: suffices g'1 : g' = 1 by
    rw [hd.cycleType_mul, hc.cycleType, g'1, cycleType_one, add_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
⊢ g' = 1
have contrapose! : ∀ (g'1 : g' ≠ 1), #c.support + 2 ≤ Fintype.card α
Tactic: contrapose! hn2 with g'1
Cleared hypotheses: hn2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hng : #c.support ∈ (c * g').cycleType
g'1 : g' ≠ 1
⊢ #c.support + 2 ≤ Fintype.card α
have grw : #c.support + 2 ≤ #(c * g').support
Tactic: grw [← (c * g').support.card_le_univ, hd.card_support_mul, two_le_card_support_of_ne_one g'1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hng : #c.support ∈ (c * g').cycleType
g'1 : g' ≠ 1
grw : #c.support + 2 ≤ #(c * g').support
⊢ #c.support + 2 ≤ Fintype.card α
have grw₁ : #c.support + 2 ≤ #c.support + #g'.support
Tactic: grw [← (c * g').support.card_le_univ, hd.card_support_mul, two_le_card_support_of_ne_one g'1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hng : #c.support ∈ (c * g').cycleType
g'1 : g' ≠ 1
grw : #c.support + 2 ≤ #(c * g').support
grw₁ : #c.support + 2 ≤ #c.support + #g'.support
⊢ #c.support + 2 ≤ Fintype.card α
have grw₂ : #c.support + #g'.support ≤ #c.support + #g'.support
Tactic: grw [← (c * g').support.card_le_univ, hd.card_support_mul, two_le_card_support_of_ne_one g'1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have rw : (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
  if Odd n then 1
  else
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
Tactic: rw [sign_of_cycleType', hσ, Multiset.map_replicate, Multiset.prod_replicate]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inl : ∀ (h : Even n),
  (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
Tactic: obtain h | h := Nat.even_or_odd n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
inl :
  ∀ (h : Even n),
    (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
      if Odd n then 1
      else
        HPow.hPow (α := ℤˣ) (-1)
          ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inr : ∀ (h : Odd n),
  (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
Tactic: obtain h | h := Nat.even_or_odd n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ σ.cycleType.sum = σ.cycleType.card * n
have rw : (Multiset.replicate σ.cycleType.card n).sum = (Multiset.replicate σ.cycleType.card n).card * n
Tactic: rw [hσ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inl : (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
  HPow.hPow (α := ℤˣ) (-1)
    ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
Tactic: rw [if_neg (Nat.not_odd_iff_even.mpr h), h.neg_one_pow, σ.card_fixedPoints,
      Nat.sub_sub_self σ.sum_cycleType_le,
      show σ.cycleType.sum = σ.cycleType.card * n by rw [hσ]; simp,
        Nat.mul_div_cancel _ hn]