case mk
G : Type u_1
G' : Type ?u.156101
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.156110
inst✝ : AddGroup A
H✝ K✝ H K : Subgroup G
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ H
⊢ ↑(↑(inclusion h) { val := val✝, property := property✝ }) = ↑{ val := val✝, property := property✝ }
G : Type u_1
G' : Type ?u.156101
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.156110
inst✝ : AddGroup A
H✝ K✝ H K : Subgroup G
h : H ≤ K
a : { x // x ∈ H }
⊢ ↑(↑(inclusion h) a) = ↑a
cases a
no goals
case mk
G : Type u_1
G' : Type ?u.156101
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.156110
inst✝ : AddGroup A
H✝ K✝ H K : Subgroup G
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ H
⊢ ↑(↑(inclusion h) { val := val✝, property := property✝ }) = ↑{ val := val✝, property := property✝ }
simp only [inclusion, coe_mk, MonoidHom.mk'_apply]