awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
h :
  ∀ (x : G),
    Membership.mem (γ := Subgroup G) (stabilizer.{u_1, u_3} G (α := Set α) univ) x ↔
      Membership.mem (γ := Subgroup G) ⊤ x
⊢ Eq (α := Subgroup G) (stabilizer.{u_1, u_3} G (α := Set α) univ) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
x : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer.{u_1, u_3} G (α := Set α) univ) x ↔ Membership.mem (γ := Subgroup G) ⊤ x

Tactic:
simp
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
b : α
h :
  ∀ (x : G),
    Membership.mem (γ := Subgroup G) (stabilizer G (α := Set α) {b}) x ↔
      Membership.mem (γ := Subgroup G) (stabilizer G b) x
⊢ Eq (α := Subgroup G) (stabilizer G (α := Set α) {b}) (stabilizer G b)

Tactic:
ext
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
b : α
x : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (α := Set α) {b}) x ↔
    Membership.mem (γ := Subgroup G) (stabilizer G b) x

Tactic:
simp
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s

Tactic:
mem_stabilizer_iff.trans ⟨fun h b ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro, Iff.trans, MulAction.mem_stabilizer_iff
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
refine_1 : ∀ (h : a • s = s) (b : α), a • b ∈ s ↔ b ∈ s
refine_2 : ∀ (h : ∀ (b : α), a • b ∈ s ↔ b ∈ s), a • s = s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s

Tactic:
refine mem_stabilizer_iff.trans ⟨fun h b ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro, Iff.trans, MulAction.mem_stabilizer_iff
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
h : a • s = s
b : α
refine_1 : a • b ∈ s ↔ a • b ∈ a • s
refine_1₁ refine_1₂ : a • b ∈ s ↔ a • b ∈ s
⊢ a • b ∈ s ↔ b ∈ s

Tactic:
rw [← (smul_mem_smul_set_iff : a • b ∈ _ ↔ _), h]

Premises used: Set.smul_mem_smul_set_iff
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
refine_2 : ∀ (x : α), a⁻¹ • x ∈ s ↔ x ∈ s
⊢ a • s = s

Tactic:
simp_rw [Set.ext_iff, mem_smul_set_iff_inv_smul_mem]

Premises used: Set.ext_iff, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ ∀ (b : α),
    (HSMul.hSMul (β := α) a ((Equiv.symm (toPerm a) : (a : α) → α) b : α) ∈ s ↔
        Membership.mem (α := α) s ((Equiv.symm (toPerm a) : (a : α) → α) b : α)) ↔
      (a⁻¹ • b ∈ s ↔ b ∈ s)

Tactic:
simp [Iff.comm]

Premises used: Iff.comm
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ ∀ (x : α), a⁻¹ • x ∈ s ↔ x ∈ s

Tactic:
exact ((MulAction.toPerm a).forall_congr' <| by simp [Iff.comm]).1 h

Premises used: MulAction.toPerm, Equiv.forall_congr', Iff.mp
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
f : G →* H
s : Set G
a : H
simp :
  ∀ (x : G),
    x • s = s → (f : (a : G) → H) x = a → HSMul.hSMul (β := Set H) a ((⇑f : (a : G) → H) '' s) = (⇑f : (a : G) → H) '' s
⊢ a ∈ Subgroup.map f (stabilizer G s) →
    Membership.mem (γ := Subgroup H) (stabilizer H (α := Set H) ((⇑f : (a : G) → H) '' s)) a

Tactic:
simp only [Subgroup.mem_map, mem_stabilizer_iff, forall_exists_index, and_imp]

Premises used: and_imp, forall_exists_index, Subgroup.mem_map, MulAction.mem_stabilizer_iff
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
f : G →* H
s : Set G
a : G
ha : a • s = s
rw : Eq.{u_2 + 1} (α := Set H) ((⇑f : (a : G) → H) '' (a • s)) ((⇑f : (a : G) → H) '' s)
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set H) ((⇑f : (a : G) → H) '' s) ((⇑f : (a : G) → H) '' s)
⊢ HSMul.hSMul (α := H) (β := Set H) ((f : (a : G) → H) a : H) ((⇑f : (a : G) → H) '' s) = (⇑f : (a : G) → H) '' s

Tactic:
rw [← image_smul_distrib, ha]

