case mk
G : Type u_2
G' : Type ?u.66281
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.66290
inst✝⁴ : AddGroup A
M : Type ?u.66296
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 K : S
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ H
⊢ ↑(↑(inclusion h) { val := val✝, property := property✝ }) = ↑{ val := val✝, property := property✝ }
G : Type u_2
G' : Type ?u.66281
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.66290
inst✝⁴ : AddGroup A
M : Type ?u.66296
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 K : S
h : H ≤ K
a : { x // x ∈ H }
⊢ ↑(↑(inclusion h) a) = ↑a
cases a
no goals
case mk
G : Type u_2
G' : Type ?u.66281
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.66290
inst✝⁴ : AddGroup A
M : Type ?u.66296
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 K : S
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ H
⊢ ↑(↑(inclusion h) { val := val✝, property := property✝ }) = ↑{ val := val✝, property := property✝ }
simp only [inclusion, MonoidHom.mk'_apply]