Prop4d8

lemma prop4d8 {ℒ : Type*} [Nontrivial ℒ] [PartialOrder ℒ] [BoundedOrder ℒ]{V : Type*} [TotallyOrderedRealVectorSpace V] [Nontrivial V](r : {p :ℒ × ℒ // p.1 < p.2} → NNReal)(d : {p :ℒ × ℒ // p.1 < p.2} → V)(h₁ : ∀ (x y z : ℒ), (h : x < y ∧ y < z) → d ⟨(x, z), lt_trans h.1 h.2⟩ = d ⟨(x, y), h.1⟩ +  d ⟨(y, z), h.2⟩ ∧ r ⟨(x, z), lt_trans h.1 h.2⟩ = r ⟨(x, y), h.1⟩ + r ⟨(y, z), h.2⟩)(h₂ : ∀ (x y : ℒ), (h : x < y) → r ⟨(x, y), h⟩ = 0 → d ⟨(x, y), h⟩ > 0): SlopeLike (μQuotient r d) := by  have smul_lt_smul_iff_pos {c : NNReal} (hc : c > 0) (b₁ b₂ : V) :      c • b₁ < c • b₂ ↔ b₁ < b₂ := by    have hc' : (0 : ℝ) < (c : ℝ) := NNReal.coe_pos.mpr hc    simpa [NNReal.smul_def] using smul_lt_smul_iff_of_pos_left hc'  have smul_lt_smul_pos {c : NNReal} {b₁ b₂ : V} (hb : b₁ < b₂) (hc : c > 0) : c • b₁ < c • b₂ :=    (smul_lt_smul_iff_pos hc b₁ b₂).2 hb  let μ := μQuotient r d  refine (prop4d6 μ).2 fun x y z h ↦ ?_  rcases eq_zero_or_pos (r ⟨(x, z), lt_trans h.1 h.2⟩) with h' | h'  · have : r ⟨(x, y), h.1⟩ = 0 ∧ r ⟨(y, z), h.2⟩ = 0 := add_eq_zero.1 <| (h₁ x y z h).2 ▸ h'    have : ¬ r ⟨(y, z), h.2⟩ > 0 ∧ ¬ r ⟨(x,y), h.1⟩ > 0 := by      constructor      · rw [this.2]        exact not_lt_zero      · rw [this.1]        exact not_lt_zero    have : μ ⟨(x, z), lt_trans h.1 h.2⟩ = ⊤ ∧ μ ⟨(x, y), h.1⟩ = ⊤ ∧ μ ⟨(y, z), h.2⟩ = ⊤ := by      refine ⟨?_,⟨?_,?_⟩⟩      · simp only [μQuotient, h', gt_iff_lt, lt_self_iff_false, ↓reduceDIte, μ]      · simp only [μQuotient, gt_iff_lt, this.2, ↓reduceDIte, μ]      · simp only [μQuotient, gt_iff_lt, this.1, ↓reduceDIte, μ]    aesop  · by_cases h'' : r ⟨(x, y), h.1⟩ > 0 ∧ r ⟨(y, z), h.2⟩ > 0    · rcases μQuotient_helper r d ⟨(x, y), h.1⟩ h''.1 with ⟨μxy,⟨hxy₁,hxy₂⟩⟩      rcases μQuotient_helper r d ⟨(y, z), h.2⟩ h''.2 with ⟨μyz,⟨hyz₁,hyz₂⟩⟩      rcases μQuotient_helper r d ⟨(x, z), lt_trans h.1 h.2⟩ h' with ⟨μxz,⟨hxz₁,hxz₂⟩⟩      have := add_smul (r ⟨(x, y), h.1⟩) (r ⟨(y, z), h.2⟩) μxz ▸ (h₁ x y z h).2 ▸        hxy₂ ▸ hyz₂ ▸ hxz₂ ▸ (h₁ x y z h).1      simp only [hxy₁, hxz₁, OrderEmbedding.lt_iff_lt, hyz₁, gt_iff_lt,        EmbeddingLike.apply_eq_iff_eq, μ]      by_cases hs : μxy < μxz      · exact Or.inl ⟨hs,(smul_lt_smul_iff_pos h''.2 _ _).1 <|          (add_lt_add_iff_left <| r ⟨(x, y), h.1⟩ • μxy).1 <| lt_sub_iff_add_lt.1 <|          (eq_sub_of_add_eq this) ▸ (smul_lt_smul_iff_pos h''.1 _ _).2 hs⟩      · by_cases hs' : μxy = μxz        · refine Or.inr <| Or.inr <| ⟨hs',?_⟩          rw [hs'] at this          have h_eq : r ⟨(y, z), h.2⟩ • μxz = r ⟨(y, z), h.2⟩ • μyz :=            (add_right_inj (r ⟨(x, y), h.1⟩ • μxz)).mp this          have hμ_eq : μxz = μyz := by            by_contra! hne            have hlt : μxz < μyz ∨ μyz < μxz := lt_or_gt_of_ne hne            rcases hlt with (hlt | hlt)            · exact (smul_lt_smul_pos hlt h''.2).ne h_eq            · exact (smul_lt_smul_pos hlt h''.2).ne h_eq.symm          exact hμ_eq        · have hs' : μxz < μxy := lt_of_not_ge (Eq.mpr (id (congrArg (fun _a ↦ ¬_a)            (propext le_iff_eq_or_lt))) (not_or.mpr ⟨hs', hs⟩))          exact Or.inr <| Or.inl <| ⟨hs',(smul_lt_smul_iff_pos h''.2 _ _).1 <|            (add_lt_add_iff_left <| r ⟨(x, y), h.1⟩ • μxy).1 <| sub_lt_iff_lt_add.1 <|            (eq_sub_of_add_eq this) ▸ (smul_lt_smul_iff_pos h''.1 _ _).2 hs'⟩    · by_cases h''' : r ⟨(x, y), h.1⟩ = 0 ∧ r ⟨(y, z), h.2⟩ > 0      · have h2 : μ ⟨(x, y), h.1⟩ = ⊤ := by simp only [μQuotient, h'''.1, gt_iff_lt,        lt_self_iff_false, ↓reduceDIte, μ]        have h4 := (zero_add <| r ⟨(y, z), h.2⟩) ▸ h'''.1 ▸ (h₁ x y z h).2        rcases le_iff_eq_or_lt.1 (h2 ▸ le_top : μ ⟨(x, z), lt_trans h.1 h.2⟩ ≤ μ ⟨(x, y), h.1⟩)          with h3 | h3        · rcases μQuotient_helper r d ⟨(x,z),lt_trans h.1 h.2⟩ (h4 ▸ h'''.2) with ⟨w,⟨hw₁,_⟩⟩          simp only [μ] at h3; simp only [μ] at h2          exact False.elim (not_top_lt ((h2 ▸ h3 ▸ hw₁).symm ▸            not_top_of_Nontrivial_TotallyOrderedRealVectorSpace w))        · refine Or.inr <| Or.inl <| ⟨h3,?_⟩          simp only [μQuotient, gt_iff_lt, Eq.mpr (id (congrArg (fun _a ↦ _a > 0) h4)) h'''.right,            ↓reduceDIte, Function.Embedding.toFun_eq_coe, RelEmbedding.coe_toEmbedding, h'''.2,            OrderEmbedding.lt_iff_lt, μ]          exact h4 ▸ ((smul_lt_smul_iff_pos (by exact Right.inv_pos.mpr h') _ _).2 <|            (h₁ x y z h).1 ▸ lt_add_of_pos_left (d ⟨(y, z), h.right⟩) <| h₂ x y h.1 h'''.1)      · apply not_and_or.1 at h''        apply not_and_or.1 at h'''        simp only [pos_iff_ne_zero.symm, gt_iff_lt, not_lt, nonpos_iff_eq_zero] at h'''        have : r ⟨(y, z), h.2⟩ = 0 := by aesop        have this' := (add_zero <| r ⟨(x, y), h.1⟩) ▸ (this ▸ (h₁ x y z h).2) ▸ h'        have h2 : μ ⟨(y, z), h.2⟩ = ⊤ := by simp only [μQuotient, this, gt_iff_lt,          lt_self_iff_false, ↓reduceDIte, μ]        have h4 := (add_zero <| r ⟨(x, y), h.1⟩) ▸ this ▸ (h₁ x y z h).2        rcases le_iff_eq_or_lt.1 (h2 ▸ le_top : μ ⟨(x, z), lt_trans h.1 h.2⟩ ≤ μ ⟨(y, z), h.2⟩)          with h3 | h3        · rcases μQuotient_helper r d ⟨(x,z),lt_trans h.1 h.2⟩ (h4 ▸ this') with ⟨w,hw₁,_⟩          simp only [μ] at h3; simp only [μ] at h2          exact False.elim (not_top_lt            ((h2 ▸ h3 ▸ hw₁).symm ▸ not_top_of_Nontrivial_TotallyOrderedRealVectorSpace w))        · refine Or.inl <| ⟨?_,h3⟩          simp only [μQuotient, gt_iff_lt, this', ↓reduceDIte, Function.Embedding.toFun_eq_coe,            RelEmbedding.coe_toEmbedding, Eq.mpr (id (congrArg (fun _a ↦ _a > 0) h4)),            OrderEmbedding.lt_iff_lt, μ]          exact h4 ▸ ((smul_lt_smul_iff_pos (by exact Right.inv_pos.mpr h') _ _).2 <|            (h₁ x y z h).1 ▸ lt_add_of_pos_right (d ⟨(x, y), h.1⟩) <| h₂ y z h.2 this)