awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
g : G
yh : (fun (m : G) ↦ m • a) g ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
h : G
zh : (fun (m : G) ↦ m • a) h ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
⊢ (↑((h * g⁻¹) •
          Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
            ((fun (m : G) ↦ m • a) g) yh) :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
          ((fun (m : G) ↦ m • a) h) zh) :
      α)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Finite G
inst_3 : Finite.{u_2 + 1} Ω
rw : Finite.{u_2 + 1} ((ω : Ω) × (↑ω.orbit : Type u_2))
⊢ Finite α

Tactic:
rw [(selfEquivSigmaOrbits' G _).finite_iff]

Premises used: Equiv.finite_iff, MulAction.selfEquivSigmaOrbits'
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Finite G
inst_3 : Finite.{u_2 + 1} Ω
g : Ω
h : ∀ (a : α), Finite.{u_2 + 1} (↑(orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) : Type u_2)
⊢ Finite.{u_2 + 1} (↑g.orbit : Type u_2)

Tactic:
induction g using Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Finite G
inst_3 : Finite.{u_2 + 1} Ω
a : α
⊢ Finite.{u_2 + 1} (↑(orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) : Type u_2)

Tactic:
simpa [Set.finite_coe_iff] using Finite.finite_mulAction_orbit _

Premises used: Finite.finite_mulAction_orbit, Set.finite_coe_iff
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Finite G
inst_3 : Finite.{u_2 + 1} Ω
⊢ ∀ (g : Ω), Finite.{u_2 + 1} (↑g.orbit : Type u_2)

Tactic:
have : ∀ g : Ω, Finite g.orbit := by
    intro g
    induction g using Quotient.inductionOn'
    simpa [Set.finite_coe_iff] using Finite.finite_mulAction_orbit _
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Finite G
inst_3 : Finite.{u_2 + 1} Ω
this : ∀ (g : Ω), Finite.{u_2 + 1} (↑g.orbit : Type u_2)
⊢ Finite.{u_2 + 1} ((ω : Ω) × (↑ω.orbit : Type u_2))

Tactic:
Finite.instSigma

Premises used: Finite.instSigma
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Finite G
inst_3 : Finite.{u_2 + 1} Ω
this : ∀ (g : Ω), Finite.{u_2 + 1} (↑g.orbit : Type u_2)
⊢ Finite.{u_2 + 1} ((ω : Ω) × (↑ω.orbit : Type u_2))

Tactic:
exact Finite.instSigma

Premises used: Finite.instSigma
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
⊢ LE.le (α := Setoid (α × β)) (orbitRel G (α × β)) (Setoid.comap Prod.fst (orbitRel G α))

Tactic:
Setoid.le_def.2 fst_mem_orbit_of_mem_orbit

Premises used: Iff.mpr, MulAction.fst_mem_orbit_of_mem_orbit, Setoid.le_def
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
⊢ LE.le (α := Setoid (α × β)) (orbitRel G (α × β)) (Setoid.comap Prod.snd (orbitRel G β))

Tactic:
Setoid.le_def.2 snd_mem_orbit_of_mem_orbit

Premises used: Iff.mpr, MulAction.snd_mem_orbit_of_mem_orbit, Setoid.le_def
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : IsCancelSMul G α
a : α
⊢ Eq (α := Subgroup G) (stabilizer G a) ⊥

Tactic:
Subgroup.eq_bot_iff_forall _ |>.mpr fun _ hg ↦ IsCancelSMul.eq_one_of_smul hg

Premises used: Iff.mpr, Subgroup.eq_bot_iff_forall, IsCancelSMul.eq_one_of_smul
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
⊢ IsCancelSMul G α ↔ ∀ (a : α), Eq (α := Subgroup G) (stabilizer G a) ⊥

Tactic:
simp [isCancelSMul_iff_eq_one_of_smul_eq, Subgroup.eq_bot_iff_forall, forall_comm (α := G)]

Premises used: forall_comm, Subgroup.eq_bot_iff_forall, isCancelSMul_iff_eq_one_of_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h :
  ∀ (h : G),
    Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
      Membership.mem (γ := Subgroup G)
        (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
⊢ Eq (α := Subgroup G) (stabilizer G (g • a))
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a))

Tactic:
ext h
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : G
h₁ :
  h • g • a = g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₂ :
  g⁻¹ • h • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₃ :
  (g⁻¹ * h) • g • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₄ :
  (g⁻¹ * h * g) • a = g⁻¹ • g • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₅ :
  (g⁻¹ * h * g) • a = (g⁻¹ * g) • a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₆ :
  (g⁻¹ * h * g) • a = HSMul.hSMul.{u_1, u_2, u_2} (α := G) 1 a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₇ :
  (g⁻¹ * h * g) • a = a ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₈ :
  Membership.mem (γ := Subgroup G) (stabilizer G a) (g⁻¹ * h * g) ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h
h₉ :
  Membership.mem (γ := Subgroup G) (stabilizer G a) (g⁻¹ * h * g) ↔
    Membership.mem (α := G) (γ := Subgroup G) (stabilizer G a)
      ((MulEquiv.symm ((MulAut.conj : (a : G) → MulAut G) g) : (a : G) → G) h : G)
h₁₀ h₁₁ :
  Membership.mem (γ := Subgroup G) (stabilizer G a) (g⁻¹ * h * g) ↔
    Membership.mem (γ := Subgroup G) (stabilizer G a) (g⁻¹ * h * g)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (g • a)) h ↔
    Membership.mem (γ := Subgroup G)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a)) h

