Rmk4d10₁

lemma rmk4d10₁ {ℒ : Type*} [Nontrivial ℒ] [PartialOrder ℒ] [BoundedOrder ℒ]{S : Type*} [CompleteLattice S](μ : {p :ℒ × ℒ // p.1 < p.2} → S) :μBstar μ ≤ μAstar μ ↔  ∀ x : ℒ, (hx : x ≠ ⊤) → ∀ y : ℒ, (hy : ⊥ < y) →    μmin μ ⟨(⊥,y),hy⟩ ≤ μmax μ ⟨(x,⊤),lt_top_iff_ne_top.2 hx⟩ := by  constructor  · intro h x hx y hy    simp only [μBstar, μAstar] at h    unfold μA at h    unfold μB at h    apply sSup_le_iff.1 at h    simp only [ne_eq, Set.mem_setOf_eq, le_sInf_iff, forall_exists_index] at h    refine (((fun (x : ℒ) (hx : ¬ ⊥ = x) ↦ h (μmin μ ⟨(⊥, x), bot_lt_iff_ne_bot.2 (by tauto)⟩) <| x)      y <| ne_of_lt hy) ⟨in_TotIntvl y,ne_of_lt hy⟩ <| rfl)      (μmax μ ⟨(x, ⊤), lt_top_iff_ne_top.2 hx⟩) x ⟨in_TotIntvl x, hx⟩ rfl  · refine fun h ↦ sSup_le_iff.2 ?_    simp only [ne_eq, Set.mem_setOf_eq, forall_exists_index]    refine fun b x hx h' ↦ h' ▸ le_sInf_iff.2 ?_    simp only [ne_eq, Set.mem_setOf_eq, forall_exists_index]    exact fun _ x' _ h'' ↦ h'' ▸ h x' (by tauto) x _