case hH
G : Type u_1
G' : Type ?u.612020
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.612029
inst✝¹ : AddGroup A
N : Type ?u.612035
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ H ≤ H ⊔ K

case hK
G : Type u_1
G' : Type ?u.612020
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.612029
inst✝¹ : AddGroup A
N : Type ?u.612035
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ K ≤ H ⊔ K
G : Type u_1
G' : Type ?u.612020
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.612029
inst✝¹ : AddGroup A
N : Type ?u.612035
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ Codisjoint (subgroupOf H (H ⊔ K)) (subgroupOf K (H ⊔ K))
rw [codisjoint_iff, sup_subgroupOf_eq, subgroupOf_self]
no goals
case hH
G : Type u_1
G' : Type ?u.612020
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.612029
inst✝¹ : AddGroup A
N : Type ?u.612035
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ H ≤ H ⊔ K

case hK
G : Type u_1
G' : Type ?u.612020
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.612029
inst✝¹ : AddGroup A
N : Type ?u.612035
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ K ≤ H ⊔ K
exacts [le_sup_left, le_sup_right]