awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
s : Set X
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)₀
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set Y) s univ)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
x : X
zero_x : f x 0 = 0
⊢ Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (↑(mkD (f x) g) : C(Y, E))
have h : Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (ContinuousMap.mkD (f x) (↑g : C(Y, E)))
Tactic: rw [mkD_eq_mkD_of_map_zero _ _ zero_x]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
⊢ AEStronglyMeasurable (β := ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) μ
have rw : AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
  (fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))) μ
Tactic: rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
⊢ AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))) μ
have refine : (ae μ).EventuallyEq (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
  (fun (x : X) ↦ ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E))) fun (x : X) ↦
  (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
Tactic: refine aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry f g f_cont
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
⊢ (ae μ).EventuallyEq (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
have h : ∀ (x : X) (zero_x : f x (↑0 : Y) = 0),
  Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
Tactic: filter_upwards [f_zero] with x zero_x
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
x : X
zero_x : f x (↑0 : Y) = 0
⊢ Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
have h : Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
  (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
  (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
Tactic: rw [mkD_eq_mkD_of_map_zero _ _ zero_x]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set X
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
hs : MeasurableSet s
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x (↑0 : Y) = 0
⊢ AEStronglyMeasurable (β := ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) (μ.restrict s)
have rw : AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
  (fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))) (μ.restrict s)
Tactic: rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set X
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
hs : MeasurableSet s
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x (↑0 : Y) = 0
⊢ AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))) (μ.restrict s)
have refine : (ae (μ.restrict s)).EventuallyEq (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
  (fun (x : X) ↦ ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E))) fun (x : X) ↦
  (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
Tactic: refine aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry hs f g f_cont
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set X
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
hs : MeasurableSet s
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x (↑0 : Y) = 0
⊢ (ae (μ.restrict s)).EventuallyEq (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
have h : ∀ (x : X) (zero_x : f x (↑0 : Y) = 0),
  Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
Tactic: filter_upwards [f_zero] with x zero_x
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set X
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
hs : MeasurableSet s
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x (↑0 : Y) = 0
x : X
zero_x : f x (↑0 : Y) = 0
⊢ Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
have h : Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
  (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
  (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
Tactic: rw [mkD_eq_mkD_of_map_zero _ _ zero_x]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) p μ
⊢ f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i
have h : ∀ (x : X) (x_1 : ι), f x x_1 = (∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) p μ
⊢ MemLp f p μ
have this : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i
Tactic: have : f = ∑ i, (Pi.single i) ∘ (f · i) := by ext; simp
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) p μ
this : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i
⊢ MemLp f p μ
have rw : MemLp (ε := (i : ι) → E i) (∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) p μ
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) p μ
this : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i
⊢ MemLp (ε := (i : ι) → E i) (∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) p μ
have refine : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    MemLp (ε := (i : ι) → E i) (Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) p μ
Tactic: refine memLp_finsetSum' _ fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) p μ
⊢ MemLp f p μ
have have : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i
Tactic: classical
    have : f = ∑ i, (Pi.single i) ∘ (f · i) := by ext; simp
    rw [this]
    refine memLp_finsetSum' _ fun i _ ↦ ?_
    exact (Isometry.single i).lipschitz.comp_memLp (by simp) (hf i)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) p μ
have : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i
⊢ MemLp f p μ
have have₁ : ∀ (this : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i), MemLp f p μ
Tactic: classical
    have : f = ∑ i, (Pi.single i) ∘ (f · i) := by ext; simp
    rw [this]
    refine memLp_finsetSum' _ fun i _ ↦ ?_
    exact (Isometry.single i).lipschitz.comp_memLp (by simp) (hf i)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) p μ
have : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i
have₁ : ∀ (this : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i), MemLp f p μ
have₂ : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i
have₃ have₄ : ∀ (this : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i), MemLp f p μ
⊢ MemLp f p μ
have have₅ : ∀ (this : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i),
  MemLp (ε := (i : ι) → E i) (∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) p μ
Tactic: classical
    have : f = ∑ i, (Pi.single i) ∘ (f · i) := by ext; simp
    rw [this]
    refine memLp_finsetSum' _ fun i _ ↦ ?_
    exact (Isometry.single i).lipschitz.comp_memLp (by simp) (hf i)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) p μ
have : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i
have₁ : ∀ (this : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i), MemLp f p μ
have₂ : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i
have₃ have₄ : ∀ (this : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i), MemLp f p μ
have₅ :
  ∀ (this : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i),
    MemLp (ε := (i : ι) → E i) (∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) p μ
⊢ MemLp f p μ
have have₆ : ∀ (this : f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    MemLp (ε := (i : ι) → E i) (Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) p μ
Tactic: classical
    have : f = ∑ i, (Pi.single i) ∘ (f · i) := by ext; simp
    rw [this]
    refine memLp_finsetSum' _ fun i _ ↦ ?_
    exact (Isometry.single i).lipschitz.comp_memLp (by simp) (hf i)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
⊢ Integrable f μ ↔ ∀ (i : ι), Integrable.{u_3, u_1} (ε := E i) (fun (x : X) ↦ f x i) μ
have simp_rw : MemLp f 1 μ ↔ ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) 1 μ
Tactic: simp_rw [← memLp_one_iff_integrable, memLp_pi_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : X → E × F
h : MemLp.{u_1, u_2} (ε := E) (fun (x : X) ↦ (f x).1) p μ ∧ MemLp.{u_1, u_3} (ε := F) (fun (x : X) ↦ (f x).2) p μ
⊢ f =
    HAdd.hAdd (α := X → E × F)
      (Function.comp (β := E) (⇑(AddMonoidHom.inl E F) : (a : E) → E × F) fun (x : X) ↦ (f x).1)
      (Function.comp (β := F) (⇑(AddMonoidHom.inr E F) : (a : F) → E × F) fun (x : X) ↦ (f x).2)
have h₁ : ∀ (x : X),
  (f x).1 =
    (HAdd.hAdd (α := X → E × F) (β := X → E × F)
        (Function.comp (β := E) (⇑(AddMonoidHom.inl E F) : (a : E) → E × F) fun (x : X) ↦ (f x).1)
        (Function.comp (β := F) (⇑(AddMonoidHom.inr E F) : (a : F) → E × F) fun (x : X) ↦ (f x).2) x).1
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : X → E × F
h : MemLp.{u_1, u_2} (ε := E) (fun (x : X) ↦ (f x).1) p μ ∧ MemLp.{u_1, u_3} (ε := F) (fun (x : X) ↦ (f x).2) p μ
h₁ :
  ∀ (x : X),
    (f x).1 =
      (HAdd.hAdd (α := X → E × F) (β := X → E × F)
          (Function.comp (β := E) (⇑(AddMonoidHom.inl E F) : (a : E) → E × F) fun (x : X) ↦ (f x).1)
          (Function.comp (β := F) (⇑(AddMonoidHom.inr E F) : (a : F) → E × F) fun (x : X) ↦ (f x).2) x).1
⊢ f =
    HAdd.hAdd (α := X → E × F)
      (Function.comp (β := E) (⇑(AddMonoidHom.inl E F) : (a : E) → E × F) fun (x : X) ↦ (f x).1)
      (Function.comp (β := F) (⇑(AddMonoidHom.inr E F) : (a : F) → E × F) fun (x : X) ↦ (f x).2)
have h₂ : ∀ (x : X),
  (f x).2 =
    (HAdd.hAdd (α := X → E × F) (β := X → E × F)
        (Function.comp (β := E) (⇑(AddMonoidHom.inl E F) : (a : E) → E × F) fun (x : X) ↦ (f x).1)
        (Function.comp (β := F) (⇑(AddMonoidHom.inr E F) : (a : F) → E × F) fun (x : X) ↦ (f x).2) x).2
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.Pi (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : X → E × F
h : MemLp.{u_1, u_2} (ε := E) (fun (x : X) ↦ (f x).1) p μ ∧ MemLp.{u_1, u_3} (ε := F) (fun (x : X) ↦ (f x).2) p μ
this :
  f =
    HAdd.hAdd (α := X → E × F)
      (Function.comp (β := E) (⇑(AddMonoidHom.inl E F) : (a : E) → E × F) fun (x : X) ↦ (f x).1)
      (Function.comp (β := F) (⇑(AddMonoidHom.inr E F) : (a : F) → E × F) fun (x : X) ↦ (f x).2)
⊢ MemLp f p μ
have rw : MemLp
  (HAdd.hAdd (α := X → E × F) (Function.comp (β := E) (⇑(AddMonoidHom.inl E F) : (a : E) → E × F) fun (x : X) ↦ (f x).1)
    (Function.comp (β := F) (⇑(AddMonoidHom.inr E F) : (a : F) → E × F) fun (x : X) ↦ (f x).2))
  p μ
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst : Fact (1 ≤ q)
ι : Type u_2
inst_1 : Fintype ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
⊢ MemLp f p μ ↔ ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ (f x).ofLp i) p μ
have simp_rw : MemLp f p μ ↔ MemLp (ε := (i : ι) → E i) (fun (x : X) ↦ (WithLp.ofLp ∘ f) x) p μ
Tactic: simp_rw [← memLp_pi_iff, ← Function.comp_apply (f := WithLp.ofLp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
ι : Type u_2
inst_1 : Fintype ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
⊢ Integrable f μ ↔ ∀ (i : ι), Integrable.{u_3, u_1} (ε := E i) (fun (x : X) ↦ (f x).ofLp i) μ
have simp_rw : MemLp f 1 μ ↔ ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ (f x).ofLp i) 1 μ
Tactic: simp_rw [← memLp_one_iff_integrable, memLp_piLp_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
ι : Type u_2
inst_1 : Fintype ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
inst_3 : (i : ι) → NormedSpace ℝ (E i)
inst_4 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
hf : ∀ (i : ι), Integrable.{u_3, u_1} (ε := E i) (fun (x : X) ↦ (f x).ofLp i) μ
i : ι
⊢ Eq.{u_3 + 1} (α := E i) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ) i) (∫ (x : X), (f x).ofLp i ∂μ)
have rw : Eq.{u_3 + 1} (α := E i) (∫ (x : X), (PiLp.proj q E i : (a : PiLp q E) → E i) (f x) ∂μ) (∫ (x : X), (f x).ofLp i ∂μ)
Tactic: rw [← PiLp.proj_apply (𝕜 := ℝ) q E i (∫ x, f x ∂μ), ← ContinuousLinearMap.integral_comp_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
ι : Type u_2
inst_1 : Fintype ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
inst_3 : (i : ι) → NormedSpace ℝ (E i)
inst_4 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
hf : ∀ (i : ι), Integrable.{u_3, u_1} (ε := E i) (fun (x : X) ↦ (f x).ofLp i) μ
i : ι
rw : Eq.{u_3 + 1} (α := E i) (∫ (x : X), (PiLp.proj q E i : (a : PiLp q E) → E i) (f x) ∂μ) (∫ (x : X), (f x).ofLp i ∂μ)
⊢ Eq.{u_3 + 1} (α := E i) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ) i) (∫ (x : X), (f x).ofLp i ∂μ)
have φ_int : Integrable f μ
Tactic: rw [← PiLp.proj_apply (𝕜 := ℝ) q E i (∫ x, f x ∂μ), ← ContinuousLinearMap.integral_comp_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : X → WithLp q (E × F)
⊢ MemLp f p μ ↔
    MemLp.{u_1, u_2} (ε := E) (fun (x : X) ↦ (f x).fst) p μ ∧ MemLp.{u_1, u_3} (ε := F) (fun (x : X) ↦ (f x).snd) p μ
have simp_rw : MemLp f p μ ↔ MemLp (ε := E × F) (fun (x : X) ↦ (f x).ofLp) p μ
Tactic: simp_rw [← WithLp.ofLp_fst, ← WithLp.ofLp_snd, ← memLp_prod_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : X → WithLp q (E × F)
⊢ Integrable f μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : X) ↦ (f x).fst) μ ∧
      Integrable.{u_3, u_1} (ε := F) (fun (x : X) ↦ (f x).snd) μ
have simp_rw : MemLp f 1 μ ↔
  MemLp.{u_1, u_2} (ε := E) (fun (x : X) ↦ (f x).fst) 1 μ ∧ MemLp.{u_1, u_3} (ε := F) (fun (x : X) ↦ (f x).snd) 1 μ
Tactic: simp_rw [← memLp_one_iff_integrable, memLp_prodLp_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.WithLp (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
hf : Integrable f μ
| Eq.{u_2 + 1} (α := E) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).1 (∫ (x : X), (f x).fst ∂μ)
have enter : WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)
Tactic: enter [1, 1]