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

Tactic:
have : f = ∑ i, (Pi.single i) ∘ (f · i) := by ext; simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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
rw : MemLp (ε := (i : ι) → E i) (∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) p μ
⊢ MemLp f p μ

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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 μ

Tactic:
memLp_finsetSum' _ fun i _ ↦ ?_

Premises used: MeasureTheory.memLp_finsetSum'
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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
refine :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      MemLp (ε := (i : ι) → E i) (Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) p μ
⊢ MemLp (ε := (i : ι) → E i) (∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) p μ

Tactic:
refine memLp_finsetSum' _ fun i _ ↦ ?_

Premises used: MeasureTheory.memLp_finsetSum'
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Eq (α := (i : ι) → E i) (Pi.single (M := E) i 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ MemLp (ε := (i : ι) → E i) (Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) p μ

Tactic:
exact (Isometry.single i).lipschitz.comp_memLp (by simp) (hf i)

Premises used: LipschitzWith.comp_memLp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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 μ
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 μ
⊢ 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)

Premises used: MeasureTheory.memLp_finsetSum'
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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
simp_rw : MemLp f 1 μ ↔ ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) 1 μ
⊢ Integrable f μ ↔ ∀ (i : ι), Integrable.{u_3, u_1} (ε := E i) (fun (x : X) ↦ f x i) μ

Tactic:
simp_rw [← memLp_one_iff_integrable, memLp_pi_iff]

Premises used: MeasureTheory.memLp_pi_iff, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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
inst_2 : (i : ι) → NormedSpace ℝ (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
hf : ∀ (i : ι), Integrable.{u_3, u_1} (ε := E i) (fun (x : X) ↦ f x i) μ
i : ι
⊢ Eq.{u_3 + 1} (α := E i) ((∫ (x : X), f x ∂μ) i) (∫ (x : X), f x i ∂μ)

Tactic:
simp [← ContinuousLinearMap.proj_apply (R := ℝ) i (∫ x, f x ∂μ),
    ← ContinuousLinearMap.integral_comp_comm _ (Integrable.of_eval hf)]

Premises used: MeasureTheory.Integrable.of_eval, ContinuousLinearMap.proj_apply, MeasureTheory.integral, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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 f p μ
⊢ Eq.{u_2 + 1} (α := E) 0.1 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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 f p μ
⊢ Eq.{u_3 + 1} (α := F) 0.2 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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
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
⊢ 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)

Tactic:
ext
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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 μ
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:
simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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 μ
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:
simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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)
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 μ
⊢ MemLp f p μ

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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)
⊢ Eq (α := E × F) ((AddMonoidHom.inl E F : (a : E) → E × F) 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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)
⊢ Eq (α := E × F) ((AddMonoidHom.inr E F : (a : F) → E × F) 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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 f p μ
⊢ MemLp.{u_1, u_2} (ε := E) (fun (x : X) ↦ (f x).1) p μ

Tactic:
memLp_prod_iff.1 h |>.1

Premises used: MeasureTheory.memLp_prod_iff, And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
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 f p μ
⊢ MemLp.{u_1, u_3} (ε := F) (fun (x : X) ↦ (f x).2) p μ

Tactic:
memLp_prod_iff.1 h |>.2

Premises used: MeasureTheory.memLp_prod_iff, And.right, Iff.mp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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
simp_rw : MemLp f p μ ↔ MemLp (ε := (i : ι) → E i) (fun (x : X) ↦ (WithLp.ofLp ∘ f) x) p μ
⊢ MemLp f p μ ↔ ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ (f x).ofLp i) p μ

Tactic:
simp_rw [← memLp_pi_iff, ← Function.comp_apply (f := WithLp.ofLp)]

Premises used: MeasureTheory.memLp_pi_iff, Function.comp_apply
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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
⊢ Eq (α := (i : ι) → E i) (WithLp.ofLp (p := q) 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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 μ ↔ MemLp (ε := (i : ι) → E i) (fun (x : X) ↦ (WithLp.ofLp ∘ f) x) p μ

Tactic:
exact (PiLp.lipschitzWith_ofLp q E).memLp_comp_iff_of_antilipschitz
    (PiLp.antilipschitzWith_ofLp q E) (by simp) |>.symm

Premises used: LipschitzWith.memLp_comp_iff_of_antilipschitz, PiLp.lipschitzWith_ofLp, PiLp.antilipschitzWith_ofLp, Iff.symm
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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
simp_rw : MemLp f 1 μ ↔ ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ (f x).ofLp i) 1 μ
⊢ Integrable f μ ↔ ∀ (i : ι), Integrable.{u_3, u_1} (ε := E i) (fun (x : X) ↦ (f x).ofLp i) μ

Tactic:
simp_rw [← memLp_one_iff_integrable, memLp_piLp_iff]

Premises used: MeasureTheory.memLp_piLp_iff, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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 ∂μ)
φ_int : Integrable f μ
⊢ Eq.{u_3 + 1} (α := E i) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ) i) (∫ (x : X), (f x).ofLp i ∂μ)

Tactic:
rw [← PiLp.proj_apply (𝕜 := ℝ) q E i (∫ x, f x ∂μ), ← ContinuousLinearMap.integral_comp_comm]