Premises used: Set.image_smul_distrib
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Set G
h : ∀ (x : G), x ∈ (↑(stabilizer G s) : Set G) * s ↔ x ∈ s
⊢ (↑(stabilizer G s) : Set G) * s = s

Tactic:
ext
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Set G
x : G
⊢ x ∈ (↑(stabilizer G s) : Set G) * s ↔ x ∈ s

Tactic:
⟨?_, fun h ↦ ⟨_, (stabilizer G s).one_mem, _, h, one_mul _⟩⟩

Premises used: Subgroup.one_mem, And.intro, Iff.intro, Exists.intro, MulAction.stabilizer, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Set G
x : G
h : x ∈ (↑(stabilizer G s) : Set G) * s → x ∈ s
⊢ x ∈ (↑(stabilizer G s) : Set G) * s ↔ x ∈ s

Tactic:
refine ⟨?_, fun h ↦ ⟨_, (stabilizer G s).one_mem, _, h, one_mul _⟩⟩
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Set G
a : G
ha : a ∈ (↑(stabilizer G s) : Set G)
b : G
hb : b ∈ s
h : (fun (x1 x2 : G) ↦ x1 * x2) a b ∈ a • s
⊢ (fun (x1 x2 : G) ↦ x1 * x2) a b ∈ s

Tactic:
rw [← mem_stabilizer_iff.1 ha]

Premises used: Iff.mp, MulAction.mem_stabilizer_iff
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Set G
a : G
ha : a ∈ (↑(stabilizer G s) : Set G)
b : G
hb : b ∈ s
⊢ (fun (x1 x2 : G) ↦ x1 * x2) a b ∈ a • s

Tactic:
smul_mem_smul_set hb

Premises used: Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Set G
a : G
ha : a ∈ (↑(stabilizer G s) : Set G)
b : G
hb : b ∈ s
⊢ (fun (x1 x2 : G) ↦ x1 * x2) a b ∈ a • s

Tactic:
exact smul_mem_smul_set hb

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
f : Set α → Set α → Set α
hf : ∀ (a : G), a • f s t = f (a • s) (a • t)
⊢ LE.le (α := Subgroup G) (stabilizer G s ⊓ stabilizer G t) (stabilizer G (f s t))

Tactic:
aesop (add simp [SetLike.le_def])

Premises used: SetLike.le_def
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
⊢ LE.le (α := Subgroup G) (stabilizer G s ⊓ stabilizer G t) (stabilizer G (s ∪ t))

Tactic:
stabilizer_inf_stabilizer_le_stabilizer_apply₂ fun _ ↦ smul_set_union

Premises used: Set.smul_set_union, MulAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
⊢ LE.le (α := Subgroup G) (stabilizer G s ⊓ stabilizer G t) (stabilizer G (s ∩ t))

Tactic:
stabilizer_inf_stabilizer_le_stabilizer_apply₂ fun _ ↦ smul_set_inter

Premises used: Set.smul_set_inter, MulAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
⊢ LE.le (α := Subgroup G) (stabilizer G s ⊓ stabilizer G t) (stabilizer G (s \ t))

Tactic:
stabilizer_inf_stabilizer_le_stabilizer_apply₂ fun _ ↦ smul_set_sdiff

Premises used: Set.smul_set_sdiff, MulAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
⊢ Eq (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G s)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
refine_1 : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G s)
refine_2 : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G (s ∪ t))
⊢ Eq (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G s)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
⊢ LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G (s ∪ t) ⊓ stabilizer G t)

Tactic:
simpa
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
⊢ LE.le (α := Subgroup G) (stabilizer G (s ∪ t) ⊓ stabilizer G t) (stabilizer G ((s ∪ t) \ t))

Tactic:
stabilizer_inf_stabilizer_le_stabilizer_sdiff

Premises used: MulAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
rw : s ∩ t ⊆ ∅
⊢ Eq (α := Subgroup G) (stabilizer G ((s ∪ t) \ t)) (stabilizer G s)

Tactic:
rw [union_diff_cancel_right]

Premises used: Set.union_diff_cancel_right
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
⊢ s ∩ t ⊆ ∅

Tactic:
simpa [← disjoint_iff_inter_eq_empty]

