case h
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
g : α
x : β
h : α
⊢ h ∈ stabilizer α (g • x) ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (↑MulAut.conj g)) (stabilizer α x)
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
g : α
x : β
⊢ stabilizer α (g • x) = Subgroup.map (MulEquiv.toMonoidHom (↑MulAut.conj g)) (stabilizer α x)
ext h
no goals
case h
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
g : α
x : β
h : α
⊢ h ∈ stabilizer α (g • x) ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (↑MulAut.conj g)) (stabilizer α x)
rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul, mul_left_inv,
  one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]