Tactic:
rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]

Premises used: inv_mul_cancel, Subgroup.mem_map_equiv, smul_smul, one_smul, Inv.inv, MulAut.conj_symm_apply, MulAction.mem_stabilizer_iff, smul_left_cancel_iff
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
g h k : G
a b c : α
hg : b = g • a
rw :
  Eq (α := Subgroup G) (Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) (stabilizer G a))
    (stabilizer G (g • a))
rw₁ :
  Eq (α := Subgroup G) (Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) (stabilizer G a))
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a))
rw₂ rw₃ :
  Eq (α := Subgroup G) (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a))
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) (stabilizer G a))
⊢ Eq (α := Subgroup G) (Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) (stabilizer G a))
    (stabilizer G b)

Tactic:
rw [hg, stabilizer_smul_eq_stabilizer_map_conj g a, ← MulEquiv.toMonoidHom_eq_coe]

Premises used: MulEquiv.toMonoidHom_eq_coe, MulAction.stabilizer_smul_eq_stabilizer_map_conj
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(stabilizer G a)
⊢ Eq (α := G) ((↑((stabilizerEquivStabilizer hg : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G) : G)
    ((((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) (↑x : G) : G)

Tactic:
simp [stabilizerEquivStabilizer]

Premises used: MulAction.stabilizerEquivStabilizer
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(stabilizer G b)
⊢ Eq (α := G) ((↑(((stabilizerEquivStabilizer hg).symm : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G) : G)
    ((((MulAut.conj : (a : G) → MulAut G) g⁻¹ : MulAut G) : (a : G) → G) (↑x : G) : G)

Tactic:
simp [stabilizerEquivStabilizer]

Premises used: MulAction.stabilizerEquivStabilizer
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
h₁ :
  ∀ (x : ↥(stabilizer G a)),
    Eq.{u_1 + 1} (α := G)
      (↑(((stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) :
              (a : ↥(stabilizer G a)) → ↥(stabilizer G c))
            x) :
        G)
      (↑((stabilizerEquivStabilizer hk : (a : ↥(stabilizer G a)) → ↥(stabilizer G c)) x) : G)
⊢ (stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = stabilizerEquivStabilizer hk

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
x : ↥(stabilizer G a)
⊢ Eq.{u_1 + 1} (α := G)
    (↑(((stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) :
            (a : ↥(stabilizer G a)) → ↥(stabilizer G c))
          x) :
      G)
    (↑((stabilizerEquivStabilizer hk : (a : ↥(stabilizer G a)) → ↥(stabilizer G c)) x) : G)

Tactic:
simp [stabilizerEquivStabilizer_apply, H]

Premises used: MulAction.stabilizerEquivStabilizer_apply
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
h :
  ∀ (x : ↥(stabilizer G a)),
    Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer ⋯ : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)
      (↑((MulEquiv.refl ↥(stabilizer G a) : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)
⊢ Eq (α := ↥(stabilizer G a) ≃* ↥(stabilizer G a)) (stabilizerEquivStabilizer ⋯) (MulEquiv.refl ↥(stabilizer G a))

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
x : ↥(stabilizer G a)
⊢ Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer ⋯ : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)
    (↑((MulEquiv.refl ↥(stabilizer G a) : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)

Tactic:
simp [stabilizerEquivStabilizer_apply]

Premises used: MulAction.stabilizerEquivStabilizer_apply
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
h :
  ∀ (x : ↥(stabilizer G b)),
    Eq.{u_1 + 1} (α := G)
      (↑(((stabilizerEquivStabilizer hg).symm : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)
      (↑((stabilizerEquivStabilizer ⋯ : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)
⊢ (stabilizerEquivStabilizer hg).symm = stabilizerEquivStabilizer ⋯

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(stabilizer G b)
⊢ Eq.{u_1 + 1} (α := G) (↑(((stabilizerEquivStabilizer hg).symm : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)
    (↑((stabilizerEquivStabilizer ⋯ : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)

Tactic:
simp [stabilizerEquivStabilizer]

Premises used: MulAction.stabilizerEquivStabilizer
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
hg : b = g⁻¹ • a
h :
  ∀ (x : ↥(stabilizer G a)),
    Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer hg : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)
      (↑(((stabilizerEquivStabilizer ⋯).symm : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)
⊢ stabilizerEquivStabilizer hg = (stabilizerEquivStabilizer ⋯).symm

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
hg : b = g⁻¹ • a
x : ↥(stabilizer G a)
⊢ Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer hg : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)
    (↑(((stabilizerEquivStabilizer ⋯).symm : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)

Tactic:
simp [stabilizerEquivStabilizer]

Premises used: MulAction.stabilizerEquivStabilizer
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a : α
h :
  ∀ (h : G),
    Membership.mem (γ := AddSubgroup G) (stabilizer G (g +ᵥ a)) h ↔
      Membership.mem (γ := AddSubgroup G)
        (AddSubgroup.map
          (AddEquiv.toAddMonoidHom
            ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
          (stabilizer G a))
        h
⊢ Eq (α := AddSubgroup G) (stabilizer G (g +ᵥ a))
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))

Tactic:
ext h
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g_1 h_1 k_1 : G
a_1 b_1 c_1 : α
g h k : G
a b c : α
hg : b = g +ᵥ a
rw :
  Eq (α := AddSubgroup G)
    (AddSubgroup.map
      (↑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        G →+ G)
      (stabilizer G a))
    (stabilizer G (g +ᵥ a))
rw₁ :
  Eq (α := AddSubgroup G)
    (AddSubgroup.map
      (↑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        G →+ G)
      (stabilizer G a))
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
rw₂ rw₃ :
  Eq (α := AddSubgroup G)
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
⊢ Eq (α := AddSubgroup G)
    (AddSubgroup.map
      (↑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        G →+ G)
      (stabilizer G a))
    (stabilizer G b)

Tactic:
rw [hg, stabilizer_vadd_eq_stabilizer_map_conj g a, ← AddEquiv.toAddMonoidHom_eq_coe]

Premises used: AddEquiv.toAddMonoidHom_eq_coe, AddAction.stabilizer_vadd_eq_stabilizer_map_conj
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a b : α
hg : b = g +ᵥ a
x : ↥(stabilizer G a)
⊢ Eq (α := G) ((↑((stabilizerEquivStabilizer hg : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G) : G)
    ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
          (a : G) → G)
        (↑x : G) :
      G)

Tactic:
simp [stabilizerEquivStabilizer]

Premises used: AddAction.stabilizerEquivStabilizer
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
b : α
hg : b = g +ᵥ b
x : ↥(stabilizer G b)
⊢ Eq (α := G) ((↑(((stabilizerEquivStabilizer hg).symm : (a : ↥(stabilizer G b)) → ↥(stabilizer G b)) x) : G) : G)
    ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) (-g)) :
            AddAut G) :
          (a : G) → G)
        (↑x : G) :
      G)

Tactic:
simp [stabilizerEquivStabilizer]

Premises used: AddAction.stabilizerEquivStabilizer
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g h k : G
a b c : α
hg : b = g +ᵥ a
hh : c = h +ᵥ b
hk : c = k +ᵥ a
H : k = h + g
h₁ :
  ∀ (x : ↥(stabilizer G a)),
    Eq.{u_1 + 1} (α := G)
      (↑(((stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) :
              (a : ↥(stabilizer G a)) → ↥(stabilizer G c))
            x) :
        G)
      (↑((stabilizerEquivStabilizer hk : (a : ↥(stabilizer G a)) → ↥(stabilizer G c)) x) : G)
⊢ (stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = stabilizerEquivStabilizer hk

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g h k : G
a b c : α
hg : b = g +ᵥ a
hh : c = h +ᵥ b
hk : c = k +ᵥ a
H : k = h + g
x : ↥(stabilizer G a)
⊢ Eq.{u_1 + 1} (α := G)
    (↑(((stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) :
            (a : ↥(stabilizer G a)) → ↥(stabilizer G c))
          x) :
      G)
    (↑((stabilizerEquivStabilizer hk : (a : ↥(stabilizer G a)) → ↥(stabilizer G c)) x) : G)

Tactic:
simp [stabilizerEquivStabilizer_apply, H]

Premises used: AddAction.stabilizerEquivStabilizer_apply
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
a : α
h :
  ∀ (x : ↥(stabilizer G a)),
    Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer ⋯ : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)
      (↑((AddEquiv.refl ↥(stabilizer G a) : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)
⊢ Eq (α := ↥(stabilizer G a) ≃+ ↥(stabilizer G a)) (stabilizerEquivStabilizer ⋯) (AddEquiv.refl ↥(stabilizer G a))

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
a : α
x : ↥(stabilizer G a)
⊢ Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer ⋯ : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)
    (↑((AddEquiv.refl ↥(stabilizer G a) : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)

Tactic:
simp [stabilizerEquivStabilizer_apply]

Premises used: AddAction.stabilizerEquivStabilizer_apply
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a b : α
hg : b = g +ᵥ a
h :
  ∀ (x : ↥(stabilizer G b)),
    Eq.{u_1 + 1} (α := G)
      (↑(((stabilizerEquivStabilizer hg).symm : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)
      (↑((stabilizerEquivStabilizer ⋯ : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)
⊢ (stabilizerEquivStabilizer hg).symm = stabilizerEquivStabilizer ⋯

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a b : α
hg : b = g +ᵥ a
x : ↥(stabilizer G b)
⊢ Eq.{u_1 + 1} (α := G) (↑(((stabilizerEquivStabilizer hg).symm : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)
    (↑((stabilizerEquivStabilizer ⋯ : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)

Tactic:
simp [stabilizerEquivStabilizer]

Premises used: AddAction.stabilizerEquivStabilizer
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a b : α
hg : b = -g +ᵥ a
h :
  ∀ (x : ↥(stabilizer G a)),
    Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer hg : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)
      (↑(((stabilizerEquivStabilizer ⋯).symm : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)
⊢ stabilizerEquivStabilizer hg = (stabilizerEquivStabilizer ⋯).symm

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a b : α
hg : b = -g +ᵥ a
x : ↥(stabilizer G a)
⊢ Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer hg : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)
    (↑(((stabilizerEquivStabilizer ⋯).symm : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)

Tactic:
simp [stabilizerEquivStabilizer]

Premises used: AddAction.stabilizerEquivStabilizer
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
rw : (∀ (x : α), x ∈ (swap a b)⁻¹ • S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)
⊢ Membership.mem (γ := Subgroup (Perm α)) (MulAction.stabilizer (Perm α) S) (swap a b) ↔ (a ∈ S ↔ b ∈ S)

Tactic:
rw [MulAction.mem_stabilizer_iff, Set.ext_iff, ← swap_inv]

Premises used: Equiv.swap_inv, MulAction.mem_stabilizer_iff, Set.ext_iff
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
simp_rw : (∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)
⊢ (∀ (x : α), x ∈ (swap a b)⁻¹ • S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)

Tactic:
simp_rw [Set.mem_inv_smul_set_iff, Perm.smul_def, swap_apply_def]

Premises used: Equiv.Perm.smul_def, Equiv.swap_apply_def, Set.mem_inv_smul_set_iff
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
h : ∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S
⊢ a ∈ S ↔ b ∈ S

Tactic:
simpa [Iff.comm] using h a

Premises used: Iff.comm
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
h : a ∈ S ↔ b ∈ S
x : α
pos : x = a → (b ∈ S ↔ x ∈ S)
pos₁ : ¬x = a → x = b → (a ∈ S ↔ x ∈ S)
neg : ¬x = a → ¬x = b → (x ∈ S ↔ x ∈ S)
⊢ (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S

Tactic:
split_ifs
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
h : a ∈ S ↔ b ∈ S
x : α
h_1 : x = a
⊢ b ∈ S ↔ x ∈ S

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
h : a ∈ S ↔ b ∈ S
x : α
h_1 : ¬x = a
h_2 : x = b
⊢ a ∈ S ↔ x ∈ S

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
h : a ∈ S ↔ b ∈ S
x : α
h_1 : ¬x = a
h_2 : ¬x = b
⊢ x ∈ S ↔ x ∈ S

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
⊢ (∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)

Tactic:
exact ⟨fun h ↦ by simpa [Iff.comm] using h a, by intros; split_ifs <;> simp [*]⟩
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
mp : H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s
mpr : (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s
⊢ H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
mp : g • s = s
⊢ g • s ⊆ s

Tactic:
apply Eq.subset

Premises used: Eq.subset