awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
hfg : f =ᶠ[ae μ] g
h_ae :
  Integrable f μ →
    (fun (φ : X → E) ↦
          Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
        f →
      (fun (φ : X → E) ↦
          Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
        g
⊢ Integrable f μ →
    (fun (φ : X → E) ↦
          Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
        f →
      (fun (φ : X → E) ↦
          Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
        g

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
hfg : f =ᶠ[ae μ] g
h : Integrable f μ
hf : Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (f x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), f x ∂μ) : F)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (f x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), f x ∂μ) : F)

Tactic:
hf
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
hfg : f =ᶠ[ae μ] g
h_1 : Integrable f μ
hf : Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (f x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), f x ∂μ) : F)
h : Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (g x) ∂μ) (∫ (x : X), (L : (a : E) → F) (f x) ∂μ)
h₁ : Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (∫ (x : X), g x ∂μ) : F) ((L : (a : E) → F) (∫ (x : X), f x ∂μ) : F)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (g x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), g x ∂μ) : F)

Tactic:
convert! hf using 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
hfg : f =ᶠ[ae μ] g
h : Integrable f μ
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (g x) ∂μ) (∫ (x : X), (L : (a : E) → F) (f x) ∂μ)

Tactic:
integral_congr_ae (hfg.fun_comp L).symm

Premises used: MeasureTheory.integral_congr_ae, Filter.EventuallyEq.fun_comp, DFunLike.coe, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
hfg : f =ᶠ[ae μ] g
h : Integrable f μ
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (g x) ∂μ) (∫ (x : X), (L : (a : E) → F) (f x) ∂μ)

Tactic:
exact integral_congr_ae (hfg.fun_comp L).symm

Premises used: MeasureTheory.integral_congr_ae, Filter.EventuallyEq.fun_comp, DFunLike.coe, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
hfg : f =ᶠ[ae μ] g
h_1 : Integrable f μ
h h₁ : Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (∫ (a : X), f a ∂μ) : F) ((L : (a : E) → F) (∫ (x : X), f x ∂μ) : F)
⊢ Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (∫ (x : X), g x ∂μ) : F) ((L : (a : E) → F) (∫ (x : X), f x ∂μ) : F)

Tactic:
rw [integral_congr_ae hfg.symm]

Premises used: MeasureTheory.integral_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
Fₗ : Type u_5
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup Fₗ
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace ℝ Fₗ
inst_7 : CompleteSpace Fₗ
inst_8 : NormedSpace ℝ E
inst_9 : CompleteSpace E
L : E →L[𝕜] Fₗ
φ : X → E
φ_int : Integrable φ μ
⊢ ∀ (r : ℝ) (x : 𝕜), (RingHom.id 𝕜 : (a : 𝕜) → 𝕜) (r • x) = HSMul.hSMul (β := 𝕜) r ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
H : Type u_8
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
pos :
  ∀ (hE : CompleteSpace E),
    Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)
neg :
  ∀ (hE : ¬CompleteSpace E),
    Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
H : Type u_8
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
hE : CompleteSpace E
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)

Tactic:
((ContinuousLinearMap.apply 𝕜 E v).integral_comp_comm φ_int).symm

Premises used: ContinuousLinearMap.apply, Eq.symm, ContinuousLinearMap.integral_comp_comm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
H : Type u_8
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
hE : CompleteSpace E
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)

Tactic:
exact ((ContinuousLinearMap.apply 𝕜 E v).integral_comp_comm φ_int).symm

Premises used: ContinuousLinearMap.apply, Eq.symm, ContinuousLinearMap.integral_comp_comm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
H : Type u_8
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
hE : ¬CompleteSpace E
neg :
  ∀ (hH : Subsingleton H),
    Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)
neg₁ :
  ∀ (hH : Nontrivial H),
    Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)

Tactic:
rcases subsingleton_or_nontrivial H with hH | hH

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
H : Type u_8
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
hE : ¬CompleteSpace E
hH : Subsingleton H
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)

Tactic:
simp [Subsingleton.eq_zero v]

Premises used: Subsingleton.eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
H : Type u_8
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
hE : ¬CompleteSpace E
hH : Nontrivial H
rwa rwa₁ rwa₂ rwa₃ : ¬CompleteSpace E
⊢ ¬CompleteSpace (H →L[𝕜] E)

Tactic:
rwa [SeparatingDual.completeSpace_continuousLinearMap_iff]

Premises used: SeparatingDual.completeSpace_continuousLinearMap_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
H : Type u_8
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
hE : ¬CompleteSpace E
hH : Nontrivial H
⊢ ¬CompleteSpace (H →L[𝕜] E)

Tactic:
have : ¬(CompleteSpace (H →L[𝕜] E)) := by
        rwa [SeparatingDual.completeSpace_continuousLinearMap_iff]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
H : Type u_8
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
hE : ¬CompleteSpace E
hH : Nontrivial H
this : ¬CompleteSpace (H →L[𝕜] E)
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)

