awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : (f : (a : α) → α) b = b
pos : ∀ (h : b = a), a = b
⊢ (if b = a then a else if b = a then (f : (a : α) → α) a else b) = b
have neg : ∀ (h : ¬b = a), b = b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
f : Equiv.Perm α
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure {σ : Equiv.Perm α | σ.IsSwap}) f ↔ (fixedBy α f)ᶜ.Finite
have refine : ∀ (x : α),
  Membership.mem (γ := Subgroup (Equiv.Perm α))
    (closure fun (x : Equiv.Perm α) ↦ ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ x = swap x_1 y) (swap x ((f : (a : α) → α) x))
Tactic: refine (mem_closure_isSwap fun _ ↦ id).trans
    (and_iff_left fun x ↦ ⟨⟨swap x (f x), ?_⟩, swap_apply_left x (f x)⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
f : Equiv.Perm α
x : α
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α))
    (closure fun (x : Equiv.Perm α) ↦ ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ x = swap x_1 y) (swap x ((f : (a : α) → α) x))
have pos : ∀ (h : x = (f : (a : α) → α) x),
  Membership.mem (γ := Subgroup (Equiv.Perm α))
    (closure fun (x : Equiv.Perm α) ↦ ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ x = swap x_1 y) (swap x ((f : (a : α) → α) x))
Tactic: by_cases h : x = f x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
f : Equiv.Perm α
x : α
pos :
  ∀ (h : x = (f : (a : α) → α) x),
    Membership.mem (γ := Subgroup (Equiv.Perm α))
      (closure fun (x : Equiv.Perm α) ↦ ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ x = swap x_1 y) (swap x ((f : (a : α) → α) x))
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α))
    (closure fun (x : Equiv.Perm α) ↦ ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ x = swap x_1 y) (swap x ((f : (a : α) → α) x))
have neg : ∀ (h : ¬x = (f : (a : α) → α) x),
  Membership.mem (γ := Subgroup (Equiv.Perm α))
    (closure fun (x : Equiv.Perm α) ↦ ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ x = swap x_1 y) (swap x ((f : (a : α) → α) x))
Tactic: by_cases h : x = f x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
f : Equiv.Perm α
x : α
h : x = (f : (a : α) → α) x
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α))
    (closure fun (x : Equiv.Perm α) ↦ ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ x = swap x_1 y) (swap x ((f : (a : α) → α) x))
have pos : Membership.mem (γ := Subgroup (Equiv.Perm α))
  (closure fun (x : Equiv.Perm α) ↦ ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ x = swap x_1 y) (Equiv.refl α)
