Theorem: n_1_2_13 (AlgebraI/Subgroups.lean)

State before:
case mpr
G : Type u_1
inst✝ : Group G
A B : Set G
g : G
⊢ {x | ∃ a ∈ A, g⁻¹ * a = x} = B → A = {x | ∃ b ∈ B, g * b = x}
Tactic:
rintro rfl
State after:
case mpr
G : Type u_1
inst✝ : Group G
A : Set G
g : G
⊢ A = {x | ∃ b ∈ {x | ∃ a ∈ A, g⁻¹ * a = x}, g * b = x}

State before:
case mpr
G : Type u_1
inst✝ : Group G
A : Set G
g : G
⊢ A = {x | ∃ b ∈ {x | ∃ a ∈ A, g⁻¹ * a = x}, g * b = x}
Tactic:
ext
State after:
case mpr.h
G : Type u_1
inst✝ : Group G
A : Set G
g x✝ : G
⊢ x✝ ∈ A ↔ x✝ ∈ {x | ∃ b ∈ {x | ∃ a ∈ A, g⁻¹ * a = x}, g * b = x}

State before:
case mpr.h
G : Type u_1
inst✝ : Group G
A : Set G
g x✝ : G
⊢ x✝ ∈ A ↔ x✝ ∈ {x | ∃ b ∈ {x | ∃ a ∈ A, g⁻¹ * a = x}, g * b = x}
Tactic:
simp
State after:
no goals