Theorem: conjugate.inv_mem (FormalisingMathematics2024/Solutions/Section07subgroupsAndHomomorphisms/Sheet1.lean)

State before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
hy : y ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
⊢ y⁻¹ ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Tactic:
rcases hy with ⟨g, hg, rfl⟩
State after:
case intro.intro
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x z g : G
hg : g ∈ H
⊢ (x * g * x⁻¹)⁻¹ ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}

State before:
case intro.intro
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x z g : G
hg : g ∈ H
⊢ (x * g * x⁻¹)⁻¹ ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Tactic:
use g⁻¹, inv_mem hg
State after:
case right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x z g : G
hg : g ∈ H
⊢ (x * g * x⁻¹)⁻¹ = x * g⁻¹ * x⁻¹

State before:
case right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x z g : G
hg : g ∈ H
⊢ (x * g * x⁻¹)⁻¹ = x * g⁻¹ * x⁻¹
Tactic:
group
State after:
no goals