Tactic:
simp [integral, hE, this]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
ι : Type u_8
inst_5 : Fintype ι
M : ι → Type u_9
inst_6 : (i : ι) → NormedAddCommGroup (M i)
inst_7 : (i : ι) → NormedSpace.{u_6, u_9} 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
pos :
  ∀ (hE : CompleteSpace E),
    Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
      (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)
neg :
  ∀ (hE : ¬CompleteSpace E),
    Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
      (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
    (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
ι : Type u_8
inst_5 : Fintype ι
M : ι → Type u_9
inst_6 : (i : ι) → NormedAddCommGroup (M i)
inst_7 : (i : ι) → NormedSpace.{u_6, u_9} 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : CompleteSpace E
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
    (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)

Tactic:
((ContinuousMultilinearMap.apply 𝕜 M E m).integral_comp_comm φ_int).symm

Premises used: Eq.symm, ContinuousLinearMap.integral_comp_comm, ContinuousMultilinearMap.apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
ι : Type u_8
inst_5 : Fintype ι
M : ι → Type u_9
inst_6 : (i : ι) → NormedAddCommGroup (M i)
inst_7 : (i : ι) → NormedSpace.{u_6, u_9} 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : CompleteSpace E
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
    (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)

Tactic:
exact ((ContinuousMultilinearMap.apply 𝕜 M E m).integral_comp_comm φ_int).symm

Premises used: Eq.symm, ContinuousLinearMap.integral_comp_comm, ContinuousMultilinearMap.apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
ι : Type u_8
inst_5 : Fintype ι
M : ι → Type u_9
inst_6 : (i : ι) → NormedAddCommGroup (M i)
inst_7 : (i : ι) → NormedSpace.{u_6, u_9} 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
pos :
  ∀ (hm : ∀ (i : ι), m i ≠ 0),
    Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
      (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)
neg :
  ∀ (hm : ∃ (i : ι), m i = 0),
    Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
      (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
    (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)

Tactic:
by_cases! hm : ∀ i, m i ≠ 0
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
ι : Type u_8
inst_5 : Fintype ι
M : ι → Type u_9
inst_6 : (i : ι) → NormedAddCommGroup (M i)
inst_7 : (i : ι) → NormedSpace.{u_6, u_9} 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
hm : ∀ (i : ι), m i ≠ 0
rwa rwa₁ rwa₂ rwa₃ : ¬CompleteSpace E
⊢ ¬CompleteSpace (ContinuousMultilinearMap 𝕜 M E)

Tactic:
rwa [SeparatingDual.completeSpace_continuousMultilinearMap_iff _ _ hm]

Premises used: SeparatingDual.completeSpace_continuousMultilinearMap_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
ι : Type u_8
inst_5 : Fintype ι
M : ι → Type u_9
inst_6 : (i : ι) → NormedAddCommGroup (M i)
inst_7 : (i : ι) → NormedSpace.{u_6, u_9} 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
hm : ∀ (i : ι), m i ≠ 0
⊢ ¬CompleteSpace (ContinuousMultilinearMap 𝕜 M E)

Tactic:
have : ¬ CompleteSpace (ContinuousMultilinearMap 𝕜 M E) := by
        rwa [SeparatingDual.completeSpace_continuousMultilinearMap_iff _ _ hm]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
ι : Type u_8
inst_5 : Fintype ι
M : ι → Type u_9
inst_6 : (i : ι) → NormedAddCommGroup (M i)
inst_7 : (i : ι) → NormedSpace.{u_6, u_9} 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
hm : ∀ (i : ι), m i ≠ 0
this : ¬CompleteSpace (ContinuousMultilinearMap 𝕜 M E)
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
    (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)

Tactic:
simp [integral, hE, this]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
ι : Type u_8
inst_5 : Fintype ι
M : ι → Type u_9
inst_6 : (i : ι) → NormedAddCommGroup (M i)
inst_7 : (i : ι) → NormedSpace.{u_6, u_9} 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
hm : ∃ (i : ι), m i = 0
neg :
  ∀ (i : ι) (hi : m i = 0),
    Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
      (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
    (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)

Tactic:
rcases hm with ⟨i, hi⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
ι : Type u_8
inst_5 : Fintype ι
M : ι → Type u_9
inst_6 : (i : ι) → NormedAddCommGroup (M i)
inst_7 : (i : ι) → NormedSpace.{u_6, u_9} 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
i : ι
hi : m i = 0
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : (i : ι) → M i) → E) m : E)
    (∫ (x : X), (φ x : (a : (i : ι) → M i) → E) m ∂μ : E)

Tactic:
simp [ContinuousMultilinearMap.map_coord_zero _ i hi]

Premises used: ContinuousMultilinearMap.map_coord_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
Fₗ : Type u_5
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup Fₗ
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace ℝ Fₗ
inst_7 : CompleteSpace Fₗ
inst_8 : NormedSpace ℝ E
inst_9 : CompleteSpace E
L : E →L[𝕜] Fₗ
K : ℝ≥0
hL : AntilipschitzWith.{u_3, u_5} (α := E) (β := Fₗ) K (⇑L : (a : E) → Fₗ)
φ : X → E
pos :
  ∀ (h : Integrable φ μ),
    Eq.{u_5 + 1} (α := Fₗ) (∫ (x : X), (L : (a : E) → Fₗ) (φ x) ∂μ : Fₗ) ((L : (a : E) → Fₗ) (∫ (x : X), φ x ∂μ) : Fₗ)
neg :
  ∀ (h : ¬Integrable φ μ),
    Eq.{u_5 + 1} (α := Fₗ) (∫ (x : X), (L : (a : E) → Fₗ) (φ x) ∂μ : Fₗ) ((L : (a : E) → Fₗ) (∫ (x : X), φ x ∂μ) : Fₗ)
⊢ Eq.{u_5 + 1} (α := Fₗ) (∫ (x : X), (L : (a : E) → Fₗ) (φ x) ∂μ : Fₗ) ((L : (a : E) → Fₗ) (∫ (x : X), φ x ∂μ) : Fₗ)

Tactic:
by_cases h : Integrable φ μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
Fₗ : Type u_5
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup Fₗ
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace ℝ Fₗ
inst_7 : CompleteSpace Fₗ
inst_8 : NormedSpace ℝ E
inst_9 : CompleteSpace E
L : E →L[𝕜] Fₗ
K : ℝ≥0
hL : AntilipschitzWith.{u_3, u_5} (α := E) (β := Fₗ) K (⇑L : (a : E) → Fₗ)
φ : X → E
h : Integrable φ μ
⊢ Eq.{u_5 + 1} (α := Fₗ) (∫ (x : X), (L : (a : E) → Fₗ) (φ x) ∂μ : Fₗ) ((L : (a : E) → Fₗ) (∫ (x : X), φ x ∂μ) : Fₗ)

Tactic:
integral_comp_comm L h

Premises used: ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
Fₗ : Type u_5
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup Fₗ
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace ℝ Fₗ
inst_7 : CompleteSpace Fₗ
inst_8 : NormedSpace ℝ E
inst_9 : CompleteSpace E
L : E →L[𝕜] Fₗ
K : ℝ≥0
hL : AntilipschitzWith.{u_3, u_5} (α := E) (β := Fₗ) K (⇑L : (a : E) → Fₗ)
φ : X → E
h : Integrable φ μ
⊢ Eq.{u_5 + 1} (α := Fₗ) (∫ (x : X), (L : (a : E) → Fₗ) (φ x) ∂μ : Fₗ) ((L : (a : E) → Fₗ) (∫ (x : X), φ x ∂μ) : Fₗ)

Tactic:
exact integral_comp_comm L h

Premises used: ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
Fₗ : Type u_5
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup Fₗ
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace ℝ Fₗ
inst_7 : CompleteSpace Fₗ
inst_8 : NormedSpace ℝ E
inst_9 : CompleteSpace E
L : E →L[𝕜] Fₗ
K : ℝ≥0
hL : AntilipschitzWith.{u_3, u_5} (α := E) (β := Fₗ) K (⇑L : (a : E) → Fₗ)
φ : X → E
h : ¬Integrable φ μ
rwa : ¬Integrable.{u_5, u_1} (ε := Fₗ) ((⇑L : (a : E) → Fₗ) ∘ φ) μ
rwa₁ rwa₂ rwa₃ rwa₄ : ¬Integrable φ μ
⊢ ¬Integrable.{u_5, u_1} (ε := Fₗ) (fun (x : X) ↦ (L : (a : E) → Fₗ) (φ x)) μ

Tactic:
rwa [← Function.comp_def,
      LipschitzWith.integrable_comp_iff_of_antilipschitz L.lipschitz hL L.map_zero]

Premises used: MeasureTheory.LipschitzWith.integrable_comp_iff_of_antilipschitz, ContinuousLinearMap.map_zero, ContinuousLinearMap.lipschitz, Function.comp_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
Fₗ : Type u_5
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup Fₗ
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace ℝ Fₗ
inst_7 : CompleteSpace Fₗ
inst_8 : NormedSpace ℝ E
inst_9 : CompleteSpace E
L : E →L[𝕜] Fₗ
K : ℝ≥0
hL : AntilipschitzWith.{u_3, u_5} (α := E) (β := Fₗ) K (⇑L : (a : E) → Fₗ)
φ : X → E
h : ¬Integrable φ μ
⊢ ¬Integrable.{u_5, u_1} (ε := Fₗ) (fun (x : X) ↦ (L : (a : E) → Fₗ) (φ x)) μ

Tactic:
have : ¬Integrable (fun x => L (φ x)) μ := by
    rwa [← Function.comp_def,
      LipschitzWith.integrable_comp_iff_of_antilipschitz L.lipschitz hL L.map_zero]