awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
hF : CompleteSpace F
hfi' : Integrable f μ'
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_2} (↑(range f ∪ {0}) : Type u_2)
i : ℕ
⊢ Eq.{u_3 + 1} (α := F)
    (∑ x_1 ∈ (SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range,
      (T' (preimage (β := E) (⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) : (a : β) → E) {x_1}) : (a : E) → F) x_1)
    (∑ x_1 ∈ ((SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).comp φ hφ).range,
      (T (preimage (β := E) (⇑((SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).comp φ hφ) : (a : α) → E) {x_1}) :
          (a : E) → F)
        x_1)
have h₁ : Eq.{u_3 + 1} (α := F)
  (∑ x_1 ∈ (SimpleFunc.approxOn f sorry (insert 0 (range f)) 0 sorry i).range,
    (T (preimage (β := E) ((⇑(SimpleFunc.approxOn f sorry (insert 0 (range f)) 0 sorry i) : (a : β) → E) ∘ φ) {x_1}) :
        (a : E) → F)
      x_1)
  (∑ x_1 ∈ ((SimpleFunc.approxOn f sorry (insert 0 (range f)) 0 sorry i).comp φ hφ).range,
    (T (preimage (β := E) ((⇑(SimpleFunc.approxOn f sorry (insert 0 (range f)) 0 sorry i) : (a : β) → E) ∘ φ) {x_1}) :
        (a : E) → F)
      x_1)
Tactic: simp only [union_singleton, SimpleFunc.measurableSet_preimage, h, ← preimage_comp,
    SimpleFunc.coe_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
hF : CompleteSpace F
hfi' : Integrable f μ'
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_2} (↑(range f ∪ {0}) : Type u_2)
i : ℕ
⊢ Eq.{u_3 + 1} (α := F)
    (∑ x_1 ∈ (SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i).range,
      (T (preimage (β := E) ((⇑(SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i) : (a : β) → E) ∘ φ) {x_1}) :
          (a : E) → F)
        x_1)
    (∑ x_1 ∈ ((SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i).comp φ hφ).range,
      (T (preimage (β := E) ((⇑(SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i) : (a : β) → E) ∘ φ) {x_1}) :
          (a : E) → F)
        x_1)
have h₁ : ∀ y ∈ (SimpleFunc.approxOn f sorry (insert 0 (range f)) 0 sorry i).range,
  ∀ (hy : y ∉ ((SimpleFunc.approxOn f sorry (insert 0 (range f)) 0 sorry i).comp φ hφ).range),
    Eq.{u_3 + 1} (α := F)
      ((T (preimage (β := E) ((⇑(SimpleFunc.approxOn f sorry (insert 0 (range f)) 0 sorry i) : (a : β) → E) ∘ φ) {y}) :
            (a : E) → F)
          y :
        F)
      (0 : F)
Tactic: refine (Finset.sum_subset (SimpleFunc.range_comp_subset_range _ hφ) fun y _ hy => ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
hF : CompleteSpace F
hfi' : Integrable f μ'
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_2} (↑(range f ∪ {0}) : Type u_2)
i : ℕ
y : E
h_1 : y ∈ (SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i).range
hy : y ∉ ((SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i).comp φ hφ).range
⊢ Eq.{u_3 + 1} (α := F)
    ((T (preimage (β := E) ((⇑(SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i) : (a : β) → E) ∘ φ) {y}) :
          (a : E) → F)
        y :
      F)
    (0 : F)
have hy₁ : preimage (β := E) ((⇑(SimpleFunc.approxOn f sorry (insert 0 (range f)) 0 sorry i) : (a : β) → E) ∘ φ) {y} = ∅
Tactic: rw [SimpleFunc.mem_range, ← Set.preimage_singleton_eq_empty, SimpleFunc.coe_comp] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : AEStronglyMeasurable (m₀ := x) f (Measure.map φ μ)
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
g : β → E := AEStronglyMeasurable.mk f hfm
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
have A : setToFun μ' T' hT' f = setToFun μ' T' hT' g
Tactic: have A : setToFun μ' T' hT' f = setToFun μ' T' hT' g :=
    setToFun_congr_ae _ (ae_mono hμ' hfm.ae_eq_mk)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : AEStronglyMeasurable (m₀ := x) f (Measure.map φ μ)
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
g : β → E := AEStronglyMeasurable.mk f hfm
A : setToFun μ' T' hT' f = setToFun μ' T' hT' g
⊢ setToFun μ T hT (f ∘ φ) = setToFun μ T hT (g ∘ φ)
have h₁ : f ∘ φ =ᶠ[ae μ] g ∘ φ
Tactic: apply setToFun_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : AEStronglyMeasurable (m₀ := x) f (Measure.map φ μ)
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
g : β → E := AEStronglyMeasurable.mk f hfm
A : setToFun μ' T' hT' f = setToFun μ' T' hT' g
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
have B : setToFun μ T hT (f ∘ φ) = setToFun μ T hT (g ∘ φ)
Tactic: have B : setToFun μ T hT (f ∘ φ) = setToFun μ T hT (g ∘ φ) := by
    apply setToFun_congr_ae
    exact ae_of_ae_map hφ.aemeasurable hfm.ae_eq_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : AEStronglyMeasurable (m₀ := x) f (Measure.map φ μ)
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
g : β → E := AEStronglyMeasurable.mk f hfm
A : setToFun μ' T' hT' f = setToFun μ' T' hT' g
B : setToFun μ T hT (f ∘ φ) = setToFun μ T hT (g ∘ φ)
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
have rw : setToFun μ' T' hT' g = setToFun μ T hT (g ∘ φ)
Tactic: rw [A, B]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
⊢ Continuous (Y := ↥(Lp G 1 μ')) fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯
have pos : ∀ (hc'0 : c' = 0), Continuous (Y := ↥(Lp G 1 μ')) fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) sorry
Tactic: by_cases hc'0 : c' = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
pos :
  ∀ (hc'0 : c' = 0),
    Continuous (Y := ↥(Lp G 1 μ')) fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯
⊢ Continuous (Y := ↥(Lp G 1 μ')) fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯
have neg : ∀ (hc'0 : ¬c' = 0), Continuous (Y := ↥(Lp G 1 μ')) fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) sorry
Tactic: by_cases hc'0 : c' = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ μ' = 0
have rw : μ' ≤ 0
Tactic: rw [← Measure.nonpos_iff_eq_zero']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ μ' ≤ 0
have refine : c' • μ ≤ 0
Tactic: refine hμ'_le.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ Continuous (Y := ↥(Lp G 1 μ')) fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯
have hμ'0 : μ' = 0
Tactic: have hμ'0 : μ' = 0 := by rw [← Measure.nonpos_iff_eq_zero']; refine hμ'_le.trans ?_; simp [hc'0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
⊢ Eq (α := (f : ↥(Lp G 1 μ)) → ↥(Lp G 1 μ')) (fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) 0
have h : ∀ (f : ↥(Lp G 1 μ)), Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) sorry = 0 f
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : ↥(Lp G 1 μ)
⊢ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯ = 0 f
have h : (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ'] G) : α → G) =ᶠ[ae μ'] (↑(↑(0 f) : α →ₘ[μ'] G) : α → G)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : ↥(Lp G 1 μ)
⊢ (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) =ᶠ[ae μ'] (↑(↑(0 f) : α →ₘ[μ'] G) : α → G)
have h : (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ'] G) : α → G) =ᶠ[ae (F := Measure α) 0]
  (↑(↑(0 f) : α →ₘ[μ'] G) : α → G)
Tactic: simp_rw [hμ'0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
⊢ Continuous (Y := ↥(Lp G 1 μ')) fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯
have h_im_zero : Eq (α := (f : ↥(Lp G 1 μ)) → ↥(Lp G 1 μ')) (fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) sorry) 0
Tactic: have h_im_zero :
      (fun f : α →₁[μ] G =>
          (Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f)).toL1 f) =
        0 := by
      ext1 f; ext1; simp_rw [hμ'0]; simp only [ae_zero, EventuallyEq, eventually_bot]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
h_im_zero :
  Eq (α := (f : ↥(Lp G 1 μ)) → ↥(Lp G 1 μ')) (fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) 0
⊢ Continuous (Y := ↥(Lp G 1 μ')) fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯
have pos : Continuous (X := ↥(Lp G 1 μ)) (Y := ↥(Lp G 1 μ')) 0
Tactic: rw [h_im_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
⊢ Continuous (Y := ↥(Lp G 1 μ')) fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯
have neg : ∀ (b : ↥(Lp G 1 μ)),
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ (a : ↥(Lp G 1 μ)),
        dist a b < δ →
          dist (Integrable.toL1 (↑(↑a : α →ₘ[μ] G) : α → G) sorry) (Integrable.toL1 (↑(↑b : α →ₘ[μ] G) : α → G) sorry) < ε
Tactic: rw [Metric.continuous_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
⊢ ∃ δ > 0,
    ∀ (a : ↥(Lp G 1 μ)),
      dist a f < δ →
        dist (Integrable.toL1 (↑(↑a : α →ₘ[μ] G) : α → G) ⋯) (Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) < ε
have h : ε / 2 / c'.toReal > 0 ∧
  ∀ (a : ↥(Lp G 1 μ)),
    dist a f < ε / 2 / c'.toReal →
      dist (Integrable.toL1 (↑(↑a : α →ₘ[μ] G) : α → G) sorry) (Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) sorry) < ε
Tactic: use ε / 2 / c'.toReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
⊢ ε / 2 / c'.toReal > 0 ∧
    ∀ (a : ↥(Lp G 1 μ)),
      dist a f < ε / 2 / c'.toReal →
        dist (Integrable.toL1 (↑(↑a : α →ₘ[μ] G) : α → G) ⋯) (Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) < ε
have h : ∀ (a : ↥(Lp G 1 μ)),
  dist a f < ε / 2 / c'.toReal →
    dist (Integrable.toL1 (↑(↑a : α →ₘ[μ] G) : α → G) sorry) (Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) sorry) < ε
Tactic: refine ⟨div_pos (half_pos hε_pos) (toReal_pos hc'0 hc'), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : dist g f < ε / 2 / c'.toReal
⊢ dist (Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) (Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) < ε
have h : ∀ (hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal),
  (eLpNorm
        ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ'] G) : α → G) -
          (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ'] G) : α → G))
        1 μ').toReal <
    ε
Tactic: rw [Lp.dist_def] at hfg ⊢
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
⊢ (eLpNorm
        ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
          (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
        1 μ').toReal <
    ε
have this : eLpNorm
    ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ'] G) : α → G) -
      (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ'] G) : α → G))
    1 μ' =
  eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
Tactic: have :
    eLpNorm (⇑(Integrable.toL1 g (h_int g)) - ⇑(Integrable.toL1 f (h_int f))) 1 μ' =
      eLpNorm (⇑g - ⇑f) 1 μ' :=
    eLpNorm_congr_ae ((Integrable.coeFn_toL1 _).sub (Integrable.coeFn_toL1 _))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
⊢ (eLpNorm
        ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
          (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
        1 μ').toReal <
    ε
have h : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ').toReal < ε
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
⊢ eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
have rw : eLpNorm (↑(↑(g - f) : α →ₘ[μ] G) : α → G) 1 μ ≠ ∞
Tactic: rw [← eLpNorm_congr_ae (Lp.coeFn_sub _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
⊢ (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ').toReal < ε
have h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
Tactic: have h_eLpNorm_ne_top : eLpNorm (⇑g - ⇑f) 1 μ ≠ ∞ := by
    rw [← eLpNorm_congr_ae (Lp.coeFn_sub _ _)]; exact Lp.eLpNorm_ne_top _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
⊢ (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ').toReal ≤
    (c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal
have refine : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ' ≤
  c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ
Tactic: refine toReal_mono (ENNReal.mul_ne_top hc' h_eLpNorm_ne_top) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
⊢ eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ' ≤
    c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ
have refine : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 (c' • μ) =
  c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ
Tactic: refine (eLpNorm_mono_measure (⇑g - ⇑f) hμ'_le).trans_eq ?_