Premises used: Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (MulAction.stabilizer G s) (MulAction.stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (MulAction.stabilizer G (s ∪ t)) (MulAction.stabilizer G t)
stabilizer :
  LE.le (α := Subgroup G) (MulAction.stabilizer G (s ∪ t)) (MulAction.stabilizer G (s ∪ t) ⊓ MulAction.stabilizer G t)
stabilizer₁ : Eq (α := Subgroup G) (MulAction.stabilizer G ((s ∪ t) \ t)) (MulAction.stabilizer G s)
⊢ LE.le (α := Subgroup G) (MulAction.stabilizer G (s ∪ t)) (MulAction.stabilizer G s)

Tactic:
calc
      stabilizer G (s ∪ t)
        ≤ stabilizer G (s ∪ t) ⊓ stabilizer G t := by simpa
      _ ≤ stabilizer G ((s ∪ t) \ t) := stabilizer_inf_stabilizer_le_stabilizer_sdiff
      _ = stabilizer G s := by rw [union_diff_cancel_right]; simpa [← disjoint_iff_inter_eq_empty]

Premises used: MulAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff, SDiff.sdiff, Union.union, MulAction.stabilizer
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
⊢ LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G s ⊓ stabilizer G t)

Tactic:
simpa
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
⊢ LE.le (α := Subgroup G) (stabilizer G s ⊓ stabilizer G t) (stabilizer G (s ∪ t))

Tactic:
stabilizer_inf_stabilizer_le_stabilizer_union

Premises used: MulAction.stabilizer_inf_stabilizer_le_stabilizer_union
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (MulAction.stabilizer G s) (MulAction.stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (MulAction.stabilizer G (s ∪ t)) (MulAction.stabilizer G t)
stabilizer : LE.le (α := Subgroup G) (MulAction.stabilizer G s) (MulAction.stabilizer G s ⊓ MulAction.stabilizer G t)
⊢ LE.le (α := Subgroup G) (MulAction.stabilizer G s) (MulAction.stabilizer G (s ∪ t))

Tactic:
calc
      stabilizer G s
        ≤ stabilizer G s ⊓ stabilizer G t := by simpa
      _ ≤ stabilizer G (s ∪ t) := stabilizer_inf_stabilizer_le_stabilizer_union

Premises used: MulAction.stabilizer_inf_stabilizer_le_stabilizer_union, Union.union, MulAction.stabilizer
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G t) (stabilizer G s)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G s)
rw : Eq (α := Subgroup G) (stabilizer G (t ∪ s)) (stabilizer G t)
rw₁ rw₂ : Eq (α := Subgroup G) (stabilizer G t) (stabilizer G t)
⊢ Eq (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)

Tactic:
rw [union_comm, stabilizer_union_eq_left hdisj.symm hstab (union_comm .. ▸ hstab_union)]

Premises used: Eq.rec, Set.union_comm, Disjoint.symm, MulAction.stabilizer_union_eq_left
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ (↑(stabilizer G s) : Set G)
rw : b <• a ∈ b •> s
⊢ b <• a ∈ s

Tactic:
rw [← hb]
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ (↑(stabilizer G s) : Set G)
⊢ b <• a ∈ b •> s

Tactic:
smul_mem_smul_set ha

Premises used: Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ (↑(stabilizer G s) : Set G)
⊢ b <• a ∈ b •> s

Tactic:
exact smul_mem_smul_set ha

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ (↑(stabilizer G s) : Set G)
rwa : b • a ∈ s
rwa₁ rwa₂ rwa₃ rwa₄ : a ∈ s
⊢ b * a ∈ s

Tactic:
rwa [← smul_eq_mul, mem_stabilizer_set.1 hb]

Premises used: MulAction.mem_stabilizer_set, Iff.mp, smul_eq_mul
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Set G
hs₀ : s.Nonempty
hs : s.Finite
obtain : ∀ (a : G) (ha : a ∈ s), (↑(stabilizer G s) : Set G).Finite
⊢ (↑(stabilizer G s) : Set G).Finite

Tactic:
obtain ⟨a, ha⟩ := hs₀
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : s.Finite
a : G
ha : a ∈ s
⊢ (↑(stabilizer G s) : Set G).Finite

Tactic:
(hs.div <| finite_singleton _).subset <| stabilizer_subset_div_right ha

