MeasureTheory.distribution_mono_left

@[gcongr only]lemma distribution_mono_left (h : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) :    distribution f t μ ≤ distribution g t μ := by  have h₀ : {x | t < ‖f x‖ₑ} \ {x | t < ‖g x‖ₑ} ⊆ {x | ¬‖f x‖ₑ ≤ ‖g x‖ₑ} := fun x ↦ by    simp_rw [Set.mem_sdiff, mem_setOf_eq, not_lt, not_le, and_imp]    intro i₁ i₂; simpa using i₂.trans_lt i₁  calc    _ ≤ μ ({x | t < ‖f x‖ₑ} ∩ {x | t < ‖g x‖ₑ})      + μ ({x | t < ‖f x‖ₑ} \ {x | t < ‖g x‖ₑ}) := measure_le_inter_add_sdiff μ _ _    _ = μ ({x | t < ‖f x‖ₑ} ∩ {x | t < ‖g x‖ₑ}) := by rw [measure_mono_null h₀ h, add_zero]    _ ≤ _ := by apply measure_mono; simp