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

State before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Tactic:
use 1
State after:
case h
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ H ∧ 1 = x * 1 * x⁻¹

State before:
case h
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ H ∧ 1 = x * 1 * x⁻¹
Tactic:
constructor
State after:
case h.left
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ H

case h.right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 = x * 1 * x⁻¹

State before:
case h.left
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ H
Tactic:
exact H.one_mem
State after:
no goals

State before:
case h.right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 = x * 1 * x⁻¹
Tactic:
group
State after:
no goals