awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
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∞)
⊢ f =ᶠ[ae μ] 0
have B : ∀ᵐ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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)
⊢ f =ᶠ[ae μ] 0
have h : ∀ (x : α) (hx : ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) ((fn n : (a : α) → E) x : E) (0 : E)), f x = 0 x
Tactic: filter_upwards [B] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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)
⊢ f x = 0 x
have h : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (0 x))
Tactic: apply tendsto_nhds_unique (hfn_lim x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : AEFinStronglyMeasurable f μ
h'f : ¬f =ᶠ[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∞)
have apply : ¬AEFinStronglyMeasurable.mk f hf =ᶠ[ae μ] 0
Tactic: apply hf.finStronglyMeasurable_mk.exists_measurableSet_measure_pos_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : AEFinStronglyMeasurable f μ
h'f : ¬f =ᶠ[ae μ] 0
⊢ ¬AEFinStronglyMeasurable.mk f hf =ᶠ[ae μ] 0
have contrapose! : ∀ (h'f : AEFinStronglyMeasurable.mk f hf =ᶠ[ae μ] 0), f =ᶠ[ae μ] 0
Tactic: contrapose! h'f
Cleared hypotheses: h'f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)
have obtain : ∀ (f : ↥(Lp E p μ)) (hf : f ≠ 0), Nontrivial.{u_1} ↥(Lp ℝ p μ)
Tactic: obtain ⟨f, hf⟩ : ∃ f : Lp E p μ, f ≠ 0 := exists_ne 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
have contrapose! : ∀ (hf : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0), f = 0
Tactic: contrapose! hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
⊢ f = 0
have h : (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] E) : α → E)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] E) : α → E)
have h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 (↑(↑0 : α →ₘ[μ] E) : α → E)
Tactic: grw [hf, Lp.coeFn_zero E p μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] E) : α → E)
have h₁ : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0
Tactic: grw [hf, Lp.coeFn_zero E p μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
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
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)
have hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
Tactic: have hfne : ¬ (f =ᵐ[μ] 0) := by
    contrapose! hf
    ext
    grw [hf, Lp.coeFn_zero E p μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)
have inl : ∀ [Nontrivial ↥(Lp E ∞ μ)] (f : ↥(Lp E ∞ μ)) (hf : f ≠ 0) (hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0),
  Nontrivial.{u_1} ↥(Lp ℝ ∞ μ)
