case a
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
⊢ ⁅prod H₁ K₁, prod H₂ K₂⁆ ≤ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆

case a
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
⊢ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
⊢ ⁅prod H₁ K₁, prod H₂ K₂⁆ = prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
apply le_antisymm
case a
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
⊢ ∀ (g₁ : G × G'), g₁ ∈ prod H₁ K₁ → ∀ (g₂ : G × G'), g₂ ∈ prod H₂ K₂ → ⁅g₁, g₂⁆ ∈ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
case a
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
⊢ ⁅prod H₁ K₁, prod H₂ K₂⁆ ≤ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
rw [commutator_le]
case a.mk.intro.mk.intro
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
p₁ : G
p₂ : G'
hp₁ : (p₁, p₂).fst ∈ ↑H₁.toSubmonoid
hp₂ : (p₁, p₂).snd ∈ ↑K₁.toSubmonoid
q₁ : G
q₂ : G'
hq₁ : (q₁, q₂).fst ∈ ↑H₂.toSubmonoid
hq₂ : (q₁, q₂).snd ∈ ↑K₂.toSubmonoid
⊢ ⁅(p₁, p₂), (q₁, q₂)⁆ ∈ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
case a
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
⊢ ∀ (g₁ : G × G'), g₁ ∈ prod H₁ K₁ → ∀ (g₂ : G × G'), g₂ ∈ prod H₂ K₂ → ⁅g₁, g₂⁆ ∈ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
rintro ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩
no goals
case a.mk.intro.mk.intro
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
p₁ : G
p₂ : G'
hp₁ : (p₁, p₂).fst ∈ ↑H₁.toSubmonoid
hp₂ : (p₁, p₂).snd ∈ ↑K₁.toSubmonoid
q₁ : G
q₂ : G'
hq₁ : (q₁, q₂).fst ∈ ↑H₂.toSubmonoid
hq₂ : (q₁, q₂).snd ∈ ↑K₂.toSubmonoid
⊢ ⁅(p₁, p₂), (q₁, q₂)⁆ ∈ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩
case a
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
case a
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
⊢ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
rw [prod_le_iff]
case a.right
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inr G G') K₁, map (MonoidHom.inr G G') K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
case a.right
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
rw [map_commutator]
no goals
case a.right
G : Type u_2
G' : Type u_1
F : Type ?u.96044
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
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inr G G') K₁, map (MonoidHom.inr G G') K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
apply commutator_mono <;>
  simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
    MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]