MeasureTheory.distribution_indicator_add_of_support_subset

lemma distribution_indicator_add_of_support_subset {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε]  (enorm_add : ∀ a b : ε, ‖a + b‖ₑ = ‖a‖ₑ + ‖b‖ₑ) --TODO: new type class for this property?  {f : α → ε} {c : ε} (hc : ‖c‖ₑ ≠ ⊤) {s : Set α}  (hfs : Function.support f ⊆ s) :    distribution (f + s.indicator (Function.const α c)) t μ = if t < ‖c‖ₑ then μ s else distribution f (t - ‖c‖ₑ) μ := by  unfold distribution  split_ifs with ht  · congr 1 with x    simp only [Pi.add_apply, mem_setOf_eq]    constructor    · intro h      contrapose! h      have : x ∉ support f := fun a ↦ h (hfs a)      simp_all    · intro h      rw [enorm_add, add_comm]      exact lt_add_of_lt_of_nonneg (by simpa [h]) zero_le  · push Not at ht    congr 1 with x    simp only [Pi.add_apply, mem_setOf_eq]    rw [enorm_add, ENNReal.sub_lt_iff_lt_right hc ht]    constructor    · intro h      apply h.trans_le      gcongr      unfold indicator      split_ifs <;> simp    · intro h      apply h.trans_le      gcongr      unfold indicator      split_ifs with hxs      · simp      exfalso      have : x ∉ support f := by exact fun a ↦ hxs (hfs a)      simp only [mem_support, ne_eq, not_not] at this      rw [this, enorm_zero, zero_add] at h      exact (lt_self_iff_false _).mp (h.trans_le ht)