Tactic: rw [← h, swap_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Finite α
S : Set G
hS1 :
  ∀ σ ∈ S,
    Eq.{u_2 + 1} (α := Equiv.Perm α)
        (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ : Equiv.Perm α)
        (1 : Equiv.Perm α) ∨
      Perm.IsSwap.{u_2} (α := α) (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ)
hS2 : Eq (α := Subgroup G) (closure S) ⊤
h : IsPretransitive G α
⊢ closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}) = MonoidHom.range (toPermHom G α)
have rw : closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S) = MonoidHom.range (toPermHom G α)
Tactic: rw [closure_diff_one, ← MonoidHom.map_closure, hS2, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Finite α
S : Set G
hS1 :
  ∀ σ ∈ S,
    Eq.{u_2 + 1} (α := Equiv.Perm α)
        (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ : Equiv.Perm α)
        (1 : Equiv.Perm α) ∨
      Perm.IsSwap.{u_2} (α := α) (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ)
hS2 : Eq (α := Subgroup G) (closure S) ⊤
h : IsPretransitive G α
rw : closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S) = MonoidHom.range (toPermHom G α)
⊢ closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}) = MonoidHom.range (toPermHom G α)
have rw₁ : Subgroup.map (toPermHom G α) (closure S) = MonoidHom.range (toPermHom G α)
Tactic: rw [closure_diff_one, ← MonoidHom.map_closure, hS2, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Finite α
S : Set G
hS1 :
  ∀ σ ∈ S,
    Eq.{u_2 + 1} (α := Equiv.Perm α)
        (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ : Equiv.Perm α)
        (1 : Equiv.Perm α) ∨
      Perm.IsSwap.{u_2} (α := α) (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ)
hS2 : Eq (α := Subgroup G) (closure S) ⊤
h : IsPretransitive G α
rw : closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S) = MonoidHom.range (toPermHom G α)
rw₁ : Subgroup.map (toPermHom G α) (closure S) = MonoidHom.range (toPermHom G α)
⊢ closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}) = MonoidHom.range (toPermHom G α)
have rw₂ : Subgroup.map (toPermHom G α) ⊤ = MonoidHom.range (toPermHom G α)
Tactic: rw [closure_diff_one, ← MonoidHom.map_closure, hS2, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Finite α
S : Set G
hS1 :
  ∀ σ ∈ S,
    Eq.{u_2 + 1} (α := Equiv.Perm α)
        (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ : Equiv.Perm α)
        (1 : Equiv.Perm α) ∨
      Perm.IsSwap.{u_2} (α := α) (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ)
hS2 : Eq (α := Subgroup G) (closure S) ⊤
h : IsPretransitive G α
rw : closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S) = MonoidHom.range (toPermHom G α)
rw₁ : Subgroup.map (toPermHom G α) (closure S) = MonoidHom.range (toPermHom G α)
rw₂ : Subgroup.map (toPermHom G α) ⊤ = MonoidHom.range (toPermHom G α)
⊢ closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}) = MonoidHom.range (toPermHom G α)
have rw₃ : MonoidHom.range (toPermHom G α) = MonoidHom.range (toPermHom G α)
Tactic: rw [closure_diff_one, ← MonoidHom.map_closure, hS2, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Finite α
S : Set G
hS1 :
  ∀ σ ∈ S,
    Eq.{u_2 + 1} (α := Equiv.Perm α)
        (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ : Equiv.Perm α)
        (1 : Equiv.Perm α) ∨
      Perm.IsSwap.{u_2} (α := α) (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ)
hS2 : Eq (α := Subgroup G) (closure S) ⊤
h : IsPretransitive G α
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := Equiv.Perm α) (⇑(toPermHom G α) : (a : G) → Equiv.Perm α)
have h₁ : closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}) = MonoidHom.range (toPermHom G α)
Tactic: have h : closure ((toPermHom G α '' S) \ {1}) = (toPermHom G α).range := by
    rw [closure_diff_one, ← MonoidHom.map_closure, hS2, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Finite α
S : Set G
hS1 :
  ∀ σ ∈ S,
    Eq.{u_2 + 1} (α := Equiv.Perm α)
        (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ : Equiv.Perm α)
        (1 : Equiv.Perm α) ∨
      Perm.IsSwap.{u_2} (α := α) (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ)
hS2 : Eq (α := Subgroup G) (closure S) ⊤
h_1 : IsPretransitive G α
h : closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}) = MonoidHom.range (toPermHom G α)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := Equiv.Perm α) (⇑(toPermHom G α) : (a : G) → Equiv.Perm α)
have this : IsPretransitive (↥(MonoidHom.range (toPermHom G α))) α
Tactic: have := IsPretransitive.of_compHom (α := α) (toPermHom G α).rangeRestrict
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Finite α
S : Set G
hS1 :
  ∀ σ ∈ S,
    Eq.{u_2 + 1} (α := Equiv.Perm α)
        (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ : Equiv.Perm α)
        (1 : Equiv.Perm α) ∨
      Perm.IsSwap.{u_2} (α := α) (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ)
hS2 : Eq (α := Subgroup G) (closure S) ⊤
h_1 : IsPretransitive G α
h : closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}) = MonoidHom.range (toPermHom G α)
this : IsPretransitive (↥(MonoidHom.range (toPermHom G α))) α
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := Equiv.Perm α) (⇑(toPermHom G α) : (a : G) → Equiv.Perm α)
have this₁ : IsPretransitive (↥(closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}))) α
Tactic: rw [← h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Finite α
S : Set G
hS1 :
  ∀ σ ∈ S,
    Eq.{u_2 + 1} (α := Equiv.Perm α)
        (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ : Equiv.Perm α)
        (1 : Equiv.Perm α) ∨
      Perm.IsSwap.{u_2} (α := α) (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ)
hS2 : Eq (α := Subgroup G) (closure S) ⊤
h_1 : IsPretransitive G α
h : closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}) = MonoidHom.range (toPermHom G α)
this : IsPretransitive (↥(closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}))) α
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := Equiv.Perm α) (⇑(toPermHom G α) : (a : G) → Equiv.Perm α)
have hS : ∀ (σ : Equiv.Perm α),
  Membership.mem (γ := Set (Equiv.Perm α)) ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}) σ → σ.IsSwap
