Theorem: conjugate.mul_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⁻¹}
hz : z ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
⊢ y * z ∈ {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
hz : z ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
g : G
hg : g ∈ H
⊢ x * g * x⁻¹ * z ∈ {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
hz : z ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
g : G
hg : g ∈ H
⊢ x * g * x⁻¹ * z ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Tactic:
rcases hz with ⟨k, hk, rfl⟩
State after:
case intro.intro.intro.intro
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x g : G
hg : g ∈ H
k : G
hk : k ∈ H
⊢ x * g * x⁻¹ * (x * k * x⁻¹) ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}

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

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