awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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
⊢ b = a

Tactic:
simpa [hb] using supp_subset hb'
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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
⊢ (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b

Tactic:
simp [show b = a by simpa [hb] using supp_subset hb']
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
f : Equiv.Perm α
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure {σ : Equiv.Perm α | σ.IsSwap}) f ↔ (fixedBy α f)ᶜ.Finite

Tactic:
(mem_closure_isSwap fun _ ↦ id).trans
    (and_iff_left fun x ↦ ⟨⟨swap x (f x), ?_⟩, swap_apply_left x (f x)⟩)

Premises used: Set.Mem, Equiv.swap, setOf, and_iff_left, mem_closure_isSwap, Equiv.Perm.IsSwap, id, Subtype.mk, Exists.intro, Iff.trans, DFunLike.coe, Equiv.swap_apply_left
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
f : Equiv.Perm α
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))
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure {σ : Equiv.Perm α | σ.IsSwap}) f ↔ (fixedBy α f)ᶜ.Finite

Tactic:
refine (mem_closure_isSwap fun _ ↦ id).trans
    (and_iff_left fun x ↦ ⟨⟨swap x (f x), ?_⟩, swap_apply_left x (f x)⟩)

Premises used: Equiv.swap, and_iff_left, mem_closure_isSwap, id, Subtype.mk, Exists.intro, Iff.trans, DFunLike.coe, Equiv.swap_apply_left
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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))
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))
⊢ 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

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
f : Equiv.Perm α
x : α
h : x = (f : (a : α) → α) x
pos :
  Membership.mem (γ := Subgroup (Equiv.Perm α))
    (closure fun (x : Equiv.Perm α) ↦ ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ x = swap x_1 y) (Equiv.refl α)
⊢ 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:
rw [← h, swap_self]

Premises used: Equiv.swap_self
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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) (Equiv.refl α)

Tactic:
apply Subgroup.one_mem

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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))

Tactic:
subset_closure ⟨x, f x, h, rfl⟩

Premises used: Subgroup.subset_closure, And.intro, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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))

Tactic:
exact subset_closure ⟨x, f x, h, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Finite α
S : Set (Equiv.Perm α)
hS : ∀ σ ∈ S, σ.IsSwap
inst_2 : IsPretransitive (↥(closure S)) α
⊢ Eq (α := Subgroup (Equiv.Perm α)) (closure S) ⊤

Tactic:
simp [eq_top_iff', mem_closure_isSwap hS, orbit_eq_univ, Set.toFinite]

Premises used: mem_closure_isSwap, Subgroup.eq_top_iff', Set.toFinite, MulAction.orbit_eq_univ
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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 α)
rw₃ rw₄ : MonoidHom.range (toPermHom G α) = MonoidHom.range (toPermHom G α)
⊢ closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}) = MonoidHom.range (toPermHom G α)

Tactic:
rw [closure_diff_one, ← MonoidHom.map_closure, hS2, ← MonoidHom.range_eq_map]

Premises used: MonoidHom.range_eq_map, MonoidHom.map_closure, Subgroup.closure_diff_one
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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 α)

Tactic:
have h : closure ((toPermHom G α '' S) \ {1}) = (toPermHom G α).range := by
    rw [closure_diff_one, ← MonoidHom.map_closure, hS2, ← MonoidHom.range_eq_map]
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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 α)
⊢ IsPretransitive (↥(MonoidHom.range (toPermHom G α))) α

Tactic:
have := IsPretransitive.of_compHom (α := α) (toPermHom G α).rangeRestrict
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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 α))) α
⊢ IsPretransitive (↥(closure ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}))) α

Tactic:
rw [← h] at this
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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}))) α
hS :
  ∀ (σ : Equiv.Perm α),
    Membership.mem (γ := Set (Equiv.Perm α)) ((⇑(toPermHom G α) : (a : G) → Equiv.Perm α) '' S \ {1}) σ → σ.IsSwap
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := Equiv.Perm α) (⇑(toPermHom G α) : (a : G) → Equiv.Perm α)

Tactic:
rw [← MonoidHom.range_eq_top, ← h, closure_of_isSwap_of_isPretransitive]

Premises used: MonoidHom.range_eq_top, closure_of_isSwap_of_isPretransitive
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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}))) α
σ : G
hσ : σ ∈ S
hσ1 : (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ : Equiv.Perm α) ∉ {1}
⊢ Perm.IsSwap.{u_2} (α := α) (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ)

