MeasureTheory.AESublinearOn.biSup2

lemma biSup2 {ι : Type*} {𝓑 : Set ι} (h𝓑 : 𝓑.Countable) {T : ι → (α → ε₁) → α' → ℝ≥0∞}    {P : (α → ε₁) → Prop} {Q : (α → ε₁) → Prop}    (hPT : ∀ (u : α → ε₁), P u → ∀ᵐ x ∂ν, ⨆ i ∈ 𝓑, T i u x ≠ ∞)    (hQT : ∀ (u : α → ε₁), Q u → ∀ᵐ x ∂ν, ⨆ i ∈ 𝓑, T i u x ≠ ∞)    (P0 : P 0)    (Q0 : Q 0)    (haP : ∀ {f g : α → ε₁}, P f → P g → P (f + g))    (haQ : ∀ {f g : α → ε₁}, Q f → Q g → Q (f + g))    (hsP : ∀ {f : α → ε₁} {c : ℝ≥0}, P f → P (c • f))    (hsQ : ∀ {f : α → ε₁} {c : ℝ≥0}, Q f → Q (c • f))    {A : ℝ≥0} -- todo, here and elsewhere: probably better to have {A : ℝ≥0∞} (hA : A ≠ ⊤)    (hAP : ∀ i ∈ 𝓑,      AESublinearOn (T i) (fun g ↦ g ∈ {f | P f} + {f | Q f}) A ν) :    AESublinearOn (fun u x ↦ ⨆ i ∈ 𝓑, T i u x) (fun f ↦ P f ∨ Q f) A ν := by  set R := fun g ↦ g ∈ {f | P f} + {f | Q f}  have hPR : ∀ {f}, P f → R f := fun hu ↦ ⟨_, hu, 0, Q0, by simp⟩  have hQR : ∀ {f}, Q f → R f := fun hu ↦ ⟨0, P0, _, hu, by simp⟩  apply AESublinearOn.antitone (P' := R) (fun hu ↦ hu.elim hPR hQR)  refine AESublinearOn.biSup (P := R) h𝓑 ?_ ?_ ?_ hAP  · rintro _ ⟨f, hf, g, hg, rfl⟩    filter_upwards [hPT f hf, hQT g hg,      AESubadditiveOn.forall_le h𝓑 (fun i hi ↦ hAP i hi |>.1) (hPR hf) (hQR hg)] with x hfx hgx hTx    simp_rw [← lt_top_iff_ne_top] at hfx hgx ⊢    simp_rw [enorm_eq_self] at hTx    calc      _ ≤ ⨆ i ∈ 𝓑, A * (T i f x + T i g x) := by gcongr; exact hTx _ ‹_›      _ ≤ A * ((⨆ i ∈ 𝓑, T i f x) + (⨆ i ∈ 𝓑, T i g x)) := by          simp_rw [← ENNReal.mul_iSup]          gcongr          -- todo: make lemma          simp_rw [iSup_le_iff]          intro i hi          gcongr <;> apply le_biSup _ hi      _ < ⊤ := mul_lt_top coe_lt_top <| add_lt_top.mpr ⟨hfx, hgx⟩  · rintro _ _ ⟨f₁, hf₁, g₁, hg₁, rfl⟩ ⟨f₂, hf₂, g₂, hg₂, rfl⟩    exact ⟨f₁ + f₂, haP hf₁ hf₂, g₁ + g₂, haQ hg₁ hg₂, by dsimp only; abel_nf⟩  · rintro _ c ⟨f, hf, g, hg, rfl⟩    exact ⟨c • f, hsP hf, c • g, hsQ hg, by module⟩