Prop2d8₂I

lemma prop2d8₂I  (I : {p : ℒ × ℒ // p.1 < p.2})  (μ : {p :ℒ × ℒ // p.1 < p.2} → S) (hμcvx : ConvexI I μ)  (x : ℒ) (hxI : InIntvl I x)  (y : ℒ) (hyI : InIntvl I y)  (u : ℒ) (huI : InIntvl I u)  (h : u < x ∧ u < y)  (hcpb : IsComparable (μA μ ⟨(u, x), h.1⟩)  (μA μ ⟨(u, y), h.2⟩) ∨ IsAttained μ ⟨(u, x ⊔ y), lt_sup_of_lt_left h.1⟩) :  μA μ ⟨(u, x), h.1⟩ ≤ μA μ ⟨(u, x ⊔ y), lt_sup_of_lt_left h.1⟩ ∨  μA μ ⟨(u, y), h.2⟩ ≤ μA μ ⟨(u, x ⊔ y), lt_sup_of_lt_left h.1⟩ := by  rcases hcpb with h₁ | h₂  · rcases h₁ with h₃ | h₄    · exact Or.inl <| (inf_eq_left.2 h₃).symm ▸ (prop2d8₁I I μ hμcvx x hxI y hyI u huI h)    · have h' : μA μ ⟨(u, x), h.1⟩ ⊓ μA μ ⟨(u, y), h.2⟩ ≤ μA μ ⟨(u, x ⊔ y), lt_sup_of_lt_left h.1⟩        := prop2d8₁I I μ hμcvx x hxI y hyI u huI h      rw [inf_comm] at h'      exact Or.inr <| (inf_eq_left.2 h₄).symm ▸ h'  · rcases h₂ with ⟨a, ha, ⟨ha',ha''⟩⟩    exact ha'' ▸ (prop2d8₀I I μ hμcvx x hxI y hyI u h a ⟨le_trans huI.1 ha.1, le_trans ha.2 <|      sup_le hxI.2 hyI.2⟩ ⟨ha.1,lt_of_le_of_ne ha.2 ha'⟩)