-- Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
theorem Measure.MeasureDense.indicatorConstLp_subset_closure (h𝒜 : μ.MeasureDense 𝒜) (c : E) :
    {indicatorConstLp p hs hμs c | (s : Set X) (hs : MeasurableSet s) (hμs : μ s ≠ ∞)} ⊆
    closure {indicatorConstLp p (h𝒜.measurable s hs) hμs c |
      (s : Set X) (hs : s ∈ 𝒜) (hμs : μ s ≠ ∞)}

Proof state:
case inl.intro.intro.intro
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)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ indicatorConstLp p ms hμs 0 ∈ {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs 0 = x}

Tactic:
obtain ⟨t, ht, hμt⟩ := h𝒜.nonempty'

Result:
case inl.intro.intro.intro.intro.intro
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)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
⊢ indicatorConstLp p ms hμs 0 ∈ {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs 0 = x}

Proof state:
case inr.intro.intro.intro
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
⊢ ∃ b ∈ {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs c = x},
    dist (indicatorConstLp p ms hμs c) b < ε

Tactic:
obtain ⟨t, ht, hμt, hμst⟩ := h𝒜.fin_meas_approx ms hμs ((ε / ‖c‖) ^ p.toReal) aux

Result:
case inr.intro.intro.intro.intro.intro.intro
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ∃ b ∈ {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs c = x},
    dist (indicatorConstLp p ms hμs c) b < ε

Proof state:
case inl.intro.intro.intro.intro.intro.e_f
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)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
⊢ (t.indicator fun x => 0) = s.indicator fun x => 0

Tactic:
simp

Result:
no goals

Proof state:
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ 0 ≤ (μ (s ∆ t)).toReal

Tactic:
simp

Result:
no goals

Proof state:
case inr
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), indicatorConstLp p hs hμs c = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs c = x}

Tactic:
have p_pos : 0 < p := lt_of_lt_of_le (by norm_num) one_le_p.elim

Result:
case inr
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), indicatorConstLp p hs hμs c = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs c = x}

Proof state:
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ (μ (s ∆ t)).toReal ^ (1 / p.toReal) < (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal)

Tactic:
refine Real.rpow_lt_rpow (by simp) ?_
  (one_div_pos.2 <| toReal_pos p_pos.ne.symm p_ne_top.elim)

Result:
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ (μ (s ∆ t)).toReal < (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal

Proof state:
case inr
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), indicatorConstLp p hs hμs c = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs c = x}

Tactic:
rintro - ⟨s, ms, hμs, rfl⟩

Result:
case inr.intro.intro.intro
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ indicatorConstLp p ms hμs c ∈ closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs c = x}

Proof state:
case inr.intro.intro.intro.intro.intro.intro
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖c‖ * (μ (s ∆ t)).toReal ^ (1 / p.toReal) < ε

Tactic:
calc
  ‖c‖ * (μ (s ∆ t)).toReal ^ (1 / p.toReal)
    < ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) := by
      rw [_root_.mul_lt_mul_left (norm_pos_iff.2 hc)]
      refine Real.rpow_lt_rpow (by simp) ?_
        (one_div_pos.2 <| toReal_pos p_pos.ne.symm p_ne_top.elim)
      rwa [toReal_lt_toReal (measure_symmDiff_ne_top hμs hμt) ofReal_ne_top]
  _ = ε := by
    rw [toReal_ofReal (rpow_nonneg (div_nonneg hε.le (norm_nonneg _)) _),
      one_div, Real.rpow_rpow_inv (div_nonneg hε.le (norm_nonneg _))
        (toReal_pos p_pos.ne.symm p_ne_top.elim).ne.symm,
      mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]

Result:
no goals

Proof state:
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ (μ (s ∆ t)).toReal < (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal

Tactic:
rwa [toReal_lt_toReal (measure_symmDiff_ne_top hμs hμt) ofReal_ne_top]

Result:
no goals