Tactic: rw [← MonoidHom.range_eq_top, ← h, closure_of_isSwap_of_isPretransitive]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ a ∈ (k • g).support ↔
    Membership.mem (α := α) g.support
      ((((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k⁻¹ : Perm α) : (a : α) → α) a : α)
have simp : (((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) : (a : α) → α)
      ((g : (a : α) → α)
          (((((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k)⁻¹ : Perm α) : (a : α) → α) a : α) :
        α) =
    a ↔
  Eq (α := α)
    ((g : (a : α) → α) (((((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k)⁻¹ : Perm α) : (a : α) → α) a : α) :
      α)
    (((((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k)⁻¹ : Perm α) : (a : α) → α) a : α)
Tactic: simp only [mem_support, ConjAct.smul_def, not_iff_not, coe_mul,
    Function.comp_apply, ConjAct.ofConjAct_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g : Perm α
⊢ (k • g).support =
    HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
have h : ∀ (a : α),
  a ∈ (k • g).support ↔
    a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ a ∈ (k • g).support ↔
    a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
have h : Membership.mem (α := α) g.support
    ((((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k⁻¹ : Perm α) : (a : α) → α) a : α) ↔
  a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
Tactic: rw [mem_conj_support, ← Perm.smul_def, ConjAct.ofConjAct_inv, Finset.inv_smul_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
h :
  Membership.mem (α := α) g.support
      ((((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k⁻¹ : Perm α) : (a : α) → α) a : α) ↔
    a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
⊢ a ∈ (k • g).support ↔
    a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
have h₁ : HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k⁻¹ : Perm α) a ∈ g.support ↔
  a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
Tactic: rw [mem_conj_support, ← Perm.smul_def, ConjAct.ofConjAct_inv, Finset.inv_smul_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
h :
  Membership.mem (α := α) g.support
      ((((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k⁻¹ : Perm α) : (a : α) → α) a : α) ↔
    a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
h₁ :
  HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k⁻¹ : Perm α) a ∈ g.support ↔
    a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
⊢ a ∈ (k • g).support ↔
    a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
have h₂ : HSMul.hSMul (α := Perm α) (((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k)⁻¹ : Perm α) a ∈ g.support ↔
  a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
Tactic: rw [mem_conj_support, ← Perm.smul_def, ConjAct.ofConjAct_inv, Finset.inv_smul_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
h :
  Membership.mem (α := α) g.support
      ((((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k⁻¹ : Perm α) : (a : α) → α) a : α) ↔
    a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
h₁ :
  HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k⁻¹ : Perm α) a ∈ g.support ↔
    a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
h₂ :
  HSMul.hSMul (α := Perm α) (((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k)⁻¹ : Perm α) a ∈ g.support ↔
    a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
⊢ a ∈ (k • g).support ↔
    a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
have h₃ : a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support ↔
  a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
Tactic: rw [mem_conj_support, ← Perm.smul_def, ConjAct.ofConjAct_inv, Finset.inv_smul_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k g : Perm α
⊢ (HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
        g).support =
    k • g.support
have rw : HSMul.hSMul (α := Perm α)
    ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α)
        ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α)) :
      Perm α)
    g.support =
  k • g.support
Tactic: rw [Equiv.Perm.support_conj_eq_smul_support, ConjAct.ofConjAct_toConjAct]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k g : Perm α
rw :
  HSMul.hSMul (α := Perm α)
      ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α)
          ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α)) :
        Perm α)
      g.support =
    k • g.support
⊢ (HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
        g).support =
    k • g.support
have rw₁ : k • g.support = k • g.support
Tactic: rw [Equiv.Perm.support_conj_eq_smul_support, ConjAct.ofConjAct_toConjAct]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k : Perm α
⊢ (HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
        g).cycleFactorsFinset =
    Finset.map (Equiv.toEmbedding (MulEquiv.toEquiv ((MulAut.conj : (a : Perm α) → MulAut (Perm α)) k)))
      g.cycleFactorsFinset
have h : ∀ (c : Perm α),
  c ∈
      (HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
          g).cycleFactorsFinset ↔
    Membership.mem (γ := Finset (Perm α))
      (Finset.map (Equiv.toEmbedding (MulEquiv.toEquiv ((MulAut.conj : (a : Perm α) → MulAut (Perm α)) k)))
        g.cycleFactorsFinset)
      c
Tactic: ext c
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
⊢ c ∈
      (HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
          g).cycleFactorsFinset ↔
    Membership.mem (γ := Finset (Perm α))
      (Finset.map (Equiv.toEmbedding (MulEquiv.toEquiv ((MulAut.conj : (a : Perm α) → MulAut (Perm α)) k)))
        g.cycleFactorsFinset)
      c
have h : c ∈ (k * g * k⁻¹).cycleFactorsFinset ↔
  HMul.hMul (β := Perm α) k
        ((Equiv.symm (MulEquiv.toEquiv ((MulAut.conj : (a : Perm α) → MulAut (Perm α)) k)) : (a : Perm α) → Perm α) c :
          Perm α) *
      k⁻¹ ∈
    (k * g * k⁻¹).cycleFactorsFinset
Tactic: rw [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct, Finset.mem_map_equiv,
    ← mem_cycleFactorsFinset_conj g k]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g : Perm α
⊢ (k • g).cycleFactorsFinset = k • g.cycleFactorsFinset
have h : ∀ (c : Perm α), c ∈ (k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset
Tactic: ext c
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ c ∈ (k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset
have h : k⁻¹ • c ∈ (k⁻¹ • k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset
Tactic: rw [← mem_cycleFactorsFinset_conj' k⁻¹ (k • g) c]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ (k⁻¹ • k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset
have h : k⁻¹ • c ∈ g.cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset
Tactic: simp only [inv_smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
g : Perm α
s : Finset α
⊢ HSMul.hSMul (α := ConjAct (Perm α)) (β := Subgroup (Perm α))
      ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g : ConjAct (Perm α))
      (MonoidHom.range (G := Perm ↥s) (ofSubtype (p := fun (x : α) ↦ x ∈ s))) =
    MonoidHom.range (G := Perm ↥(g • s)) (ofSubtype (p := fun (x : α) ↦ x ∈ g • s))
have have : ∀ (this : Fintype α),
  HSMul.hSMul (α := ConjAct (Perm α)) (β := Subgroup (Perm α))
      ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g : ConjAct (Perm α))
      (MonoidHom.range (G := Perm ↥s) (ofSubtype (p := fun (x : α) ↦ x ∈ s))) =
    MonoidHom.range (G := Perm ↥(g • s)) (ofSubtype (p := fun (x : α) ↦ x ∈ g • s))
Tactic: have : Fintype α := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
g : Perm α
s : Finset α
this : Fintype α
⊢ HSMul.hSMul (α := ConjAct (Perm α)) (β := Subgroup (Perm α))
      ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g : ConjAct (Perm α))
      (MonoidHom.range (G := Perm ↥s) (ofSubtype (p := fun (x : α) ↦ x ∈ s))) =
    MonoidHom.range (G := Perm ↥(g • s)) (ofSubtype (p := fun (x : α) ↦ x ∈ g • s))
have h : ∀ (k : Perm α),
  k ∈
      HSMul.hSMul (α := ConjAct (Perm α)) (β := Subgroup (Perm α))
        ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g : ConjAct (Perm α))
        (MonoidHom.range (G := Perm ↥s) (ofSubtype (p := fun (x : α) ↦ x ∈ s))) ↔
    Membership.mem (γ := Subgroup (Perm α))
      (MonoidHom.range (G := Perm ↥(g • s)) (ofSubtype (p := fun (x : α) ↦ x ∈ g • s))) k
Tactic: ext k
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ConjAct (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
g : Perm α
s : Finset α
this : Fintype α
k : Perm α
⊢ k ∈
      HSMul.hSMul (α := ConjAct (Perm α)) (β := Subgroup (Perm α))
        ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g : ConjAct (Perm α))
        (MonoidHom.range (G := Perm ↥s) (ofSubtype (p := fun (x : α) ↦ x ∈ s))) ↔
    Membership.mem (γ := Subgroup (Perm α))
      (MonoidHom.range (G := Perm ↥(g • s)) (ofSubtype (p := fun (x : α) ↦ x ∈ g • s))) k
have h : (↑(HSMul.hSMul (α := ConjAct (Perm α)) (((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g)⁻¹ : ConjAct (Perm α))
            k).support :
      Set α) ⊆
    {x : α | x ∈ s} ↔
  (↑k.support : Set α) ⊆ {x : α | x ∈ g • s}
Tactic: simp_rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, mem_range_ofSubtype_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
x y : α
h : x = y
f : Perm α
⊢ f.SameCycle x y
have rw : f.SameCycle y y
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y z : α
h : f.SameCycle x y
h_1 : f.SameCycle y z
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
j : ℤ
hj : (f ^ j : (a : α) → α) y = z
⊢ (f ^ (j + i) : (a : α) → α) x = z
have rw : (f ^ j * f ^ i : (a : α) → α) x = z
Tactic: rw [zpow_add, mul_apply, hi, hj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y z : α
h : f.SameCycle x y
h_1 : f.SameCycle y z
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
j : ℤ
hj : (f ^ j : (a : α) → α) y = z
rw : (f ^ j * f ^ i : (a : α) → α) x = z
⊢ (f ^ (j + i) : (a : α) → α) x = z
have rw₁ : (f ^ j : (a : α) → α) ((f ^ i : (a : α) → α) x : α) = z
Tactic: rw [zpow_add, mul_apply, hi, hj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y z : α
h : f.SameCycle x y
h_1 : f.SameCycle y z
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
j : ℤ
hj : (f ^ j : (a : α) → α) y = z
rw : (f ^ j * f ^ i : (a : α) → α) x = z
rw₁ : (f ^ j : (a : α) → α) ((f ^ i : (a : α) → α) x : α) = z
rw₂ : (f ^ j : (a : α) → α) y = z
⊢ (f ^ (j + i) : (a : α) → α) x = z
have rw₃ : z = z
Tactic: rw [zpow_add, mul_apply, hi, hj]