case mk
G : Type u_2
G' : Type ?u.62545
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.62554
inst✝⁴ : AddGroup A
M : Type ?u.62560
S : Type u_1
inst✝³ : DivInvMonoid M
inst✝² : SetLike S M
hSM : SubgroupClass S M
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ K
hx : ↑{ val := val✝, property := property✝ } ∈ H
⊢ ↑(inclusion h) { val := ↑{ val := val✝, property := property✝ }, property := hx } =
    { val := val✝, property := property✝ }
G : Type u_2
G' : Type ?u.62545
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.62554
inst✝⁴ : AddGroup A
M : Type ?u.62560
S : Type u_1
inst✝³ : DivInvMonoid M
inst✝² : SetLike S M
hSM : SubgroupClass S M
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
h : H ≤ K
x : { x // x ∈ K }
hx : ↑x ∈ H
⊢ ↑(inclusion h) { val := ↑x, property := hx } = x
cases x
no goals
case mk
G : Type u_2
G' : Type ?u.62545
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.62554
inst✝⁴ : AddGroup A
M : Type ?u.62560
S : Type u_1
inst✝³ : DivInvMonoid M
inst✝² : SetLike S M
hSM : SubgroupClass S M
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ K
hx : ↑{ val := val✝, property := property✝ } ∈ H
⊢ ↑(inclusion h) { val := ↑{ val := val✝, property := property✝ }, property := hx } =
    { val := val✝, property := property✝ }
rfl