case mk
G : Type u_2
G' : Type ?u.63896
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.63905
inst✝⁴ : AddGroup A
M : Type ?u.63911
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
L : S
hHK : H ≤ K
hKL : K ≤ L
val✝ : G
property✝ : val✝ ∈ H
⊢ ↑(inclusion hKL) (↑(inclusion hHK) { val := val✝, property := property✝ }) =
    ↑(inclusion (_ : H ≤ L)) { val := val✝, property := property✝ }
G : Type u_2
G' : Type ?u.63896
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.63905
inst✝⁴ : AddGroup A
M : Type ?u.63911
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
L : S
hHK : H ≤ K
hKL : K ≤ L
x : { x // x ∈ H }
⊢ ↑(inclusion hKL) (↑(inclusion hHK) x) = ↑(inclusion (_ : H ≤ L)) x
cases x
no goals
case mk
G : Type u_2
G' : Type ?u.63896
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.63905
inst✝⁴ : AddGroup A
M : Type ?u.63911
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
L : S
hHK : H ≤ K
hKL : K ≤ L
val✝ : G
property✝ : val✝ ∈ H
⊢ ↑(inclusion hKL) (↑(inclusion hHK) { val := val✝, property := property✝ }) =
    ↑(inclusion (_ : H ≤ L)) { val := val✝, property := property✝ }
rfl