Theorem: Subgroup.smul_coe (LeanCamCombi/Kneser/Mathlib.lean)

State before:
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
⊢ a • ↑s = ↑s
Tactic:
ext
State after:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ a • ↑s ↔ x✝ ∈ ↑s

State before:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ a • ↑s ↔ x✝ ∈ ↑s
Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem]
State after:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
x✝ : α
⊢ a⁻¹ • x✝ ∈ ↑s ↔ x✝ ∈ ↑s

State before:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
x✝ : α
⊢ a⁻¹ • x✝ ∈ ↑s ↔ x✝ ∈ ↑s
Tactic:
exact Subgroup.mul_mem_cancel_left _ (inv_mem ha)
State after:
no goals