awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
δ : ℝ≥0∞
δpos : δ ≠ 0
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
⊢ ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g
have inr : ∀ (g : α → E) (hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η) (Pg : P g),
  ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g
Tactic: rcases hf η ηpos.ne' int_ff'.1 with ⟨g, hg, Pg⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
δ : ℝ≥0∞
δpos : δ ≠ 0
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η
Pg : P g
⊢ ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g
have inr : ∀ (g' : α → E) (hg' : eLpNorm ((⇑f' : (a : α) → E) - g') p μ ≤ η) (Pg' : P g'),
  ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g
Tactic: rcases hf' η ηpos.ne' int_ff'.2 with ⟨g', hg', Pg'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
δ : ℝ≥0∞
δpos : δ ≠ 0
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η
Pg : P g
g' : α → E
hg' : eLpNorm ((⇑f' : (a : α) → E) - g') p μ ≤ η
Pg' : P g'
⊢ ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g
have inr : eLpNorm ((⇑(f + f') : (a : α) → E) - (g + g')) p μ ≤ δ
Tactic: refine ⟨g + g', ?_, h1P g g' Pg Pg'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
δ : ℝ≥0∞
δpos : δ ≠ 0
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η
Pg : P g
g' : α → E
hg' : eLpNorm ((⇑f' : (a : α) → E) - g') p μ ≤ η
Pg' : P g'
⊢ eLpNorm ((⇑(f + f') : (a : α) → E) - (g + g')) p μ ≤ δ
have h : (⇑(f + f') : (a : α) → E) - (g + g') = (⇑f : (a : α) → E) - g + ((⇑f' : (a : α) → E) - g')
Tactic: convert!
      (hη _ _ (f.aestronglyMeasurable.sub (h2P g Pg)) (f'.aestronglyMeasurable.sub (h2P g' Pg')) hg
          hg').le using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
δ : ℝ≥0∞
δpos : δ ≠ 0
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η
Pg : P g
g' : α → E
hg' : eLpNorm ((⇑f' : (a : α) → E) - g') p μ ≤ η
Pg' : P g'
⊢ (⇑(f + f') : (a : α) → E) - (g + g') = (⇑f : (a : α) → E) - g + ((⇑f' : (a : α) → E) - g')
have h : HAdd.hAdd (α := (a : α) → E) (⇑f : (a : α) → E) (⇑f' : (a : α) → E) - (g + g') =
  (⇑f : (a : α) → E) - g + ((⇑f' : (a : α) → E) - g')
Tactic: rw [SimpleFunc.coe_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
f : ↥(Lp.simpleFunc E 1 μ)
⊢ Integrable.{u_4, u_1} (ε := E) (⇑(Lp.simpleFunc.toSimpleFunc f) : (a : α) → E) μ
have rw : MemLp.{u_1, u_4} (ε := E) (⇑(Lp.simpleFunc.toSimpleFunc f) : (a : α) → E) 1 μ
Tactic: rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
P : (α → E) → Prop
h_ind :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → P (s.indicator fun (x : α) ↦ c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Integrable f μ → Integrable g μ → P f → P g → P (f + g)
h_closed : IsClosed (X := ↥(Lp E 1 μ)) {f : ↥(Lp E 1 μ) | P (↑(↑f : α →ₘ[μ] E) : α → E)}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → Integrable f μ → P f → P g
⊢ ∀ ⦃f : α → E⦄, Integrable f μ → P f
have simp : ∀ (h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f 1 μ → MemLp g 1 μ → P f → P g → P (f + g))
  (h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f 1 μ → P f → P g) ⦃f : α → E⦄, MemLp f 1 μ → P f
Tactic: simp only [← memLp_one_iff_integrable] at *
Cleared hypotheses: h_add, h_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : Measurable (β := ℝ) fun (x : α) ↦ rexp (f x)
⊢ f = fun (x : α) ↦ log (rexp (f x))
have h : ∀ (x : α), f x = log (rexp (f x))
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : Measurable (β := ℝ) fun (x : α) ↦ rexp (f x)
x_1 : α
⊢ f x_1 = log (rexp (f x_1))
have h : f x_1 = f x_1
Tactic: rw [log_exp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (hypothesis)
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : Measurable (β := ℝ) fun (x : α) ↦ rexp (f x)
⊢ Measurable f
have this : f = fun (x : α) ↦ log (rexp (f x))
Tactic: have : f = fun x ↦ log (exp (f x)) := by ext; rw [log_exp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : Measurable (β := ℝ) fun (x : α) ↦ rexp (f x)
this : f = fun (x : α) ↦ log (rexp (f x))
⊢ Measurable f
have rw : Measurable (β := ℝ) fun (x : α) ↦ log (rexp (f x))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ f = fun (x : α) ↦ log (rexp (f x))
have h : ∀ (x : α), f x = log (rexp (f x))
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
x_1 : α
⊢ f x_1 = log (rexp (f x_1))
have h : f x_1 = f x_1
Tactic: rw [log_exp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (hypothesis)
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ AEMeasurable f μ
have this : f = fun (x : α) ↦ log (rexp (f x))
Tactic: have : f = fun x ↦ log (exp (f x)) := by ext; rw [log_exp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
this : f = fun (x : α) ↦ log (rexp (f x))
⊢ AEMeasurable f μ
have rw : AEMeasurable (β := ℝ) (fun (x : α) ↦ log (rexp (f x))) μ
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (goal)
Goal:
⊢ MeasurablePow ℝ≥0∞ ℝ
have refine_1 : Measurable (β := ℝ≥0∞) fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ≥0∞), p.2).1 ^ ((↑p.1 : ℝ≥0∞), p.2).2
Tactic: refine ⟨ENNReal.measurable_of_measurable_nnreal_prod ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (goal)
Goal:
refine_1 : Measurable (β := ℝ≥0∞) fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ≥0∞), p.2).1 ^ ((↑p.1 : ℝ≥0∞), p.2).2
⊢ MeasurablePow ℝ≥0∞ ℝ
have refine_2 : Measurable (β := ℝ≥0∞) fun (x : ℝ) ↦ HPow.hPow (α := ℝ≥0∞) (∞, x).1 (∞, x).2
Tactic: refine ⟨ENNReal.measurable_of_measurable_nnreal_prod ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (goal)
Goal:
⊢ Measurable (β := ℝ≥0∞) fun (p : ℝ≥0 × ℝ) ↦ if p.1 = 0 ∧ p.2 < 0 then ∞ else (↑(p.1 ^ p.2) : ℝ≥0∞)
have refine_1 : MeasurableSet (α := ℝ≥0 × ℝ) {a : ℝ≥0 × ℝ | a.1 = 0 ∧ a.2 < 0}
Tactic: refine Measurable.ite ?_ measurable_const (measurable_fst.pow measurable_snd).coe_nnreal_ennreal
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (goal)
Goal:
⊢ Measurable (β := ℝ≥0∞) fun (x : ℝ) ↦ if 0 < x then ∞ else if x = 0 then 1 else 0
have refine_2 : Measurable (β := ℝ≥0∞) fun (x : ℝ) ↦ if x = 0 then 1 else 0
Tactic: refine Measurable.ite measurableSet_Ioi measurable_const ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
f : α → 𝕜
hre : Measurable (β := ℝ) fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)
him : Measurable (β := ℝ) fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)
⊢ Measurable f
have h : ∀ (x : α),
  f x =
    (RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) x +
      HMul.hMul (α := 𝕜) ((RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) x) RCLike.I
Tactic: convert!
    Measurable.add (M := 𝕜) (RCLike.measurable_ofReal.comp hre)
      ((RCLike.measurable_ofReal.comp him).mul_const RCLike.I)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ
him : AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ
⊢ AEMeasurable f μ
have h : ∀ (x : α),
  f x =
    (RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) x +
      HMul.hMul (α := 𝕜) ((RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) x) RCLike.I
Tactic: convert!
    AEMeasurable.add (M := 𝕜) (RCLike.measurable_ofReal.comp_aemeasurable hre)
      ((RCLike.measurable_ofReal.comp_aemeasurable him).mul_const RCLike.I)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
⊢ Integrable (ε := ℝ) (fun (x : ℝ) ↦ 1) μ
have funProp : enorm (E := ℝ) 1 ≠ ⊤
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
⊢ Integrable sinc μ
have refine : ∀ (x : ℝ), ‖sinc x‖ ≤ (fun (x : ℝ) ↦ (1 : ℝ)) x
Tactic: refine Integrable.mono' (g := fun _ ↦ 1) (by fun_prop) (by fun_prop) <| ae_of_all _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ sinc (f x)) μ
have rw : ∀ (hf : AEMeasurable f μ), AEMeasurable (β := ℝ) (fun (x : α) ↦ sinc (f x)) μ
Tactic: rw [aestronglyMeasurable_iff_aemeasurable] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
⊢ AEStronglyMeasurable (m₀ := m₀) f 0
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
h : Nontrivial α
⊢ AEStronglyMeasurable (m₀ := m₀) f 0
have inhabit : ∀ (inhabited_h : Inhabited α), AEStronglyMeasurable (m₀ := m₀) f 0
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AEStronglyMeasurable id μ
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
⊢ AEStronglyMeasurable id μ
have obtain : ∀ (a : α), AEStronglyMeasurable id μ
Tactic: obtain ⟨a, -⟩ := exists_pair_ne α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
a : α
⊢ AEStronglyMeasurable id μ
have refine : StronglyMeasurable ((closure[inst] s).piecewise (β := fun (a : α) ↦ α) id fun (x : α) ↦ a)
Tactic: refine ⟨(closure s).piecewise id (fun _ ↦ a), ?_,
    Filter.mem_of_superset h2 (fun x hx ↦ by simp [subset_closure hx])⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
a : α
⊢ StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
have this : SecondCountableTopology.{u_1} (↑(closure[inst] s) : Type u_1)
Tactic: have := h1.closure.secondCountableTopology
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
a : α
⊢ StronglyMeasurable ((closure[inst] s).piecewise (β := fun (a : α) ↦ α) id fun (x : α) ↦ a)
have h : StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
  (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
Tactic: have h : StronglyMeasurable ((↑) : closure s → α) := by
    have := h1.closure.secondCountableTopology
    exact continuous_subtype_val.stronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Nontrivial α
a : α
h :
  StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
⊢ ((closure[inst] s).piecewise (β := fun (i : α) ↦ α) id fun (x : α) ↦ a) =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a
have h₁ : ∀ (x : α),
  (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Nontrivial α
a : α
h :
  StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
x : α
⊢ (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x
have pos : ∀ (hx : x ∈ closure[inst] s),
  (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x
Tactic: by_cases hx : x ∈ closure s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Nontrivial α
a : α
h :
  StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
x : α
pos :
  ∀ (hx : x ∈ closure[inst] s),
    (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
      Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x
⊢ (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x
have neg : ∀ (hx : x ∉ closure[inst] s),
  (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x
Tactic: by_cases hx : x ∈ closure s