Premises used: Set.Finite.subset, Set.Finite.div, MulAction.stabilizer_subset_div_right, Set.finite_singleton
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : s.Finite
a : G
ha : a ∈ s
⊢ (↑(stabilizer G s) : Set G).Finite

Tactic:
exact (hs.div <| finite_singleton _).subset <| stabilizer_subset_div_right ha

Premises used: Set.Finite.subset, Set.Finite.div, MulAction.stabilizer_subset_div_right, Set.finite_singleton
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : CommGroup G
s : Set G
a : G
ha : a ∈ s
⊢ a • (↑(stabilizer G s) : Set G) ⊆ s

Tactic:
simpa using op_smul_set_stabilizer_subset ha

Premises used: MulAction.op_smul_set_stabilizer_subset
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
simp_rw : ∀ (x : G), (∀ (b : G), x • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)) ↔ x ∈ s
⊢ stabilizer G (↑s : Set G) = s

Tactic:
simp_rw [SetLike.ext_iff, mem_stabilizer_set]

Premises used: SetLike.ext_iff, MulAction.mem_stabilizer_set
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
⊢ ∀ (x : G), (∀ (b : G), x • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)) ↔ x ∈ s

Tactic:
fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_left ha⟩

Premises used: Subgroup.mul_mem_cancel_left, Iff.intro
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
refine : ∀ (a : G) (h : ∀ (b : G), a • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)), a ∈ s
⊢ ∀ (x : G), (∀ (b : G), x • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)) ↔ x ∈ s

Tactic:
refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_left ha⟩
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
a : G
h : ∀ (b : G), a • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)
⊢ a ∈ s

Tactic:
simpa only [smul_eq_mul, SetLike.mem_coe, mul_one] using (h 1).2 s.one_mem

Premises used: Iff.mpr, Subgroup.one_mem, SetLike.mem_coe, smul_eq_mul, mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
simp_rw : ∀ (x : Gᵐᵒᵖ), (∀ (b : G), x • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)) ↔ x ∈ s.op
⊢ stabilizer Gᵐᵒᵖ (↑s : Set G) = s.op

Tactic:
simp_rw [SetLike.ext_iff, mem_stabilizer_set]

Premises used: SetLike.ext_iff, MulAction.mem_stabilizer_set
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
simp : ∀ (a : G), (∀ (b : G), b * a ∈ s ↔ b ∈ s) ↔ a ∈ s
⊢ ∀ (x : Gᵐᵒᵖ), (∀ (b : G), x • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)) ↔ x ∈ s.op

Tactic:
simp only [smul_eq_mul_unop, SetLike.mem_coe, Subgroup.mem_op, «forall», unop_op]

Premises used: Subgroup.mem_op, MulOpposite.forall, SetLike.mem_coe, MulOpposite.unop_op, MulOpposite.smul_eq_mul_unop
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), b * a ∈ s ↔ b ∈ s) ↔ a ∈ s

Tactic:
fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_right ha⟩

Premises used: Subgroup.mul_mem_cancel_right, Iff.intro
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
refine : ∀ (a : G) (h : ∀ (b : G), b * a ∈ s ↔ b ∈ s), a ∈ s
⊢ ∀ (a : G), (∀ (b : G), b * a ∈ s ↔ b ∈ s) ↔ a ∈ s

Tactic:
refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_right ha⟩
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
a : G
h : ∀ (b : G), b * a ∈ s ↔ b ∈ s
⊢ a ∈ s

Tactic:
simpa only [op_smul_eq_mul, SetLike.mem_coe, one_mul] using (h 1).2 s.one_mem

Premises used: Iff.mpr, op_smul_eq_mul, Subgroup.one_mem, SetLike.mem_coe, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup Gᵐᵒᵖ
simp_rw : ∀ (x : G), (∀ (b : Gᵐᵒᵖ), x • b ∈ (↑s : Set Gᵐᵒᵖ) ↔ b ∈ (↑s : Set Gᵐᵒᵖ)) ↔ x ∈ s.unop
⊢ stabilizer G (↑s : Set Gᵐᵒᵖ) = s.unop

Tactic:
simp_rw [SetLike.ext_iff, mem_stabilizer_set]