Tactic:
(hS1 σ hσ).resolve_left hσ1

Premises used: Or.resolve_left
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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}))) α
σ : G
hσ : σ ∈ S
hσ1 : (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ : Equiv.Perm α) ∉ {1}
⊢ Perm.IsSwap.{u_2} (α := α) (((toPermHom G α : MonoidHom.{u_1, u_2} G (Equiv.Perm α)) : (a : G) → Equiv.Perm α) σ)

Tactic:
exact (hS1 σ hσ).resolve_left hσ1

Premises used: Or.resolve_left
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
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,
    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 α)

Tactic:
surjective_of_isSwap_of_isPretransitive' S (fun σ hσ ↦ Or.inr (hS1 σ hσ)) hS2

Premises used: surjective_of_isSwap_of_isPretransitive', Or.inr
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
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 : α)
⊢ a ∈ (k • g).support ↔
    Membership.mem (α := α) g.support
      ((((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]

Premises used: ConjAct.smul_def, not_iff_not, Equiv.Perm.coe_mul, Equiv.Perm.mem_support, Function.comp_apply, ConjAct.ofConjAct_inv
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (((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:
apply Equiv.apply_eq_iff_eq_symm_apply

Premises used: Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g : Perm α
h :
  ∀ (a : α),
    a ∈ (k • g).support ↔
      a ∈ HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support
⊢ (k • g).support =
    HSMul.hSMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g.support

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.ConjAct
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
h₃ 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
⊢ a ∈ (k • 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]

Premises used: Finset.inv_smul_mem_iff, Equiv.Perm.smul_def, ConjAct.ofConjAct_inv, Equiv.Perm.mem_conj_support
-- Module: Mathlib.GroupTheory.Perm.ConjAct
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
rw₁ rw₂ : k • g.support = k • g.support
⊢ (HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
        g).support =
    k • g.support

Tactic:
rw [Equiv.Perm.support_conj_eq_smul_support, ConjAct.ofConjAct_toConjAct]

Premises used: Equiv.Perm.support_conj_eq_smul_support, ConjAct.ofConjAct_toConjAct
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k : Perm α
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
⊢ (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

Tactic:
ext c
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
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
⊢ 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:
rw [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct, Finset.mem_map_equiv,
    ← mem_cycleFactorsFinset_conj g k]

Premises used: ConjAct.smul_def, Equiv.Perm.mem_cycleFactorsFinset_conj, Finset.mem_map_equiv, ConjAct.ofConjAct_toConjAct
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
⊢ 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:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ HMul.hMul (β := Perm α) (HMul.hMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) c)
        (((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k)⁻¹ : Perm α) ∈
      (HMul.hMul (β := Perm α)
          (HMul.hMul (α := Perm α) ((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k : Perm α) g)
          (((ConjAct.ofConjAct : (a : ConjAct (Perm α)) → Perm α) k)⁻¹ : Perm α)).cycleFactorsFinset ↔
    c ∈ g.cycleFactorsFinset

Tactic:
apply mem_cycleFactorsFinset_conj g k

Premises used: Equiv.Perm.mem_cycleFactorsFinset_conj
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g : Perm α
h : ∀ (c : Perm α), c ∈ (k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset
⊢ (k • g).cycleFactorsFinset = k • g.cycleFactorsFinset

Tactic:
ext c
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g c : Perm α
h : k⁻¹ • c ∈ (k⁻¹ • k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset
⊢ c ∈ (k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Tactic:
rw [← mem_cycleFactorsFinset_conj' k⁻¹ (k • g) c]

Premises used: Equiv.Perm.mem_cycleFactorsFinset_conj', Inv.inv, HSMul.hSMul
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g c : Perm α
h : k⁻¹ • c ∈ g.cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset
⊢ k⁻¹ • c ∈ (k⁻¹ • k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Tactic:
simp only [inv_smul_smul]

Premises used: inv_smul_smul
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ g.cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Tactic:
Finset.inv_smul_mem_iff

Premises used: Finset.inv_smul_mem_iff, Set.Mem, setOf
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ g.cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Tactic:
exact Finset.inv_smul_mem_iff

Premises used: Finset.inv_smul_mem_iff
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
g : Perm α
s : Finset α
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))
⊢ 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 α
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
g : Perm α
s : Finset α
this : Fintype α
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
⊢ 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:
ext k