awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
fn : ℕ → SimpleFunc α E
hfn :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
hfn_lim : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (f x))
n : ℕ
this :
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)

Tactic:
have := h'f (Function.support (fn n)) (fn n).measurableSet_support (by positivity)
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
fn : ℕ → SimpleFunc α E
hfn :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
hfn_lim : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (f x))
n : ℕ
this_1 :
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
this :
  LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
⊢ False

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
fn : ℕ → SimpleFunc α E
hfn :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
hfn_lim : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (f x))
⊢ ∀ (n : ℕ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
have A n : μ (Function.support (fn n)) = 0 := by
    by_contra!
    have := h'f (Function.support (fn n)) (fn n).measurableSet_support (by positivity)
    grind
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
fn : ℕ → SimpleFunc α E
hfn :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
hfn_lim : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (f x))
A :
  ∀ (n : ℕ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) ((fn n : (a : α) → E) x : E) (0 : E)

Tactic:
have B : ∀ᵐ x ∂μ, ∀ n, fn n x = 0 := ae_all_iff.mpr A
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
fn : ℕ → SimpleFunc α E
hfn :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
hfn_lim : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (f x))
A :
  ∀ (n : ℕ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (0 : ℝ≥0∞)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) ((fn n : (a : α) → E) x : E) (0 : E)
h : ∀ (x : α) (hx : ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) ((fn n : (a : α) → E) x : E) (0 : E)), f x = 0 x
⊢ f =ᶠ[ae μ] 0

Tactic:
filter_upwards [B] with x hx
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
fn : ℕ → SimpleFunc α E
hfn :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
hfn_lim : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (f x))
A :
  ∀ (n : ℕ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (0 : ℝ≥0∞)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) ((fn n : (a : α) → E) x : E) (0 : E)
x : α
hx : ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) ((fn n : (a : α) → E) x : E) (0 : E)
h : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (0 x))
⊢ f x = 0 x

Tactic:
apply tendsto_nhds_unique (hfn_lim x)

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
fn : ℕ → SimpleFunc α E
hfn :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
hfn_lim : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (f x))
A :
  ∀ (n : ℕ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (0 : ℝ≥0∞)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) ((fn n : (a : α) → E) x : E) (0 : E)
x : α
hx : ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) ((fn n : (a : α) → E) x : E) (0 : E)
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (0 x))

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : AEFinStronglyMeasurable f μ
h'f : ¬f =ᶠ[ae μ] 0
apply : ¬AEFinStronglyMeasurable.mk f hf =ᶠ[ae μ] 0
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply hf.finStronglyMeasurable_mk.exists_measurableSet_measure_pos_lt_top

Premises used: MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk, MeasureTheory.FinStronglyMeasurable.exists_measurableSet_measure_pos_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : AEFinStronglyMeasurable f μ
h'f : ¬f =ᶠ[ae μ] 0
contrapose! : ∀ (h'f : AEFinStronglyMeasurable.mk f hf =ᶠ[ae μ] 0), f =ᶠ[ae μ] 0
⊢ ¬AEFinStronglyMeasurable.mk f hf =ᶠ[ae μ] 0

Tactic:
contrapose! h'f
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : AEFinStronglyMeasurable f μ
h'f : AEFinStronglyMeasurable.mk f hf =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] 0

Tactic:
hf.ae_eq_mk.trans h'f

Premises used: Filter.EventuallyEq.trans, MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : AEFinStronglyMeasurable f μ
h'f : AEFinStronglyMeasurable.mk f hf =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] 0

Tactic:
exact hf.ae_eq_mk.trans h'f

Premises used: Filter.EventuallyEq.trans, MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
⊢ ∃ (f : ↥(Lp E p μ)), f ≠ 0

Tactic:
exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
obtain : ∀ (f : ↥(Lp E p μ)) (hf : f ≠ 0), Nontrivial.{u_1} ↥(Lp ℝ p μ)
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)

Tactic:
obtain ⟨f, hf⟩ : ∃ f : Lp E p μ, f ≠ 0 := exists_ne 0

Premises used: exists_ne, MeasureTheory.Lp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
contrapose! : ∀ (hf : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0), f = 0
⊢ ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0

Tactic:
contrapose! hf
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] E) : α → E)
⊢ f = 0

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 (↑(↑0 : α →ₘ[μ] E) : α → E)
h₁ h₂ : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] E) : α → E)

Tactic:
grw [hf, Lp.coeFn_zero E p μ]

Premises used: MeasureTheory.Lp.coeFn_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
⊢ ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0

Tactic:
have hfne : ¬ (f =ᵐ[μ] 0) := by
    contrapose! hf
    ext
    grw [hf, Lp.coeFn_zero E p μ]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