Tactic: rcases eq_top_or_lt_top p with rfl | h'p
Cleared hypotheses: p, inst_1, f, hf, hfne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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 ℝ ∞ μ)
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)
have inr : ∀ (h'p : p < ∞), Nontrivial.{u_1} ↥(Lp ℝ p μ)
Tactic: rcases eq_top_or_lt_top p with rfl | h'p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
⊢ Nontrivial.{u_1} ↥(Lp ℝ ∞ μ)
have inl : Ne.{u_1 + 1} (α := ↥(Lp ℝ ∞ μ)) (MemLp.toLp (fun (x : α) ↦ 1) sorry) 0
Tactic: apply nontrivial_of_ne ((memLp_top_const (1 : ℝ)).toLp _) 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
⊢ Ne.{u_1 + 1} (α := ↥(Lp ℝ ∞ μ)) (MemLp.toLp (fun (x : α) ↦ 1) ⋯) 0
have inl : ∀ (hfne : Eq.{u_1 + 1} (α := ↥(Lp ℝ ∞ μ)) (MemLp.toLp (fun (x : α) ↦ 1) sorry) 0), (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
Tactic: contrapose! hfne
Cleared hypotheses: hfne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
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
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have this : (ae μ).EventuallyEq (β := ℝ) (↑(↑(MemLp.toLp (fun (x : α) ↦ 1) sorry) : α →ₘ[μ] ℝ) : α → ℝ) (↑(↑0 : α →ₘ[μ] ℝ) : α → ℝ)
Tactic: have := Lp.ext_iff.1 hfne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
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 : α →ₘ[μ] ℝ) : α → ℝ)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have this₁ : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ 1) 0
Tactic: grw [Lp.coeFn_zero, MemLp.coeFn_toLp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have 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
Tactic: filter_upwards [this] with x hx using by simp at hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have h₁ : ∀ (a : α), Eq (α := ℝ) 1 (0 a) → (↑(↑f : α →ₘ[μ] E) : α → E) a = 0 a
Tactic: filter_upwards [this] with x hx using by simp at hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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 < ∞
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)
have 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 μ)
Tactic: rcases eq_or_ne p 0 with rfl | hp
Cleared hypotheses: p, inst_1, f, hf, hfne, h'p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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 μ)
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)
have inr₁ : ∀ (hp : p ≠ 0), Nontrivial.{u_1} ↥(Lp ℝ p μ)
Tactic: rcases eq_or_ne p 0 with rfl | hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
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 ∞
⊢ Nontrivial.{u_1} ↥(Lp ℝ 0 μ)
have this : MemLp (ε := ℝ) (fun (x : α) ↦ 1) 0 μ
Tactic: have : MemLp (fun (_ : α) ↦ (1 : ℝ)) 0 μ := by simpa using aestronglyMeasurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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 μ
⊢ Nontrivial.{u_1} ↥(Lp ℝ 0 μ)
have inr : MemLp.toLp (fun (x : α) ↦ 1) this ≠ 0
Tactic: apply nontrivial_of_ne (this.toLp _) 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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 μ
⊢ MemLp.toLp (fun (x : α) ↦ 1) this ≠ 0
have inr : ∀ (hfne : MemLp.toLp (fun (x : α) ↦ 1) this = 0), (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
Tactic: contrapose! hfne
Cleared hypotheses: hfne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
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
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have this₁ : (↑(↑(MemLp.toLp (fun (x : α) ↦ 1) this) : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae μ] (↑(↑0 : α →ₘ[μ] ℝ) : α → ℝ)
Tactic: have := Lp.ext_iff.1 hfne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
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 : α →ₘ[μ] ℝ) : α → ℝ)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have this₁ : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ 1) 0
Tactic: grw [Lp.coeFn_zero, MemLp.coeFn_toLp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have 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
Tactic: filter_upwards [this] with x hx using by simp at hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have h₁ : ∀ (a : α), Eq (α := ℝ) 1 (0 a) → (↑(↑f : α →ₘ[μ] E) : α → E) a = 0 a
Tactic: filter_upwards [this] with x hx using by simp at hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
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
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)
have h'f : AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ
Tactic: have h'f : AEFinStronglyMeasurable f μ :=
      MemLp.aefinStronglyMeasurable (Lp.memLp f) hp h'p.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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) μ
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)
have 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 μ)
Tactic: obtain ⟨s, s_meas, s_pos, s_top⟩ : ∃ s, MeasurableSet s ∧ 0 < μ s ∧ μ s < ∞ :=
      h'f.exists_measurableSet_measure_pos_lt_top hfne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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∞)
⊢ Nontrivial.{u_1} ↥(Lp ℝ p μ)
have inr : Ne (α := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas sorry 1) 0
Tactic: apply nontrivial_of_ne (indicatorConstLp p s_meas s_top.ne 1) 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
⊢ norm (E := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) = norm.{u_1} (E := ↥(Lp ℝ p μ)) 0
have rw : norm.{u_1} (E := ↥(Lp ℝ p μ)) 0 = norm.{u_1} (E := ↥(Lp ℝ p μ)) 0
Tactic: rw [hzero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
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
⊢ False
have this : norm (E := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas sorry 1) = norm.{u_1} (E := ↥(Lp ℝ p μ)) 0
Tactic: have : ‖indicatorConstLp p s_meas s_top.ne (1 : ℝ)‖ = ‖(0 : Lp ℝ p μ)‖ := by rw [hzero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
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
this : norm (E := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) = norm.{u_1} (E := ↥(Lp ℝ p μ)) 0
⊢ False
have this₁ : μ.real s ^ p.toReal⁻¹ = 0
Tactic: simp only [norm_indicatorConstLp hp h'p.ne, norm_one, one_div, one_mul, Lp.norm_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
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
this : μ.real s ^ p.toReal⁻¹ = 0
⊢ False
have this₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Real.rpow_eq_zero (by positivity) (by simp [ENNReal.toReal_eq_zero_iff, hp, h'p.ne]),
      measureReal_eq_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False
have inr : ¬False → False
Tactic: order