G : Type u_1
G' : Type ?u.56694
F : Type ?u.56697
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
⊢ ∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ∀ (h : G), h ∈ H₃ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
G : Type u_1
G' : Type ?u.56694
F : Type ?u.56697
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥
h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥
⊢ ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥
simp_rw [commutator_eq_bot_iff_le_centralizer, commutator_le,
  mem_centralizer_iff_commutator_eq_one, ← commutatorElement_def] at h1 h2⊢
G : Type u_1
G' : Type ?u.56694
F : Type ?u.56697
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ H₃
⊢ ⁅z, ⁅x, y⁆⁆ = 1
G : Type u_1
G' : Type ?u.56694
F : Type ?u.56697
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
⊢ ∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ∀ (h : G), h ∈ H₃ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
intro x hx y hy z hz
G : Type u_1
G' : Type ?u.56694
F : Type ?u.56697
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ H₃
⊢ ⁅z, ⁅x, y⁆⁆ = x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹

G : Type u_1
G' : Type ?u.56694
F : Type ?u.56697
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1
G : Type u_1
G' : Type ?u.56694
F : Type ?u.56697
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ H₃
⊢ ⁅z, ⁅x, y⁆⁆ = 1
trans x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
no goals
G : Type u_1
G' : Type ?u.56694
F : Type ?u.56697
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ H₃
⊢ ⁅z, ⁅x, y⁆⁆ = x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
group
G : Type u_1
G' : Type ?u.56694
F : Type ?u.56697
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ H₃
⊢ x * z * 1⁻¹ * z⁻¹ * y * 1⁻¹ * y⁻¹ * x⁻¹ = 1
G : Type u_1
G' : Type ?u.56694
F : Type ?u.56697
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1
rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy]
no goals
G : Type u_1
G' : Type ?u.56694
F : Type ?u.56697
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ H₃
⊢ x * z * 1⁻¹ * z⁻¹ * y * 1⁻¹ * y⁻¹ * x⁻¹ = 1
group