α : Type u_1
β : Type ?u.3590
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
x : α
h : a < b
h' : projIcc a b (_ : a ≤ b) x = { val := a, property := (_ : a ∈ Icc a b) }
⊢ x ≤ a
α : Type u_1
β : Type ?u.3590
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
x : α
h : a < b
⊢ projIcc a b (_ : a ≤ b) x = { val := a, property := (_ : a ∈ Icc a b) } ↔ x ≤ a
refine' ⟨fun h' => _, projIcc_of_le_left _⟩
α : Type u_1
β : Type ?u.3590
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
x : α
h : a < b
h' : x ≤ a
⊢ x ≤ a
α : Type u_1
β : Type ?u.3590
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
x : α
h : a < b
h' : projIcc a b (_ : a ≤ b) x = { val := a, property := (_ : a ∈ Icc a b) }
⊢ x ≤ a
simp_rw [Subtype.ext_iff_val, projIcc, max_eq_left_iff, min_le_iff, h.not_le, false_or_iff] at h'
no goals
α : Type u_1
β : Type ?u.3590
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
x : α
h : a < b
h' : x ≤ a
⊢ x ≤ a
exact h'