awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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
inl :
  Subset (α := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p hs hμs 0 = x}
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs 0 = x})
inr :
  ∀ (hc : c ≠ 0),
    Subset (α := Set ↥(Lp E p μ))
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p hs hμs c = x}
      (closure
        {x : ↥(Lp E p μ) |
          ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
            indicatorConstLp (s := s) p ⋯ hμs c = x})
⊢ Subset (α := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p hs hμs c = x}
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs c = x})

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 𝒜
⊢ Subset (α := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p hs hμs 0 = x}
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs 0 = x})

Tactic:
Subset.trans ?_ subset_closure

Premises used: Set.Subset.trans, subset_closure
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 𝒜
inl :
  Subset (α := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p hs hμs 0 = x}
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p ⋯ hμs 0 = x}
⊢ Subset (α := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p hs hμs 0 = x}
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs 0 = x})

Tactic:
refine Subset.trans ?_ subset_closure

Premises used: Set.Subset.trans, subset_closure
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inl :
  ∀ (t : Set X) (ht : t ∈ 𝒜) (hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Membership.mem (γ := Set ↥(Lp E p μ))
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs 0 = x}
      (indicatorConstLp (s := s) p ms hμs 0)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p ⋯ hμs 0 = x}
    (indicatorConstLp (s := s) p ms hμs 0)

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

Premises used: MeasureTheory.Measure.MeasureDense.nonempty'
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p ⋯ hμs 0 = x}
    (indicatorConstLp (s := s) p ms hμs 0)

Tactic:
⟨t, ht, hμt, ?_⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
inl : Eq (α := ↥(Lp E p μ)) (indicatorConstLp (s := t) p ⋯ hμt 0) (indicatorConstLp (s := s) p ms hμs 0)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p ⋯ hμs 0 = x}
    (indicatorConstLp (s := s) p ms hμs 0)

Tactic:
refine ⟨t, ht, hμt, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ↥(Lp E p μ)) (MemLp.toLp (t.indicator fun (x : X) ↦ 0) ⋯) (MemLp.toLp (s.indicator fun (x : X) ↦ 0) ⋯)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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
⊢ LT.lt (α := ℝ≥0∞) 0 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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
⊢ 0 < p

Tactic:
have p_pos : 0 < p := lt_of_lt_of_le (by simp) one_le_p.elim
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs c = x})
    (indicatorConstLp (s := s) p ms hμs c)

Tactic:
Metric.mem_closure_iff.2 fun ε hε ↦ ?_

Premises used: Iff.mpr, Metric.mem_closure_iff
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inr :
  ∀ (ε : ℝ) (hε : ε > 0),
    ∃ (b : ↥(Lp E p μ)),
      Membership.mem (γ := Set ↥(Lp E p μ))
          {x : ↥(Lp E p μ) |
            ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
              indicatorConstLp (s := s) p ⋯ hμs c = x}
          b ∧
        dist (indicatorConstLp (s := s) p ms hμs c) b < ε
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs c = x})
    (indicatorConstLp (s := s) p ms hμs c)

Tactic:
refine Metric.mem_closure_iff.2 fun ε hε ↦ ?_

Premises used: Iff.mpr, Metric.mem_closure_iff
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
⊢ 0 < (ε / ‖c‖) ^ p.toReal

Tactic:
have aux : 0 < (ε / ‖c‖) ^ p.toReal := rpow_pos_of_pos (div_pos hε (norm_pos_iff.2 hc)) _
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
inr :
  ∀ (t : Set X) (ht : t ∈ 𝒜) (hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)),
    ∃ (b : ↥(Lp E p μ)),
      Membership.mem (γ := Set ↥(Lp E p μ))
          {x : ↥(Lp E p μ) |
            ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
              indicatorConstLp (s := s) p ⋯ hμs c = x}
          b ∧
        dist (indicatorConstLp (s := s) p ms hμs c) b < ε
