Theorem: conjugate_bot (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:
rw [Subgroup.mem_bot]
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 = 1

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 = 1
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 = 1

case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a = 1 → ∃ 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 = 1
Tactic:
rintro ⟨b, hb, rfl⟩
State after:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z b : G
hb : b ∈ ⊥
⊢ x * b * x⁻¹ = 1

State before:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z b : G
hb : b ∈ ⊥
⊢ x * b * x⁻¹ = 1
Tactic:
rw [Subgroup.mem_bot] at hb
State after:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z b : G
hb : b = 1
⊢ x * b * x⁻¹ = 1

State before:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z b : G
hb : b = 1
⊢ x * b * x⁻¹ = 1
Tactic:
rw [hb]
State after:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z b : G
hb : b = 1
⊢ x * 1 * x⁻¹ = 1

State before:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z b : G
hb : b = 1
⊢ x * 1 * x⁻¹ = 1
Tactic:
group
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 = 1 → ∃ h ∈ ⊥, a = x * h * x⁻¹
Tactic:
rintro rfl
State after:
case h.mpr
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ ∃ h ∈ ⊥, 1 = x * h * x⁻¹

State before:
case h.mpr
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ ∃ h ∈ ⊥, 1 = 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 ∈ ⊥ ∧ 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 ∈ ⊥ ∧ 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 ∈ ⊥

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 ∈ ⊥
Tactic:
rw [Subgroup.mem_bot]
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