Premises used: MeasureTheory.integral, PiLp.proj_apply, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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) (∫ (x : X), (PiLp.proj q E i : (a : PiLp q E) → E i) (f x) ∂μ) (∫ (x : X), (f x).ofLp i ∂μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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 : ι
⊢ Integrable f μ

Tactic:
Integrable.of_eval_piLp hf

Premises used: MeasureTheory.Integrable.of_eval_piLp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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 : ι
⊢ Integrable f μ

Tactic:
exact Integrable.of_eval_piLp hf

Premises used: MeasureTheory.Integrable.of_eval_piLp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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)
simp_rw : MemLp f p μ ↔ MemLp (ε := E × F) (fun (x : X) ↦ (f x).ofLp) p μ
⊢ 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 μ

Tactic:
simp_rw [← WithLp.ofLp_fst, ← WithLp.ofLp_snd, ← memLp_prod_iff]

Premises used: WithLp.ofLp_fst, MeasureTheory.memLp_prod_iff, WithLp.ofLp_snd
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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)
⊢ Eq (α := E × F) (WithLp.ofLp (p := q) 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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 (ε := E × F) (fun (x : X) ↦ (f x).ofLp) p μ

Tactic:
exact (WithLp.prod_lipschitzWith_ofLp q E F).memLp_comp_iff_of_antilipschitz
    (WithLp.prod_antilipschitzWith_ofLp q E F) (by simp) |>.symm

Premises used: LipschitzWith.memLp_comp_iff_of_antilipschitz, WithLp.prod_lipschitzWith_ofLp, Iff.symm, WithLp.prod_antilipschitzWith_ofLp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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)
h : MemLp f p μ
⊢ MemLp.{u_1, u_2} (ε := E) (fun (x : X) ↦ (f x).fst) p μ

Tactic:
memLp_prodLp_iff.1 h |>.1

Premises used: And.left, MeasureTheory.memLp_prodLp_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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)
h : MemLp f p μ
⊢ MemLp.{u_1, u_3} (ε := F) (fun (x : X) ↦ (f x).snd) p μ

Tactic:
memLp_prodLp_iff.1 h |>.2

Premises used: And.right, MeasureTheory.memLp_prodLp_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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)
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 μ
⊢ 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) μ

Tactic:
simp_rw [← memLp_one_iff_integrable, memLp_prodLp_iff]

Premises used: MeasureTheory.memLp_prodLp_iff, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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)
h : Integrable f μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : X) ↦ (f x).fst) μ

Tactic:
integrable_prodLp_iff.1 h |>.1

Premises used: MeasureTheory.integrable_prodLp_iff, And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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)
h : Integrable f μ
⊢ Integrable.{u_3, u_1} (ε := F) (fun (x : X) ↦ (f x).snd) μ

Tactic:
integrable_prodLp_iff.1 h |>.2

Premises used: MeasureTheory.integrable_prodLp_iff, And.right, Iff.mp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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 μ
enter : WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)
| Eq.{u_2 + 1} (α := E) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).1 (∫ (x : X), (f x).fst ∂μ)

Tactic:
enter [1, 1]
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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 μ
enter : (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)
| Eq.{u_2 + 1} (α := E) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).1 (∫ (x : X), (f x).fst ∂μ)

Tactic:
enter [1, 1]; change WithLp.prodContinuousLinearEquiv q ℝ E F _

Premises used: Real, WithLp.prodContinuousLinearEquiv, DFunLike.coe
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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 μ
conv :
  Eq.{u_2 + 1} (α := E)
    ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)).1
    (∫ (x : X), (f x).fst ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (WithLp.ofLp (p := q) (∫ (x : X), f x ∂μ)).1 (∫ (x : X), (f x).fst ∂μ)

Tactic:
conv => enter [1, 1]; change WithLp.prodContinuousLinearEquiv q ℝ E F _

Premises used: Real, WithLp.prodContinuousLinearEquiv, DFunLike.coe
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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 μ
rw :
  Eq.{u_2 + 1} (α := E)
    (∫ (x : X), ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)).1 ∂μ)
    (∫ (x : X), (f x).fst ∂μ)
rw₁ :
  Integrable (ε := E × F)
    (fun (x : X) ↦ (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)) μ
⊢ Eq.{u_2 + 1} (α := E)
    ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (∫ (x : X), f x ∂μ)).1
    (∫ (x : X), (f x).fst ∂μ)

Tactic:
rw [← ContinuousLinearEquiv.integral_comp_comm, fst_integral]

Premises used: ContinuousLinearEquiv.integral_comp_comm, fst_integral
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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)
    (∫ (x : X), ((WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)).1 ∂μ)
    (∫ (x : X), (f x).fst ∂μ)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp
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 μ
⊢ Integrable (ε := E × F)
    (fun (x : X) ↦ (WithLp.prodContinuousLinearEquiv q ℝ E F : (a : WithLp q (E × F)) → E × F) (f x)) μ

Tactic:
(ContinuousLinearEquiv.integrable_comp_iff _).2 hf

Premises used: Iff.mpr, setOf, ContinuousLinearEquiv.integrable_comp_iff