inl :
  ∀ [Nontrivial ↥(Lp E ∞ μ)] (f : ↥(Lp E ∞ μ)) (hf : f ≠ 0) (hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0),
    Nontrivial.{u_1} ↥(Lp ℝ ∞ μ)
inr : ∀ (h'p : p < ∞), Nontrivial.{u_1} ↥(Lp ℝ p μ)
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)

Tactic:
rcases eq_top_or_lt_top p with rfl | h'p

Premises used: eq_top_or_lt_top, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E ∞ μ)
f : ↥(Lp E ∞ μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
inl : Ne.{u_1 + 1} (α := ↥(Lp ℝ ∞ μ)) (MemLp.toLp (fun (x : α) ↦ 1) ⋯) 0
⊢ Nontrivial.{u_1} ↥(Lp ℝ ∞ μ)

Tactic:
apply nontrivial_of_ne ((memLp_top_const (1 : ℝ)).toLp _) 0

Premises used: nontrivial_of_ne, MeasureTheory.MemLp.toLp, OfNat.ofNat, MeasureTheory.memLp_top_const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E ∞ μ)
f : ↥(Lp E ∞ μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
inl :
  ∀ (hfne : Eq.{u_1 + 1} (α := ↥(Lp ℝ ∞ μ)) (MemLp.toLp (fun (x : α) ↦ 1) ⋯) 0), (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
⊢ Ne.{u_1 + 1} (α := ↥(Lp ℝ ∞ μ)) (MemLp.toLp (fun (x : α) ↦ 1) ⋯) 0

Tactic:
contrapose! hfne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E ∞ μ)
f : ↥(Lp E ∞ μ)
hf : f ≠ 0
hfne : Eq.{u_1 + 1} (α := ↥(Lp ℝ ∞ μ)) (MemLp.toLp (fun (x : α) ↦ 1) ⋯) 0
⊢ (ae μ).EventuallyEq (β := ℝ) (↑(↑(MemLp.toLp (fun (x : α) ↦ 1) ⋯) : α →ₘ[μ] ℝ) : α → ℝ) (↑(↑0 : α →ₘ[μ] ℝ) : α → ℝ)

Tactic:
have := Lp.ext_iff.1 hfne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E ∞ μ)
f : ↥(Lp E ∞ μ)
hf : f ≠ 0
hfne : Eq.{u_1 + 1} (α := ↥(Lp ℝ ∞ μ)) (MemLp.toLp (fun (x : α) ↦ 1) ⋯) 0
this :
  (ae μ).EventuallyEq (β := ℝ) (↑(↑(MemLp.toLp (fun (x : α) ↦ 1) ⋯) : α →ₘ[μ] ℝ) : α → ℝ) (↑(↑0 : α →ₘ[μ] ℝ) : α → ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ 1) 0

Tactic:
grw [Lp.coeFn_zero, MemLp.coeFn_toLp] at this

Premises used: MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.Lp.coeFn_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E ∞ μ)
f : ↥(Lp E ∞ μ)
hf : f ≠ 0
hfne : Eq.{u_1 + 1} (α := ↥(Lp ℝ ∞ μ)) (MemLp.toLp (fun (x : α) ↦ 1) ⋯) 0
this : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ 1) 0
x : α
hx : Eq (α := ℝ) 1 (0 x)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) x = 0 x

Tactic:
simp at hx
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E ∞ μ)
f : ↥(Lp E ∞ μ)
hf : f ≠ 0
hfne : Eq.{u_1 + 1} (α := ↥(Lp ℝ ∞ μ)) (MemLp.toLp (fun (x : α) ↦ 1) ⋯) 0
this : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ 1) 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Eq (α := ℝ) ((fun (x : α) ↦ (1 : ℝ)) x) (0 x)) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (↑(↑f : α →ₘ[μ] E) : α → E) x = 0 x) x} x}
      a
h₁ h₂ : ∀ (x : α) (hx : Eq (α := ℝ) 1 (0 x)), (↑(↑f : α →ₘ[μ] E) : α → E) x = 0 x
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0

Tactic:
filter_upwards [this] with x hx using by simp at hx
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
inr :
  ∀ [Nontrivial ↥(Lp E 0 μ)] (f : ↥(Lp E 0 μ)) (hf : f ≠ 0) (hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0)
    (h'p : LT.lt (α := ℝ≥0∞) 0 ∞), Nontrivial.{u_1} ↥(Lp ℝ 0 μ)
inr₁ : ∀ (hp : p ≠ 0), Nontrivial.{u_1} ↥(Lp ℝ p μ)
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ 1) 0 μ

Tactic:
simpa using aestronglyMeasurable_const

Premises used: MeasureTheory.aestronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ 1) 0 μ

