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