case mk
α : Type u_1
β : Type ?u.8882
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x val✝ : α
property✝ : val✝ ∈ Icc a b
⊢ projIcc a b h ↑{ val := val✝, property := property✝ } = { val := val✝, property := property✝ }
α : Type u_1
β : Type ?u.8882
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
x : ↑(Icc a b)
⊢ projIcc a b h ↑x = x
cases x
no goals
case mk
α : Type u_1
β : Type ?u.8882
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x val✝ : α
property✝ : val✝ ∈ Icc a b
⊢ projIcc a b h ↑{ val := val✝, property := property✝ } = { val := val✝, property := property✝ }
apply projIcc_of_mem