Premises used: SetLike.ext_iff, MulAction.mem_stabilizer_set
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup Gᵐᵒᵖ
⊢ ∀ (x : G), (∀ (b : Gᵐᵒᵖ), x • b ∈ (↑s : Set Gᵐᵒᵖ) ↔ b ∈ (↑s : Set Gᵐᵒᵖ)) ↔ x ∈ s.unop

Tactic:
fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_right ha⟩

Premises used: Subgroup.mul_mem_cancel_right, Iff.intro
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup Gᵐᵒᵖ
refine : ∀ (a : G) (h : ∀ (b : Gᵐᵒᵖ), a • b ∈ (↑s : Set Gᵐᵒᵖ) ↔ b ∈ (↑s : Set Gᵐᵒᵖ)), a ∈ s.unop
⊢ ∀ (x : G), (∀ (b : Gᵐᵒᵖ), x • b ∈ (↑s : Set Gᵐᵒᵖ) ↔ b ∈ (↑s : Set Gᵐᵒᵖ)) ↔ x ∈ s.unop

Tactic:
refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_right ha⟩
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup Gᵐᵒᵖ
a : G
h : ∀ (b : Gᵐᵒᵖ), a • b ∈ (↑s : Set Gᵐᵒᵖ) ↔ b ∈ (↑s : Set Gᵐᵒᵖ)
⊢ 1 * op a ∈ s

Tactic:
have : 1 * MulOpposite.op a ∈ s := (h 1).2 s.one_mem
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
inst : Group G
s : Subgroup Gᵐᵒᵖ
a : G
h : ∀ (b : Gᵐᵒᵖ), a • b ∈ (↑s : Set Gᵐᵒᵖ) ↔ b ∈ (↑s : Set Gᵐᵒᵖ)
this : 1 * op a ∈ s
⊢ a ∈ s.unop

Tactic:
simpa only [op_smul_eq_mul, SetLike.mem_coe, one_mul] using this

Premises used: op_smul_eq_mul, SetLike.mem_coe, one_mul
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
s : Finset α
h :
  ∀ (x : G),
    Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) x ↔ Membership.mem (γ := Subgroup G) (stabilizer G s) x
⊢ Eq (α := Subgroup G) (stabilizer G (↑s : Set α)) (stabilizer G s)

Tactic:
ext
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
s : Finset α
x : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) x ↔ Membership.mem (γ := Subgroup G) (stabilizer G s) x

Tactic:
simp [← Finset.coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
⊢ Eq (α := Subgroup G) (stabilizer.{u_1, u_3} G (α := Finset α) ∅) ⊤

Tactic:
Subgroup.coe_eq_univ.1 <| eq_univ_of_forall Finset.smul_finset_empty

Premises used: Finset.smul_finset_empty, Set.eq_univ_of_forall, Subgroup.coe_eq_univ, Iff.mp
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Fintype α
h :
  ∀ (x : G),
    Membership.mem (γ := Subgroup G) (stabilizer.{u_1, u_3} G (α := Finset α) Finset.univ) x ↔
      Membership.mem (γ := Subgroup G) ⊤ x
⊢ Eq (α := Subgroup G) (stabilizer.{u_1, u_3} G (α := Finset α) Finset.univ) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Fintype α
x : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer.{u_1, u_3} G (α := Finset α) Finset.univ) x ↔
    Membership.mem (γ := Subgroup G) ⊤ x

Tactic:
simp
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
b : α
h :
  ∀ (x : G),
    Membership.mem (γ := Subgroup G) (stabilizer G (α := Finset α) {b}) x ↔
      Membership.mem (γ := Subgroup G) (stabilizer G b) x
⊢ Eq (α := Subgroup G) (stabilizer G (α := Finset α) {b}) (stabilizer G b)

Tactic:
ext
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
b : α
x : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (α := Finset α) {b}) x ↔
    Membership.mem (γ := Subgroup G) (stabilizer G b) x

Tactic:
simp
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
simp_rw : Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
simp_rw₁ : (∀ (b : α), a • b ∈ (↑s : Set α) ↔ b ∈ (↑s : Set α)) ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s

Tactic:
simp_rw [← stabilizer_coe_finset, mem_stabilizer_set, Finset.mem_coe]

Premises used: MulAction.mem_stabilizer_set, Finset.mem_coe, MulAction.stabilizer_coe_finset