Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: case refine_2.refine_1
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
⊢ ∀ (c : E) {s : Set X} (hs : MeasurableSet s) (hμs : μ s < ∞), ↑(simpleFunc.indicatorConst p hs ⋯ c) ∈ closure D

pp: case refine_2.refine_2
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
⊢ ∀ ⦃f g : X → E⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    Disjoint (Function.support f) (Function.support g) →
      MemLp.toLp f hf ∈ closure D → MemLp.toLp g hg ∈ closure D → MemLp.toLp f hf + MemLp.toLp g hg ∈ closure D

Tactic:
· intro a s ms hμs
      -- We want to approximate `a • 𝟙ₛ`.
      apply ne_of_lt at hμs
      rw [SeminormedAddCommGroup.mem_closure_iff]
      intro ε ε_pos
      have μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal) := by positivity
      -- To do so, we first pick `b ∈ u` such that `‖a - b‖ < ε / (3 * (1 + (μ s)^(1/p)))`.
      have approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal))) :=
        div_pos ε_pos (by linarith [μs_pow_nonneg])
      have ⟨b, b_mem, hb⟩ := SeminormedAddCommGroup.mem_closure_iff.1 (dense_u a) _ approx_a_pos
      -- Then we pick `t ∈ 𝒜₀` such that `‖b • 𝟙ₛ - b • 𝟙ₜ‖ < ε / 3`.
      rcases SeminormedAddCommGroup.mem_closure_iff.1
        (h𝒜₀.indicatorConstLp_subset_closure p b ⟨s, ms, hμs, rfl⟩)
          (ε / 3) (by linarith [ε_pos]) with ⟨-, ⟨t, ht, hμt, rfl⟩, hst⟩
      have mt := h𝒜₀.measurable t ht
      -- We now show that `‖a • 𝟙ₛ - b • 𝟙ₜ‖ₚ < ε`, as follows:
      -- `‖a • 𝟙ₛ - b • 𝟙ₜ‖ₚ`
      --   `= ‖a • 𝟙ₛ - b • 𝟙ₛ + b • 𝟙ₛ - b • 𝟙ₜ‖ₚ`
      --   `≤ ‖a - b‖ * ‖𝟙ₛ‖ₚ + ε / 3`
      --   `= ‖a - b‖ * (μ s)^(1/p) + ε / 3`
      --   `< ε * (μ s)^(1/p) / (3 * (1 + (μ s)^(1/p))) + ε / 3`
      --   `≤ ε / 3 + ε / 3 < ε`.
      refine ⟨indicatorConstLp p mt hμt b,
        ⟨1, fun _ ↦ ⟨b, b_mem⟩, fun _ ↦ ⟨t, ht⟩, by simp [key]⟩, ?_⟩
      rw [Lp.simpleFunc.coe_indicatorConst,
        ← sub_add_sub_cancel _ (indicatorConstLp p ms hμs b), ← add_halves ε]
      refine lt_of_le_of_lt (b := ε / 3 + ε / 3) (norm_add_le_of_le ?_ hst.le) (by linarith [ε_pos])
      rw [indicatorConstLp_sub, norm_indicatorConstLp p_ne_zero p_ne_top.elim]
      calc
        ‖a - b‖ * μ.real s ^ (1 / p.toReal)
          ≤ (ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))) * μ.real s ^ (1 / p.toReal) :=
              mul_le_mul_of_nonneg_right (le_of_lt hb) μs_pow_nonneg
        _ ≤ ε / 3 := by
            rw [← mul_one (ε / 3), div_mul_eq_div_mul_one_div, mul_assoc, one_div_mul_eq_div]
            exact mul_le_mul_of_nonneg_left
              ((div_le_one (by linarith [μs_pow_nonneg])).2 (by linarith))
              (by linarith [ε_pos])

Goal state after:
case refine_2.refine_2
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
⊢ ∀ ⦃f g : X → E⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    Disjoint (Function.support f) (Function.support g) →
      MemLp.toLp f hf ∈ closure D → MemLp.toLp g hg ∈ closure D → MemLp.toLp f hf + MemLp.toLp g hg ∈ closure D