Tactic:
have : MemLp (fun (_ : α) ↦ (1 : ℝ)) 0 μ := by simpa using aestronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : LT.lt (α := ℝ≥0∞) 0 ∞
this : MemLp (ε := ℝ) (fun (x : α) ↦ 1) 0 μ
inr : MemLp.toLp (fun (x : α) ↦ 1) this ≠ 0
⊢ Nontrivial.{u_1} ↥(Lp ℝ 0 μ)

Tactic:
apply nontrivial_of_ne (this.toLp _) 0

Premises used: nontrivial_of_ne, MeasureTheory.MemLp.toLp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : LT.lt (α := ℝ≥0∞) 0 ∞
this : MemLp (ε := ℝ) (fun (x : α) ↦ 1) 0 μ
inr : ∀ (hfne : MemLp.toLp (fun (x : α) ↦ 1) this = 0), (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
⊢ MemLp.toLp (fun (x : α) ↦ 1) this ≠ 0

Tactic:
contrapose! hfne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
h'p : LT.lt (α := ℝ≥0∞) 0 ∞
this : MemLp (ε := ℝ) (fun (x : α) ↦ 1) 0 μ
hfne : MemLp.toLp (fun (x : α) ↦ 1) this = 0
⊢ (↑(↑(MemLp.toLp (fun (x : α) ↦ 1) this) : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] ℝ) : α → ℝ)

Tactic:
have := Lp.ext_iff.1 hfne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
h'p : LT.lt (α := ℝ≥0∞) 0 ∞
this_1 : MemLp (ε := ℝ) (fun (x : α) ↦ 1) 0 μ
hfne : MemLp.toLp (fun (x : α) ↦ 1) this_1 = 0
this : (↑(↑(MemLp.toLp (fun (x : α) ↦ 1) this_1) : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] ℝ) : α → ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ 1) 0

Tactic:
grw [Lp.coeFn_zero, MemLp.coeFn_toLp] at this

Premises used: MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.Lp.coeFn_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
h'p : LT.lt (α := ℝ≥0∞) 0 ∞
this_1 : MemLp (ε := ℝ) (fun (x : α) ↦ 1) 0 μ
hfne : MemLp.toLp (fun (x : α) ↦ 1) this_1 = 0
this : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ 1) 0
x : α
hx : Eq (α := ℝ) 1 (0 x)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) x = 0 x

Tactic:
simp at hx
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst_1 : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
h'p : LT.lt (α := ℝ≥0∞) 0 ∞
this_1 : MemLp (ε := ℝ) (fun (x : α) ↦ 1) 0 μ
hfne : MemLp.toLp (fun (x : α) ↦ 1) this_1 = 0
this : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ 1) 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Eq (α := ℝ) ((fun (x : α) ↦ (1 : ℝ)) x) (0 x)) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (↑(↑f : α →ₘ[μ] E) : α → E) x = 0 x) x} x}
      a
h₁ h₂ : ∀ (x : α) (hx : Eq (α := ℝ) 1 (0 x)), (↑(↑f : α →ₘ[μ] E) : α → E) x = 0 x
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0

Tactic:
filter_upwards [this] with x hx using by simp at hx
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
hp : p ≠ 0
⊢ AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ

Tactic:
have h'f : AEFinStronglyMeasurable f μ :=
      MemLp.aefinStronglyMeasurable (Lp.memLp f) hp h'p.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
h'f.exists_measurableSet_measure_pos_lt_top hfne

Premises used: MeasureTheory.AEFinStronglyMeasurable.exists_measurableSet_measure_pos_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ
inr :
  ∀ (s : Set α) (s_meas : MeasurableSet s) (s_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (s_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), Nontrivial.{u_1} ↥(Lp ℝ p μ)
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)

Tactic:
obtain ⟨s, s_meas, s_pos, s_top⟩ : ∃ s, MeasurableSet s ∧ 0 < μ s ∧ μ s < ∞ :=
      h'f.exists_measurableSet_measure_pos_lt_top hfne

Premises used: MeasureTheory.AEFinStronglyMeasurable.exists_measurableSet_measure_pos_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ
s : Set α
s_meas : MeasurableSet s
s_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
s_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inr : Ne (α := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) 0
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)

Tactic:
apply nontrivial_of_ne (indicatorConstLp p s_meas s_top.ne 1) 0

Premises used: MeasureTheory.indicatorConstLp, nontrivial_of_ne, OfNat.ofNat, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ
s : Set α
s_meas : MeasurableSet s
s_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
s_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hzero : Eq (α := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) 0
rw rw₁ : norm.{u_1} (E := ↥(Lp ℝ p μ)) 0 = norm.{u_1} (E := ↥(Lp ℝ p μ)) 0
⊢ norm (E := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) = norm.{u_1} (E := ↥(Lp ℝ p μ)) 0

Tactic:
rw [hzero]