Lem2d4₂I

lemma lem2d4₂I  (I : {p : ℒ × ℒ // p.1 < p.2})  (μ : {p :ℒ × ℒ // p.1 < p.2} → S) (hμcvx : ConvexI I μ)  (x : ℒ) (hxI : InIntvl I x)  (w : ℒ) (hwI : InIntvl I w)  (hxw : ¬ x ≤ w)  (t : ℒ)  (hxwt : x ⊔ w ≤ t) :  μmax μ ⟨(x ⊓ w, x), inf_lt_left.2 hxw⟩ ≤    μmax μ ⟨(w, t), lt_of_le_of_lt' hxwt <| right_lt_sup.2 hxw⟩ := by    let target := μmax μ ⟨(w, t), lt_of_le_of_lt' hxwt <| right_lt_sup.2 hxw⟩    have h : ∀ b : ℒ, (h' : x ⊓ w < b ∧ b ≤ x) → μ ⟨(x ⊓ w, b), h'.1⟩ ≤ target := by      intro b hb      have hh : x ⊓ w = b ⊓ w := by        refine le_antisymm ?_ <| inf_le_inf_right w hb.2        nth_rw 1 [← inf_idem w, ← inf_assoc]        exact inf_le_inf_right w <| le_of_lt hb.1      simp only [hh, ge_iff_le]      have hbnlew : ¬ b ≤ w := inf_lt_left.mp        ((congrArg (fun _a ↦ _a < b) (hh.symm)) ▸ hb.1)      have hfinal : μ ⟨(w, b ⊔ w), right_lt_sup.mpr hbnlew⟩ ≤ target := by        apply le_sSup        use b ⊔ w, ⟨⟨le_sup_right, le_trans (sup_le_sup_right hb.2 w) hxwt⟩,          (mt right_eq_sup.1) <| inf_lt_left.1 <| hh.symm ▸ hb.1⟩      apply le_trans (hμcvx.convex b w ⟨le_of_lt (lt_of_le_of_lt (le_inf hxI.1 hwI.1) hb.1),         le_trans hb.2 hxI.2⟩ hwI hbnlew) hfinal    apply sSup_le    rintro b ⟨w_1, ⟨hf₁, hf₂⟩⟩    rw [hf₂.symm]    exact h w_1 ⟨lt_of_le_of_ne hf₁.1.1 hf₁.2, hf₁.1.2⟩