Theorem: l1_2_26_iii' (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
⊢ ↑(d1226Iii G) = {1} ↔ ∀ (g h : G), g * h = h * g
Tactic:
simp only [d1226Iii]
State after:
G : Type u_1
inst✝ : Group G
⊢ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) = {1} ↔ ∀ (g h : G), g * h = h * g

State before:
G : Type u_1
inst✝ : Group G
⊢ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) = {1} ↔ ∀ (g h : G), g * h = h * g
Tactic:
rw [Set.ext_iff]
State after:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) ↔ x ∈ {1}) ↔ ∀ (g h : G), g * h = h * g

State before:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) ↔ x ∈ {1}) ↔ ∀ (g h : G), g * h = h * g
Tactic:
simp_rw [← n1_2_26_ii']
State after:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) ↔ x ∈ {1}) ↔ ∀ (g h : G), ⁅g, h⁆ = 1

State before:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) ↔ x ∈ {1}) ↔ ∀ (g h : G), ⁅g, h⁆ = 1
Tactic:
simp only [SetLike.mem_coe, Set.mem_singleton_iff, Set.setOf_exists, Subgroup.closure_iUnion,
  Set.setOf_eq_eq_singleton']
State after:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1) ↔ ∀ (g h : G), ⁅g, h⁆ = 1

State before:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1) ↔ ∀ (g h : G), ⁅g, h⁆ = 1
Tactic:
constructor
State after:
case mp
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1) → ∀ (g h : G), ⁅g, h⁆ = 1

case mpr
G : Type u_1
inst✝ : Group G
⊢ (∀ (g h : G), ⁅g, h⁆ = 1) → ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1

State before:
case mp
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1) → ∀ (g h : G), ⁅g, h⁆ = 1
Tactic:
intro h g g'
State after:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ = 1

State before:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ = 1
Tactic:
rw [← h]
State after:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}

State before:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
Tactic:
apply Subgroup.mem_iSup_of_mem g
State after:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ ⨆ i, Subgroup.closure {⁅g, i⁆}

State before:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ ⨆ i, Subgroup.closure {⁅g, i⁆}
Tactic:
apply Subgroup.mem_iSup_of_mem g'
State after:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ Subgroup.closure {⁅g, g'⁆}

State before:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ∈ Subgroup.closure {⁅g, g'⁆}
Tactic:
rw [Subgroup.mem_closure_singleton]
State after:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ∃ n, ⁅g, g'⁆ ^ n = ⁅g, g'⁆

State before:
case mp
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ∃ n, ⁅g, g'⁆ ^ n = ⁅g, g'⁆
Tactic:
use 1
State after:
case h
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ^ 1 = ⁅g, g'⁆

State before:
case h
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
g g' : G
⊢ ⁅g, g'⁆ ^ 1 = ⁅g, g'⁆
Tactic:
rw [zpow_one]
State after:
no goals

State before:
case mpr
G : Type u_1
inst✝ : Group G
⊢ (∀ (g h : G), ⁅g, h⁆ = 1) → ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1
Tactic:
intro h g
State after:
case mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ g = 1

State before:
case mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ g = 1
Tactic:
constructor
State after:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} → g = 1

case mpr.mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g = 1 → g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}

State before:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} → g = 1
Tactic:
intro h'
State after:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
h' : g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
⊢ g = 1

State before:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
h' : g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
⊢ g = 1
Tactic:
symm
State after:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
h' : g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
⊢ 1 = g

State before:
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
h' : g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
⊢ 1 = g
Tactic:
simpa only [h, ciSup_const, Subgroup.mem_closure_singleton, one_zpow, exists_const] using h'
State after:
no goals

State before:
case mpr.mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
⊢ g = 1 → g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
Tactic:
rintro rfl
State after:
case mpr.mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
⊢ 1 ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}

State before:
case mpr.mpr
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
⊢ 1 ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
Tactic:
exact Subgroup.one_mem _
State after:
no goals