awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)

Tactic:
(Finset.sum_subset (SimpleFunc.range_comp_subset_range _ hφ) fun y _ hy => ?_).symm

Premises used: MeasureTheory.SimpleFunc.range_comp_subset_range, Finset.sum_subset, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 : ℕ
h₁ :
  ∀ 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)
⊢ 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)

Tactic:
refine (Finset.sum_subset (SimpleFunc.range_comp_subset_range _ hφ) fun y _ hy => ?_).symm

Premises used: MeasureTheory.SimpleFunc.range_comp_subset_range, Finset.sum_subset, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
⊢ preimage (β := E) ((⇑(SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i) : (a : β) → E) ∘ φ) {y} = ∅

Tactic:
rw [SimpleFunc.mem_range, ← Set.preimage_singleton_eq_empty, SimpleFunc.coe_comp] at hy

Premises used: MeasureTheory.SimpleFunc.mem_range, Set.preimage_singleton_eq_empty, MeasureTheory.SimpleFunc.coe_comp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 : preimage (β := E) ((⇑(SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i) : (a : β) → E) ∘ φ) {y} = ∅
⊢ 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)

Tactic:
simp [hy, hT.1.map_empty_eq_zero]

Premises used: MeasureTheory.FinMeasAdditive.map_empty_eq_zero, And.left
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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' g

Tactic:
have A : setToFun μ' T' hT' f = setToFun μ' T' hT' g :=
    setToFun_congr_ae _ (ae_mono hμ' hfm.ae_eq_mk)
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
h₁ : f ∘ φ =ᶠ[ae μ] g ∘ φ
⊢ setToFun μ T hT (f ∘ φ) = setToFun μ T hT (g ∘ φ)

Tactic:
apply setToFun_congr_ae

Premises used: MeasureTheory.setToFun_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
⊢ f ∘ φ =ᶠ[ae μ] g ∘ φ

Tactic:
ae_of_ae_map hφ.aemeasurable hfm.ae_eq_mk

Premises used: Measurable.aemeasurable, Filter.EventuallyEq, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.ae_of_ae_map, MeasureTheory.AEStronglyMeasurable.mk, Classical.choose
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
⊢ f ∘ φ =ᶠ[ae μ] g ∘ φ

Tactic:
exact ae_of_ae_map hφ.aemeasurable hfm.ae_eq_mk

Premises used: Measurable.aemeasurable, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.ae_of_ae_map
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 ∘ φ)

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
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 ∘ φ)
rw : setToFun μ' T' hT' g = setToFun μ T hT (g ∘ φ)
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)

Tactic:
rw [A, B]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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' g = setToFun μ T hT (g ∘ φ)

Tactic:
setToFun_of_le_map_of_stronglyMeasurable _ _
    (hf.congr (ae_of_ae_map hφ.aemeasurable hfm.ae_eq_mk)) hfm.stronglyMeasurable_mk hφ hμ' h

Premises used: Measurable.aemeasurable, MeasureTheory.setToFun_of_le_map_of_stronglyMeasurable, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.ae_of_ae_map, MeasureTheory.Integrable.congr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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' g = setToFun μ T hT (g ∘ φ)

Tactic:
exact setToFun_of_le_map_of_stronglyMeasurable _ _
    (hf.congr (ae_of_ae_map hφ.aemeasurable hfm.ae_eq_mk)) hfm.stronglyMeasurable_mk hφ hμ' h

Premises used: Measurable.aemeasurable, MeasureTheory.setToFun_of_le_map_of_stronglyMeasurable, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.ae_of_ae_map, MeasureTheory.Integrable.congr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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) ⋯
neg :
  ∀ (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) ⋯

Tactic:
by_cases hc'0 : c' = 0
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
rw : μ' ≤ 0
⊢ μ' = 0

