Prop2d6₃I

lemma prop2d6₃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)  (z : ℒ) (hzI : InIntvl I z)  (h : x < y ∧ y < z)  (h' : (IsComparable (μA μ ⟨(x, y), h.1⟩) (μA μ ⟨(y, z), h.2⟩)) ∨        (IsAttained μ ⟨(x, z), lt_trans h.1 h.2⟩)) :  μA μ ⟨(y, z), h.2⟩ = μA μ ⟨(x, z), lt_trans h.1 h.2⟩ ∨  (μA μ ⟨(x, y), h.1⟩ ≤ μA μ ⟨(x, z), lt_trans h.1 h.2⟩ ∧   μA μ ⟨(x, z), lt_trans h.1 h.2⟩ < μA μ ⟨(y, z), h.2⟩) := by  rcases h' with h₁ | h₂  · apply comparable_iff (μA μ ⟨(x, y), h.1⟩) (μA μ ⟨(y, z), h.2⟩) at h₁    by_cases h₂ : μA μ ⟨(y, z), h.2⟩ = μA μ ⟨(x, z), lt_trans h.1 h.2⟩    · exact Or.inl h₂    · have h₃ : μA μ ⟨(x, y), h.1⟩ < μA μ ⟨(y, z), h.2⟩ := Or.resolve_right h₁ (fun hcontra ↦      h₂ (prop2d6₂I₁ I μ hμcvx x hxI y hyI z hzI h hcontra))      have h₄ : μA μ ⟨(x, y), h.1⟩ ≤ μA μ ⟨(x, z), lt_trans h.1 h.2⟩ ∧        μA μ ⟨(x, z), lt_trans h.1 h.2⟩ ≤ μA μ ⟨(y, z), h.2⟩ :=          prop2d6₂I₂ I μ hμcvx x hxI y hyI z hzI h h₃      exact Or.inr ⟨h₄.1, lt_of_le_of_ne h₄.2 (Ne.symm h₂)⟩  · rcases h₂ with ⟨a, ⟨ha₁, ⟨ha₂, hres⟩⟩⟩    apply or_iff_not_imp_left.2    intro hnot    have h' : ¬ y ≤ a := by      by_contra hcontra      have h''' : μA μ ⟨(y, z), h.2⟩ ≤ μmax μ ⟨(a, z), lt_of_le_of_ne ha₁.2 ha₂⟩ := by          apply sInf_le          use a , ⟨⟨hcontra, ha₁.2⟩, ha₂⟩      exact hnot <| eq_of_le_of_ge (hres ▸ h''') <| prop2d6₀ μ x y z h    exact ⟨hres ▸ (le_trans (lem2d4₁ μ y a h' x (le_inf (le_of_lt h.1) ha₁.1)) <|      lem2d4₂I I μ hμcvx y hyI a ⟨le_trans hxI.1 ha₁.1, le_trans ha₁.2 hzI.2⟩ h' z <|      sup_le (le_of_lt h.2) ha₁.2),lt_of_le_of_ne (prop2d6₀ μ x y z h) <| Ne.symm hnot⟩