G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
⊢ (∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ⁅↑f g₁, ↑f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆) ∧
    ∀ (g₁ : G'), g₁ ∈ map f H₁ → ∀ (g₂ : G'), g₂ ∈ map f H₂ → ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
⊢ map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆
simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutatorElement]
case left
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
⊢ ∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ⁅↑f g₁, ↑f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆

case right
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
⊢ ∀ (g₁ : G'), g₁ ∈ map f H₁ → ∀ (g₂ : G'), g₂ ∈ map f H₂ → ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
⊢ (∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ⁅↑f g₁, ↑f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆) ∧
    ∀ (g₁ : G'), g₁ ∈ map f H₁ → ∀ (g₂ : G'), g₂ ∈ map f H₂ → ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
constructor
case left
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
p : G
hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅↑f p, ↑f q⁆ ∈ ⁅map f H₁, map f H₂⁆
case left
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
⊢ ∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ⁅↑f g₁, ↑f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆
intro p hp q hq
no goals
case left
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
p : G
hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅↑f p, ↑f q⁆ ∈ ⁅map f H₁, map f H₂⁆
exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ ⁅↑f p, ↑f q⁆ ∈ map f ⁅H₁, H₂⁆
case right
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
⊢ ∀ (g₁ : G'), g₁ ∈ map f H₁ → ∀ (g₂ : G'), g₂ ∈ map f H₂ → ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
rintro _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ ↑f ⁅p, q⁆ ∈ map f ⁅H₁, H₂⁆
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ ⁅↑f p, ↑f q⁆ ∈ map f ⁅H₁, H₂⁆
rw [← map_commutatorElement]
no goals
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type ?u.88445
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
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ ↑f ⁅p, q⁆ ∈ map f ⁅H₁, H₂⁆
exact mem_map_of_mem _ (commutator_mem_commutator hp hq)