Tactic:
rw [← Measure.nonpos_iff_eq_zero']

Premises used: MeasureTheory.Measure.nonpos_iff_eq_zero'
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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

Tactic:
hμ'_le.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
refine : c' • μ ≤ 0
⊢ μ' ≤ 0

Tactic:
refine hμ'_le.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
⊢ c' • μ ≤ 0

Tactic:
simp [hc'0]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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

Tactic:
have hμ'0 : μ' = 0 := by rw [← Measure.nonpos_iff_eq_zero']; refine hμ'_le.trans ?_; simp [hc'0]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 : ∀ (f : ↥(Lp G 1 μ)), Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯ = 0 f
⊢ Eq (α := (f : ↥(Lp G 1 μ)) → ↥(Lp G 1 μ')) (fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) 0

Tactic:
ext1 f
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ)
h :
  (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) =ᶠ[ae μ'] (↑(↑(0 f) : α →ₘ[μ'] G) : α → G)
⊢ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯ = 0 f

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ)
h :
  (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) =ᶠ[ae (F := Measure α) 0]
    (↑(↑(0 f) : α →ₘ[μ'] G) : α → G)
⊢ (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) =ᶠ[ae μ'] (↑(↑(0 f) : α →ₘ[μ'] G) : α → G)

Tactic:
simp_rw [hμ'0]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 (F := Measure α) 0]
    (↑(↑(0 f) : α →ₘ[μ'] G) : α → G)

Tactic:
simp only [ae_zero, EventuallyEq, eventually_bot]

Premises used: MeasureTheory.ae_zero, Filter.EventuallyEq, Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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

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]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
pos : Continuous (X := ↥(Lp G 1 μ)) (Y := ↥(Lp G 1 μ')) 0
⊢ Continuous (Y := ↥(Lp G 1 μ')) fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯

Tactic:
rw [h_im_zero]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 (X := ↥(Lp G 1 μ)) (Y := ↥(Lp G 1 μ')) 0

Tactic:
continuous_zero

Premises used: continuous_zero
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 (X := ↥(Lp G 1 μ)) (Y := ↥(Lp G 1 μ')) 0

Tactic:
exact continuous_zero

Premises used: continuous_zero
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
neg :
  ∀ (b : ↥(Lp G 1 μ)),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : ↥(Lp G 1 μ)),
          dist a b < δ →
            dist (Integrable.toL1 (↑(↑a : α →ₘ[μ] G) : α → G) ⋯) (Integrable.toL1 (↑(↑b : α →ₘ[μ] G) : α → G) ⋯) < ε
⊢ Continuous (Y := ↥(Lp G 1 μ')) fun (f : ↥(Lp G 1 μ)) ↦ Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯

Tactic:
rw [Metric.continuous_iff]

Premises used: Metric.continuous_iff
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
h :
  ε / 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) ⋯) < ε
⊢ ∃ δ > 0,
    ∀ (a : ↥(Lp G 1 μ)),
      dist a f < δ →
        dist (Integrable.toL1 (↑(↑a : α →ₘ[μ] G) : α → G) ⋯) (Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) < ε

Tactic:
use ε / 2 / c'.toReal

Premises used: ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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) ⋯) < ε

Tactic:
⟨div_pos (half_pos hε_pos) (toReal_pos hc'0 hc'), ?_⟩

Premises used: half_pos, ENNReal.toReal_pos, And.intro, div_pos
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
h :
  ∀ (a : ↥(Lp G 1 μ)),
    dist a f < ε / 2 / c'.toReal →
      dist (Integrable.toL1 (↑(↑a : α →ₘ[μ] G) : α → G) ⋯) (Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) < ε
⊢ ε / 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) ⋯) < ε

Tactic:
refine ⟨div_pos (half_pos hε_pos) (toReal_pos hc'0 hc'), ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
h :
  ∀ (hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal),
    (eLpNorm
          ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
            (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
          1 μ').toReal <
      ε
⊢ dist (Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) (Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) < ε

Tactic:
rw [Lp.dist_def] at hfg ⊢

Premises used: MeasureTheory.Lp.dist_def