p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p { x // x ∈ K }
hHK : H ≤ K
a b : { x // x ∈ H }
h : ↑(Subgroup.inclusion hHK) a = ↑(Subgroup.inclusion hHK) b
⊢ ↑(↑(Subgroup.inclusion hHK) a) = ↑(↑(Subgroup.inclusion hHK) b)
p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p { x // x ∈ K }
hHK : H ≤ K
a b : { x // x ∈ H }
h : ↑(Subgroup.inclusion hHK) a = ↑(Subgroup.inclusion hHK) b
⊢ ↑a = ↑b
change ((Subgroup.inclusion hHK) a : G) = (Subgroup.inclusion hHK) b
no goals
p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p { x // x ∈ K }
hHK : H ≤ K
a b : { x // x ∈ H }
h : ↑(Subgroup.inclusion hHK) a = ↑(Subgroup.inclusion hHK) b
⊢ ↑(↑(Subgroup.inclusion hHK) a) = ↑(↑(Subgroup.inclusion hHK) b)
apply Subtype.ext_iff.mp h