⊢ ∃ (b : ↥(Lp E p μ)),
    Membership.mem (γ := Set ↥(Lp E p μ))
        {x : ↥(Lp E p μ) |
          ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
            indicatorConstLp (s := s) p ⋯ hμs c = x}
        b ∧
      dist (indicatorConstLp (s := s) 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

Premises used: Norm.norm, MeasureTheory.Measure.MeasureDense.fin_meas_approx, HDiv.hDiv, ENNReal.toReal, HPow.hPow
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ∃ (b : ↥(Lp E p μ)),
    Membership.mem (γ := Set ↥(Lp E p μ))
        {x : ↥(Lp E p μ) |
          ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
            indicatorConstLp (s := s) p ⋯ hμs c = x}
        b ∧
      dist (indicatorConstLp (s := s) p ms hμs c) b < ε

Tactic:
⟨indicatorConstLp p (h𝒜.measurable t ht) hμt c,
      ⟨t, ht, hμt, rfl⟩, ?_⟩

Premises used: MeasureTheory.indicatorConstLp, MeasureTheory.Measure.MeasureDense.measurable, And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
inr : dist (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs c) (indicatorConstLp (s := t) p ⋯ hμt c) < ε
⊢ ∃ (b : ↥(Lp E p μ)),
    Membership.mem (γ := Set ↥(Lp E p μ))
        {x : ↥(Lp E p μ) |
          ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
            indicatorConstLp (s := s) p ⋯ hμs c = x}
        b ∧
      dist (indicatorConstLp (s := s) p ms hμs c) b < ε

Tactic:
refine ⟨indicatorConstLp p (h𝒜.measurable t ht) hμt c,
      ⟨t, ht, hμt, rfl⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
inr : ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ε
⊢ dist (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs c) (indicatorConstLp (s := t) p ⋯ hμt c) < ε

Tactic:
rw [dist_indicatorConstLp_eq_norm, norm_indicatorConstLp p_pos.ne.symm p_ne_top.elim]

Premises used: MeasureTheory.norm_indicatorConstLp, Ne.symm, Fact.elim, MeasureTheory.dist_indicatorConstLp_eq_norm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ 0 < p.toReal

Tactic:
have := toReal_pos p_pos.ne.symm p_ne_top.elim
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
this : 0 < p.toReal
hbc : ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal) ≠ ∞
⊢ ‖c‖ * ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∆ t)) ^ (1 / p.toReal) <
    ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
this : 0 < p.toReal
⊢ ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal) ≠ ∞

Tactic:
ofReal_ne_top

Premises used: ENNReal.ofReal_ne_top
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
this : 0 < p.toReal
⊢ ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal) ≠ ∞

Tactic:
exact ofReal_ne_top

Premises used: ENNReal.ofReal_ne_top
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ 0 ≤ (ε / ‖c‖) ^ p.toReal

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ 0 ≤ ε / ‖c‖

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
rw : ‖c‖ * ((ε / ‖c‖) ^ p.toReal) ^ (1 / p.toReal) = ε
rw₁ : ‖c‖ * ((ε / ‖c‖) ^ p.toReal) ^ p.toReal⁻¹ = ε
rw₂ : ‖c‖ * (ε / ‖c‖) = ε
rw₃ rw₄ : ε = ε
⊢ ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) = ε

Tactic:
rw [toReal_ofReal (by positivity),
          one_div, Real.rpow_rpow_inv (by positivity) (toReal_pos p_pos.ne.symm p_ne_top.elim).ne',
          mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]

Premises used: Iff.mpr, Ne.symm, mul_div_cancel₀, ENNReal.toReal_pos, LT.lt.ne', ENNReal.toReal_ofReal, norm_ne_zero_iff, Fact.elim, one_div, Real.rpow_rpow_inv, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
have : ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal)
have₁ : ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) = ε
⊢ ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ε

Tactic:
calc
      ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal)
        < ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) := by
          have := toReal_pos p_pos.ne.symm p_ne_top.elim
          rw [measureReal_def]
          gcongr
          exact ofReal_ne_top
      _ = ε := by
        rw [toReal_ofReal (by positivity),
          one_div, Real.rpow_rpow_inv (by positivity) (toReal_pos p_pos.ne.symm p_ne_top.elim).ne',
          mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]

Premises used: Norm.norm, ENNReal.ofReal, MeasureTheory.Measure.real, HDiv.hDiv, ENNReal.toReal, HPow.hPow, OfNat.ofNat, symmDiff
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
rcases :
  ∀ (t : Set X) (t_mem : t ∈ 𝒜) (hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε),
    ∃ (t : Set X),
      Membership.mem (γ := Set (Set X))
          {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)} t ∧
        (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ (t : Set X),
    Membership.mem (γ := Set (Set X))
        {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)} t ∧
      (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
rcases Measure.MeasureDense.fin_meas_approx h𝒜 ms hμs ε ε_pos with ⟨t, t_mem, hμt, hμst⟩

Premises used: MeasureTheory.Measure.MeasureDense.fin_meas_approx
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
t_mem : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ (t : Set X),
    Membership.mem (γ := Set (Set X))
        {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)} t ∧
      (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
⟨t, ⟨t_mem, hμt⟩, hμst⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
t_mem : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ (t : Set X),
    Membership.mem (γ := Set (Set X))
        {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)} t ∧
      (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
exact ⟨t, ⟨t_mem, hμt⟩, hμst⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rw [hgen] at ms
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s t : Set X
t_mem : t ∈ 𝒜
ht : MeasurableSet t
ε : ℝ
ε_pos : 0 < ε
⊢ μ.real (t ∆ t) < ε

Tactic:
simpa