G : Type u_1
G' : Type ?u.481704
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.481713
inst✝² : AddGroup A
N : Type ?u.481719
P : Type ?u.481722
inst✝¹ : Group N
inst✝ : Group P
K H : Subgroup G
⊢ Subtype.val '' ↑⊤ = ↑H
G : Type u_1
G' : Type ?u.481704
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.481713
inst✝² : AddGroup A
N : Type ?u.481719
P : Type ?u.481722
inst✝¹ : Group N
inst✝ : Group P
K H : Subgroup G
⊢ range (Subgroup.subtype H) = H
rw [range_eq_map, ← SetLike.coe_set_eq, coe_map, Subgroup.coeSubtype]
case h
G : Type u_1
G' : Type ?u.481704
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.481713
inst✝² : AddGroup A
N : Type ?u.481719
P : Type ?u.481722
inst✝¹ : Group N
inst✝ : Group P
K H : Subgroup G
x✝ : G
⊢ x✝ ∈ Subtype.val '' ↑⊤ ↔ x✝ ∈ ↑H
G : Type u_1
G' : Type ?u.481704
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.481713
inst✝² : AddGroup A
N : Type ?u.481719
P : Type ?u.481722
inst✝¹ : Group N
inst✝ : Group P
K H : Subgroup G
⊢ Subtype.val '' ↑⊤ = ↑H
ext
no goals
case h
G : Type u_1
G' : Type ?u.481704
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.481713
inst✝² : AddGroup A
N : Type ?u.481719
P : Type ?u.481722
inst✝¹ : Group N
inst✝ : Group P
K H : Subgroup G
x✝ : G
⊢ x✝ ∈ Subtype.val '' ↑⊤ ↔ x✝ ∈ ↑H
simp