Theorem: conjugate_top (FormalisingMathematics2024/Solutions/Section07subgroupsAndHomomorphisms/Sheet1.lean)

State before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ conjugate ⊤ x = ⊤
Tactic:
ext a
State after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a ∈ conjugate ⊤ x ↔ a ∈ ⊤

State before:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a ∈ conjugate ⊤ x ↔ a ∈ ⊤
Tactic:
rw [mem_conjugate_iff]
State after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ (∃ h ∈ ⊤, a = x * h * x⁻¹) ↔ a ∈ ⊤

State before:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ (∃ h ∈ ⊤, a = x * h * x⁻¹) ↔ a ∈ ⊤
Tactic:
constructor
State after:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ (∃ h ∈ ⊤, a = x * h * x⁻¹) → a ∈ ⊤

case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a ∈ ⊤ → ∃ h ∈ ⊤, a = x * h * x⁻¹

State before:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ (∃ h ∈ ⊤, a = x * h * x⁻¹) → a ∈ ⊤
Tactic:
intro h
State after:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : ∃ h ∈ ⊤, a = x * h * x⁻¹
⊢ a ∈ ⊤

State before:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : ∃ h ∈ ⊤, a = x * h * x⁻¹
⊢ a ∈ ⊤
Tactic:
exact Subgroup.mem_top a
State after:
no goals

State before:
case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a ∈ ⊤ → ∃ h ∈ ⊤, a = x * h * x⁻¹
Tactic:
intro h
State after:
case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : a ∈ ⊤
⊢ ∃ h ∈ ⊤, a = x * h * x⁻¹

State before:
case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : a ∈ ⊤
⊢ ∃ h ∈ ⊤, a = x * h * x⁻¹
Tactic:
use x⁻¹ * a * x
State after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : a ∈ ⊤
⊢ x⁻¹ * a * x ∈ ⊤ ∧ a = x * (x⁻¹ * a * x) * x⁻¹

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

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

State before:
case h.left
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : a ∈ ⊤
⊢ x⁻¹ * a * x ∈ ⊤
Tactic:
apply Subgroup.mem_top
State after:
no goals

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