awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
h :
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} { h : Perm α // IsConj g h }
h₁ :
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₂ : Fintype.card.{u_1} ↥{g_1 : Perm α | g_1.cycleType = g.cycleType} = Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₃ :
  Fintype.card.{u_1} { x : Perm α // Membership.mem (γ := Finset (Perm α)) Finset.univ x ∧ x.cycleType = g.cycleType } =
    Fintype.card.{u_1} { h : Perm α // IsConj g h }
⊢ Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1)
have h₄ : Fintype.card.{u_1} { x : Perm α // True ∧ x.cycleType = g.cycleType } = Fintype.card.{u_1} { h : Perm α // IsConj g h }
Tactic: simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
      Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
h :
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} { h : Perm α // IsConj g h }
h₁ :
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₂ : Fintype.card.{u_1} ↥{g_1 : Perm α | g_1.cycleType = g.cycleType} = Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₃ :
  Fintype.card.{u_1} { x : Perm α // Membership.mem (γ := Finset (Perm α)) Finset.univ x ∧ x.cycleType = g.cycleType } =
    Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₄ :
  Fintype.card.{u_1} { x : Perm α // True ∧ x.cycleType = g.cycleType } =
    Fintype.card.{u_1} { h : Perm α // IsConj g h }
⊢ Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1)
have h₅ : Fintype.card.{u_1} { x : Perm α // x.cycleType = g.cycleType } = Fintype.card.{u_1} { h : Perm α // IsConj g h }
Tactic: simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
      Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
h :
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} { h : Perm α // IsConj g h }
h₁ :
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₂ : Fintype.card.{u_1} ↥{g_1 : Perm α | g_1.cycleType = g.cycleType} = Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₃ :
  Fintype.card.{u_1} { x : Perm α // Membership.mem (γ := Finset (Perm α)) Finset.univ x ∧ x.cycleType = g.cycleType } =
    Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₄ :
  Fintype.card.{u_1} { x : Perm α // True ∧ x.cycleType = g.cycleType } =
    Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₅ : Fintype.card.{u_1} { x : Perm α // x.cycleType = g.cycleType } = Fintype.card.{u_1} { h : Perm α // IsConj g h }
⊢ Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1)
have h₆ : Fintype.card.{u_1} { x : Perm α // IsConj x g } = Fintype.card.{u_1} { h : Perm α // IsConj g h }
Tactic: simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
      Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    (Fintype.card α)!
have pos : ∀ (g : Perm α) (hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a),
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
Tactic: classical
    obtain ⟨g, rfl⟩ := (exists_with_cycleType_iff α).mpr hm
    convert! card_isConj_mul_eq g
    simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
      Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
pos :
  ∀ (g : Perm α) (hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a),
    Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} *
        ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
          ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
      (Fintype.card α)!
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    (Fintype.card α)!
have h : ∀ (g : Perm α) (hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a),
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1)
Tactic: classical
    obtain ⟨g, rfl⟩ := (exists_with_cycleType_iff α).mpr hm
    convert! card_isConj_mul_eq g
    simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
      Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    0
have neg : 0 * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) = 0
Tactic: rw [(card_of_cycleType_eq_zero_iff α).mpr hm, zero_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
neg : 0 * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) = 0
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    0
have neg₁ : Eq (α := ℕ) 0 0
Tactic: rw [(card_of_cycleType_eq_zero_iff α).mpr hm, zero_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} =
    if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0
have pos : ∀ (hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a),
  Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
pos :
  ∀ (hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a),
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} =
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} =
    if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0
have neg : ∀ (hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)), Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} = 0
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
have pos : (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
  Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m}
Tactic: apply symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m}
have pos : 0 < (Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!
Tactic: apply Nat.div_eq_of_eq_mul_left
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
pos : 0 < (Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!
⊢ (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m}
have pos₁ : (Fintype.card α)! =
  Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
    ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
Tactic: apply Nat.div_eq_of_eq_mul_left
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ 0 < (Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!
have this : 0 < m.prod
Tactic: have : 0 < m.prod := Multiset.prod_pos <| fun a ha => zero_lt_two.trans_le (hm.2 a ha)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (Fintype.card α)! =
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
have pos : (Fintype.card α)! = if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0
Tactic: rw [card_of_cycleType_mul_eq, if_pos hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
pos : (Fintype.card α)! = if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0
⊢ (Fintype.card α)! =
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
have pos₁ : (Fintype.card α)! = (Fintype.card α)!
Tactic: rw [card_of_cycleType_mul_eq, if_pos hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} = (n - 1)! * (card α).choose n
have hn₀ : n ≠ 0
Tactic: have hn₀ : n ≠ 0 := by lia
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
⊢ n ! = (n - 1)! * n
have rw : n ! = n * (n - 1)!
Tactic: rw [mul_comm, mul_factorial_pred hn₀]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
rw : n ! = n * (n - 1)!
⊢ n ! = (n - 1)! * n
have rw₁ : n ! = n !
Tactic: rw [mul_comm, mul_factorial_pred hn₀]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} = (n - 1)! * (card α).choose n
have aux : n ! = (n - 1)! * n
Tactic: have aux : n ! = (n - 1)! * n := by rw [mul_comm, mul_factorial_pred hn₀]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} = (n - 1)! * (card α).choose n
have rw : Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} * (n * (card α - n)!) = (card α)!
Tactic: rw [mul_comm, ← Nat.mul_left_inj hn₀, mul_assoc, ← aux, ← Nat.mul_left_inj (factorial_ne_zero _),
    Nat.choose_mul_factorial_mul_factorial hα, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
β : Type u_3
inst : Finite β
⊢ Eq.{u_3 + 1} (α := Subgroup (Perm β)) (closure {σ : Perm β | σ.IsCycle}) ⊤
have intro : ∀ (val : Fintype β), Eq.{u_3 + 1} (α := Subgroup (Perm β)) (closure {σ : Perm β | σ.IsCycle}) ⊤
Tactic: cases nonempty_fintype β
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
β : Type u_3
inst : Finite β
⊢ Eq.{u_3 + 1} (α := Subgroup (Perm β)) (closure {σ : Perm β | σ.IsCycle}) ⊤
have intro : ∀ (val : Fintype β), Eq.{u_3 + 1} (α := Subgroup (Perm β)) (closure {σ : Perm β | σ.IsCycle}) ⊤
Tactic: classical
    cases nonempty_fintype β
    exact
      top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ : (a : α) → α) x)}) ⊤
