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

State before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
⊢ conjugate H x = H
Tactic:
ext a
State after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ a ∈ conjugate H x ↔ a ∈ H

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

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

case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ a ∈ H → ∃ h ∈ 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 : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ (∃ h ∈ H, a = x * h * x⁻¹) → a ∈ H
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 : G
habelian : ∀ (a b : G), a * b = b * a
b : G
hb : b ∈ H
⊢ x * b * x⁻¹ ∈ H

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

State before:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
b : G
hb : b ∈ H
⊢ x⁻¹ * (x * b) ∈ H
Tactic:
rwa [show x⁻¹ * (x * b) = b by group]
State after:
no goals

State before:
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
b : G
hb : b ∈ H
⊢ x⁻¹ * (x * b) = b
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 : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ a ∈ H → ∃ h ∈ H, a = x * h * x⁻¹
Tactic:
intro ha
State after:
case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ ∃ h ∈ 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 : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ ∃ h ∈ 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 : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x⁻¹ * a * x ∈ H ∧ 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 : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x⁻¹ * a * x ∈ H ∧ a = x * (x⁻¹ * a * x) * x⁻¹
Tactic:
refine' ⟨_, by group⟩
State after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x⁻¹ * a * x ∈ H

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

State before:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x * (x⁻¹ * a) ∈ H
Tactic:
rwa [show x * (x⁻¹ * a) = a by group]
State after:
no goals

State before:
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ a = x * (x⁻¹ * a * x) * x⁻¹
Tactic:
group
State after:
no goals

State before:
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x * (x⁻¹ * a) = a
Tactic:
group
State after:
no goals