G : Type u_1
G' : Type ?u.712969
inst✝³ : Group G
inst✝² : Group G'
A✝ : Type ?u.712978
inst✝¹ : AddGroup A✝
N : Type ?u.712984
inst✝ : Group N
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ map (Subgroup.subtype B) (subgroupOf (A ⊔ A') B) = map (Subgroup.subtype B) (subgroupOf A B ⊔ subgroupOf A' B)
G : Type u_1
G' : Type ?u.712969
inst✝³ : Group G
inst✝² : Group G'
A✝ : Type ?u.712978
inst✝¹ : AddGroup A✝
N : Type ?u.712984
inst✝ : Group N
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ subgroupOf (A ⊔ A') B = subgroupOf A B ⊔ subgroupOf A' B
refine'
  map_injective_of_ker_le B.subtype (ker_le_comap _ _)
    (le_trans (ker_le_comap B.subtype _) le_sup_left) _
G : Type u_1
G' : Type ?u.712969
inst✝³ : Group G
inst✝² : Group G'
A✝ : Type ?u.712978
inst✝¹ : AddGroup A✝
N : Type ?u.712984
inst✝ : Group N
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'
G : Type u_1
G' : Type ?u.712969
inst✝³ : Group G
inst✝² : Group G'
A✝ : Type ?u.712978
inst✝¹ : AddGroup A✝
N : Type ?u.712984
inst✝ : Group N
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ map (Subgroup.subtype B) (subgroupOf (A ⊔ A') B) = map (Subgroup.subtype B) (subgroupOf A B ⊔ subgroupOf A' B)
simp only [subgroupOf, map_comap_eq, map_sup, subtype_range]
no goals
G : Type u_1
G' : Type ?u.712969
inst✝³ : Group G
inst✝² : Group G'
A✝ : Type ?u.712978
inst✝¹ : AddGroup A✝
N : Type ?u.712984
inst✝ : Group N
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'
rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]