have h3 : σ ∈ H
Tactic: have h3 : σ ∈ H := subset_closure (Set.mem_insert σ _)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ : (a : α) → α) x)}) ⊤
have h4 : swap x ((σ : (a : α) → α) x) ∈ H
Tactic: have h4 : swap x (σ x) ∈ H := subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
n : ℕ
ih : Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
⊢ Membership.mem (α := Perm α) H (swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) : Perm α)
have h : swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
  HMul.hMul (β := Perm α) σ (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α) * σ⁻¹
Tactic: convert! H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
n : ℕ
ih : Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
⊢ swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
    HMul.hMul (β := Perm α) σ (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α) * σ⁻¹
have h : swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
  HMul.hMul (α := Perm α)
      (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α)) ((σ : (a : α) → α) ((σ ^ (n + 1) : (a : α) → α) x : α)) :
        Perm α)
      σ *
    σ⁻¹
Tactic: simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ', coe_mul, comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
n : ℕ
ih : Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
h :
  swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
    HMul.hMul (α := Perm α)
        (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α))
            ((σ : (a : α) → α) ((σ ^ (n + 1) : (a : α) → α) x : α)) :
          Perm α)
        σ *
      σ⁻¹
⊢ swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
    HMul.hMul (β := Perm α) σ (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α) * σ⁻¹
have h₁ : Eq (α := Perm α) (swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) : Perm α)
  (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α)) ((σ : (a : α) → α) ((σ ^ (n + 1) : (a : α) → α) x : α)) :
    Perm α)
Tactic: simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ', coe_mul, comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
n : ℕ
ih : Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
h :
  swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
    HMul.hMul (α := Perm α)
        (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α))
            ((σ : (a : α) → α) ((σ ^ (n + 1) : (a : α) → α) x : α)) :
          Perm α)
        σ *
      σ⁻¹
h₁ :
  Eq (α := Perm α) (swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) : Perm α)
    (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α)) ((σ : (a : α) → α) ((σ ^ (n + 1) : (a : α) → α) x : α)) :
      Perm α)
⊢ swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
    HMul.hMul (β := Perm α) σ (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α) * σ⁻¹
have h₂ : Eq (α := Perm α) (swap ((σ * σ ^ n : (a : α) → α) x) ((σ * (σ * σ ^ n) : (a : α) → α) x) : Perm α)
  (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α)) ((σ : (a : α) → α) ((σ * σ ^ n : (a : α) → α) x : α)) :
    Perm α)
Tactic: simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ', coe_mul, comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
n : ℕ
ih : Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
h :
  swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
    HMul.hMul (α := Perm α)
        (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α))
            ((σ : (a : α) → α) ((σ ^ (n + 1) : (a : α) → α) x : α)) :
          Perm α)
        σ *
      σ⁻¹
h₁ :
  Eq (α := Perm α) (swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) : Perm α)
    (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α)) ((σ : (a : α) → α) ((σ ^ (n + 1) : (a : α) → α) x : α)) :
      Perm α)
h₂ :
  Eq (α := Perm α) (swap ((σ * σ ^ n : (a : α) → α) x) ((σ * (σ * σ ^ n) : (a : α) → α) x) : Perm α)
    (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α)) ((σ : (a : α) → α) ((σ * σ ^ n : (a : α) → α) x : α)) :
      Perm α)
⊢ swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
    HMul.hMul (β := Perm α) σ (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α) * σ⁻¹
have h₃ : Eq (α := Perm α)
  (swap (comp (β := α) (⇑σ : (a : α) → α) (⇑(σ ^ n) : (a : α) → α) x)
      (comp (β := α) (⇑σ : (a : α) → α) (comp (β := α) (⇑σ : (a : α) → α) (⇑(σ ^ n) : (a : α) → α)) x) :
    Perm α)
  (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α))
      ((σ : (a : α) → α) (comp (β := α) (⇑σ : (a : α) → α) (⇑(σ ^ n) : (a : α) → α) x)) :
    Perm α)
Tactic: simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ', coe_mul, comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
n : ℕ
⊢ Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
have zero : Membership.mem (α := Perm α) H
  (swap ((HPow.hPow (β := ℕ) σ 0 : (a : α) → α) x) ((σ ^ HAdd.hAdd (α := ℕ) 0 1 : (a : α) → α) x) : Perm α)
Tactic: induction n with
    | zero => exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
    | succ n ih =>
      convert! H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)
      simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ', coe_mul, comp_apply]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
n : ℕ
zero :
  Membership.mem (α := Perm α) H
    (swap ((HPow.hPow (β := ℕ) σ 0 : (a : α) → α) x) ((σ ^ HAdd.hAdd (α := ℕ) 0 1 : (a : α) → α) x) : Perm α)
⊢ Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
have succ : ∀ (n : ℕ)
  (ih : Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)),
  Membership.mem (α := Perm α) H (swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) : Perm α)
Tactic: induction n with
    | zero => exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
    | succ n ih =>
      convert! H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)
      simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ', coe_mul, comp_apply]
Cleared hypotheses: n