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_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 φ μ
this : ¬Integrable.{u_5, u_1} (ε := Fₗ) (fun (x : X) ↦ (L : (a : E) → Fₗ) (φ x)) μ
⊢ Eq.{u_5 + 1} (α := Fₗ) (∫ (x : X), (L : (a : E) → Fₗ) (φ x) ∂μ : Fₗ) ((L : (a : E) → Fₗ) (∫ (x : X), φ x ∂μ) : Fₗ)

Tactic:
simp [integral_undef, h, this]

Premises used: MeasureTheory.integral_undef
-- 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ₗ
φ : ↥(Lp E 1 μ)
⊢ Eq.{u_5 + 1} (α := Fₗ) (∫ (x : X), (L : (a : E) → Fₗ) ((↑(↑φ : X →ₘ[μ] E) : X → E) x) ∂μ : Fₗ)
    ((L : (a : E) → Fₗ) (∫ (x : X), (↑(↑φ : X →ₘ[μ] E) : X → E) x ∂μ) : Fₗ)

Tactic:
L.integral_comp_comm (L1.integrable_coeFn φ)

Premises used: MeasureTheory.L1.integrable_coeFn, ContinuousLinearMap.integral_comp_comm
-- 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
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedSpace ℝ F
inst_8 : CompleteSpace E
inst_9 : NormedSpace ℝ E
L : E →ₗᵢ[𝕜] F
φ : X → E
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)

Tactic:
L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _

Premises used: ContinuousLinearMap.integral_comp_comm', LinearIsometry.antilipschitz, LinearIsometry.toContinuousLinearMap
-- 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
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 : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
⊢ CompleteSpace E ↔ CompleteSpace F

Tactic:
have : CompleteSpace E ↔ CompleteSpace F :=
    completeSpace_congr (e := L.toEquiv) L.isUniformEmbedding
-- 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
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 : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
this : CompleteSpace E ↔ CompleteSpace F
inl :
  CompleteSpace E →
    CompleteSpace F →
      Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)
inr :
  ¬CompleteSpace E →
    ¬CompleteSpace F →
      Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)

Tactic:
obtain ⟨_, _⟩ | ⟨_, _⟩ := iff_iff_and_or_not_and_not.mp this

Premises used: iff_iff_and_or_not_and_not, Iff.mp
-- 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
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 : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
this : CompleteSpace E ↔ CompleteSpace F
left : CompleteSpace E
right : CompleteSpace F
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)

Tactic:
L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _

Premises used: ContinuousLinearEquiv.antilipschitz, ContinuousLinearMap.integral_comp_comm', ContinuousLinearEquiv.toContinuousLinearMap
-- 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
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 : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
this : CompleteSpace E ↔ CompleteSpace F
left : CompleteSpace E
right : CompleteSpace F
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)

Tactic:
exact L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _

Premises used: ContinuousLinearEquiv.antilipschitz, ContinuousLinearMap.integral_comp_comm', ContinuousLinearEquiv.toContinuousLinearMap
-- 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
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 : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
this : CompleteSpace E ↔ CompleteSpace F
left : ¬CompleteSpace E
right : ¬CompleteSpace F
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)

Tactic:
simp [integral, *]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
Y : Type u_2
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
f : X → C(Y, E)
hf : Integrable f μ
y : Y
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), f x ∂μ : (a : Y) → E) y : E)
    ((evalCLM ℝ y : (a : C(Y, E)) → E) (∫ (x : X), f x ∂μ) : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
Y : Type u_2
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
f : X → C(Y, E)
hf : Integrable f μ
y : Y
⊢ Eq.{u_3 + 1} (α := E) ((evalCLM ℝ y : (a : C(Y, E)) → E) (∫ (x : X), f x ∂μ) : E)
    (∫ (x : X), (evalCLM ℝ y : (a : C(Y, E)) → E) (f x) ∂μ : E)

Tactic:
(ContinuousLinearMap.integral_comp_comm _ hf).symm

Premises used: Eq.symm, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
Y : Type u_2
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
f : X → C(Y, E)
hf : Integrable f μ
y : Y
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), (evalCLM ℝ y : (a : C(Y, E)) → E) (f x) ∂μ)
    (∫ (x : X), (evalCLM ℝ y : (a : C(Y, E)) → E) (f x) ∂μ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
Y : Type u_2
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
f : X → C(Y, E)
hf : Integrable f μ
y : Y
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), f x ∂μ : (a : Y) → E) y : E) (∫ (x : X), (f x : (a : Y) → E) y ∂μ : E)

Tactic:
calc (∫ x, f x ∂μ) y = ContinuousMap.evalCLM ℝ y (∫ x, f x ∂μ) := rfl
    _ = ∫ x, ContinuousMap.evalCLM ℝ y (f x) ∂μ :=
          (ContinuousLinearMap.integral_comp_comm _ hf).symm
    _ = _ := rfl

Premises used: Real, ContinuousMap.evalCLM, MeasureTheory.integral, Eq.symm, ContinuousLinearMap.integral_comp_comm, DFunLike.coe, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
R : Type u_8
inst_3 : NormedCommRing R
inst_4 : Zero Y
inst_5 : NormedAlgebra ℝ R
inst_6 : CompleteSpace R
f : X → C(Y, R)₀
hf : Integrable f μ
y : Y
⊢ Eq.{u_8 + 1} (α := R) ((∫ (x : X), f x ∂μ : (a : Y) → R) y : R)
    (((evalCLM ℝ y : C(Y, R)₀ →L[ℝ] R) : (a : C(Y, R)₀) → R) (∫ (x : X), f x ∂μ) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
R : Type u_8
inst_3 : NormedCommRing R
inst_4 : Zero Y
inst_5 : NormedAlgebra ℝ R
inst_6 : CompleteSpace R
f : X → C(Y, R)₀
hf : Integrable f μ
y : Y
⊢ Eq.{u_8 + 1} (α := R) (((evalCLM ℝ y : C(Y, R)₀ →L[ℝ] R) : (a : C(Y, R)₀) → R) (∫ (x : X), f x ∂μ) : R)
    (∫ (x : X), ((evalCLM ℝ y : C(Y, R)₀ →L[ℝ] R) : (a : C(Y, R)₀) → R) (f x) ∂μ : R)

Tactic:
(ContinuousLinearMap.integral_comp_comm _ hf).symm

Premises used: Eq.symm, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
R : Type u_8
inst_3 : NormedCommRing R
inst_4 : Zero Y
inst_5 : NormedAlgebra ℝ R
inst_6 : CompleteSpace R
f : X → C(Y, R)₀
hf : Integrable f μ
y : Y
⊢ Eq.{u_8 + 1} (α := R) (∫ (x : X), ((evalCLM ℝ y : C(Y, R)₀ →L[ℝ] R) : (a : C(Y, R)₀) → R) (f x) ∂μ)
    (∫ (x : X), ((evalCLM ℝ y : C(Y, R)₀ →L[ℝ] R) : (a : C(Y, R)₀) → R) (f x) ∂μ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
R : Type u_8
inst_3 : NormedCommRing R
inst_4 : Zero Y
inst_5 : NormedAlgebra ℝ R
inst_6 : CompleteSpace R
f : X → C(Y, R)₀
hf : Integrable f μ
y : Y
⊢ Eq.{u_8 + 1} (α := R) ((∫ (x : X), f x ∂μ : (a : Y) → R) y : R) (∫ (x : X), (f x : (a : Y) → R) y ∂μ : R)

Tactic:
calc (∫ x, f x ∂μ) y = ContinuousMapZero.evalCLM ℝ y (∫ x, f x ∂μ) := rfl
    _ = ∫ x, ContinuousMapZero.evalCLM ℝ y (f x) ∂μ :=
          (ContinuousLinearMap.integral_comp_comm _ hf).symm
    _ = _ := rfl

Premises used: Real, ContinuousMapZero.evalCLM, MeasureTheory.integral, Eq.symm, ContinuousLinearMap.integral_comp_comm, DFunLike.coe, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → ℝ
⊢ Eq.{u_6 + 1} (α := 𝕜) (∫ (x : X), (↑(f x) : 𝕜) ∂μ) (↑(∫ (x : X), f x ∂μ) : 𝕜)

Tactic:
(@RCLike.ofRealLI 𝕜 _).integral_comp_comm f

Premises used: RCLike.ofRealLI, LinearIsometry.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
f : X → ℝ
⊢ ∫ (x : X), (↑(f x) : ℂ) ∂μ = (↑(∫ (x : X), f x ∂μ) : ℂ)

Tactic:
integral_ofReal

Premises used: integral_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Eq (α := ℝ) (∫ (x : X), (re : (a : 𝕜) → ℝ) (f x) ∂μ : ℝ) ((re : (a : 𝕜) → ℝ) (∫ (x : X), f x ∂μ) : ℝ)

Tactic:
(@RCLike.reCLM 𝕜 _).integral_comp_comm hf

Premises used: RCLike.reCLM, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Eq (α := ℝ) (∫ (x : X), (im : (a : 𝕜) → ℝ) (f x) ∂μ : ℝ) ((im : (a : 𝕜) → ℝ) (∫ (x : X), f x ∂μ) : ℝ)

Tactic:
(@RCLike.imCLM 𝕜 _).integral_comp_comm hf

Premises used: RCLike.imCLM, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
⊢ Eq (α := 𝕜) (∫ (x : X), (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (f x) ∂μ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∫ (x : X), f x ∂μ) : 𝕜)

Tactic:
(@RCLike.conjLIE 𝕜 _).toLinearIsometry.integral_comp_comm f

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.integral_comp_comm, RCLike.conjLIE
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
rw :
  Eq.{u_6 + 1} (α := 𝕜)
    (∫ (a : X),
      (↑((re : (a : 𝕜) → ℝ) (f a)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜) ∂μ)
    (∫ (x : X), f x ∂μ)
hf₁ : Integrable.{u_6, u_1} (ε := 𝕜) (fun (x : X) ↦ (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜)) μ
hg : Integrable.{u_6, u_1} (ε := 𝕜) (fun (a : X) ↦ HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜)) μ
⊢ ∫ (x : X), (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) ∂μ +
      HMul.hMul (α := 𝕜) (∫ (x : X), (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) ∂μ) I =
    ∫ (x : X), f x ∂μ

Tactic:
rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add]

Premises used: MeasureTheory.integral_smul, mul_comm, smul_eq_mul, MeasureTheory.integral_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
e_f :
  Eq (α := X → 𝕜)
    (fun (a : X) ↦
      (↑((re : (a : 𝕜) → ℝ) (f a)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜))
    fun (x : X) ↦ f x
⊢ Eq.{u_6 + 1} (α := 𝕜)
    (∫ (a : X),
      (↑((re : (a : 𝕜) → ℝ) (f a)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜) ∂μ)
    (∫ (x : X), f x ∂μ)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
e_f :
  ∀ (x : X), (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) = f x
⊢ Eq (α := X → 𝕜)
    (fun (a : X) ↦
      (↑((re : (a : 𝕜) → ℝ) (f a)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜))
    fun (x : X) ↦ f x

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
x : X
e_f : (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) + HMul.hMul (α := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) = f x
e_f₁ : (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) I = f x
e_f₂ e_f₃ : f x = f x
⊢ (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) = f x

Tactic:
rw [smul_eq_mul, mul_comm, RCLike.re_add_im]

Premises used: RCLike.re_add_im, mul_comm, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Integrable.{u_6, u_1} (ε := 𝕜) (fun (x : X) ↦ (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜)) μ

Tactic:
hf.re.ofReal

Premises used: MeasureTheory.Integrable.re, MeasureTheory.Integrable.ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Integrable.{u_6, u_1} (ε := 𝕜) (fun (x : X) ↦ (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜)) μ

Tactic:
exact hf.re.ofReal

Premises used: MeasureTheory.Integrable.re, MeasureTheory.Integrable.ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Integrable.{u_6, u_1} (ε := 𝕜) (fun (a : X) ↦ HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜)) μ

Tactic:
hf.im.ofReal.smul (𝕜 := 𝕜) (β := 𝕜) RCLike.I

Premises used: MeasureTheory.Integrable.smul, RCLike.I, MeasureTheory.Integrable.ofReal, MeasureTheory.Integrable.im
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Integrable.{u_6, u_1} (ε := 𝕜) (fun (a : X) ↦ HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜)) μ

Tactic:
exact hf.im.ofReal.smul (𝕜 := 𝕜) (β := 𝕜) RCLike.I

Premises used: MeasureTheory.Integrable.smul, RCLike.I, MeasureTheory.Integrable.ofReal, MeasureTheory.Integrable.im
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
rw :
  ∫ (x : X), (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) ∂μ +
      HMul.hMul (α := 𝕜) (↑(∫ (x : X), (im : (a : 𝕜) → ℝ) (f x) ∂μ) : 𝕜) I =
    ∫ (x : X), f x ∂μ
rw₁ :
  ∫ (x : X), (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) ∂μ +
      HMul.hMul (α := 𝕜) (∫ (x : X), (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) ∂μ) I =
    ∫ (x : X), f x ∂μ
rw₂ rw₃ : Eq.{u_6 + 1} (α := 𝕜) (∫ (x : X), f x ∂μ) (∫ (x : X), f x ∂μ)
⊢ (↑(∫ (x : X), (re : (a : 𝕜) → ℝ) (f x) ∂μ) : 𝕜) +
      HMul.hMul (α := 𝕜) (↑(∫ (x : X), (im : (a : 𝕜) → ℝ) (f x) ∂μ) : 𝕜) I =
    ∫ (x : X), f x ∂μ

Tactic:
rw [← integral_ofReal, ← integral_ofReal, integral_coe_re_add_coe_im hf]

Premises used: integral_coe_re_add_coe_im, integral_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
i : Set X
hf : IntegrableOn f i μ
⊢ (↑(∫ (x : X) in i, (re : (a : 𝕜) → ℝ) (f x) ∂μ) : 𝕜) +
      HMul.hMul (α := 𝕜) (↑(∫ (x : X) in i, (im : (a : 𝕜) → ℝ) (f x) ∂μ) : 𝕜) I =
    ∫ (x : X) in i, f x ∂μ

Tactic:
integral_re_add_im hf

Premises used: integral_re_add_im
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
f : X → E × F
⊢ Eq (α := F × E) (Prod.swap (∫ (x : X), f x ∂μ)) (∫ (x : X), (f x).swap ∂μ)

Tactic:
.symm <| (ContinuousLinearEquiv.prodComm ℝ E F).integral_comp_comm f

Premises used: Real, ContinuousLinearEquiv.integral_comp_comm, ContinuousLinearEquiv.prodComm, Eq.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
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : X → E × F
hf : Integrable f μ
pos : ∀ (hE : CompleteSpace E), Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ).1 (∫ (x : X), (f x).1 ∂μ)
neg : ∀ (hE : ¬CompleteSpace E), Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ).1 (∫ (x : X), (f x).1 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ).1 (∫ (x : X), (f x).1 ∂μ)

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : X → E × F
hf : Integrable f μ
hE : CompleteSpace E
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ).1 (∫ (x : X), (f x).1 ∂μ)

Tactic:
((ContinuousLinearMap.fst ℝ E F).integral_comp_comm hf).symm

Premises used: Real, ContinuousLinearMap.fst, Eq.symm, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : X → E × F
hf : Integrable f μ
hE : CompleteSpace E
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ).1 (∫ (x : X), (f x).1 ∂μ)

Tactic:
exact ((ContinuousLinearMap.fst ℝ E F).integral_comp_comm hf).symm

Premises used: Real, ContinuousLinearMap.fst, Eq.symm, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : X → E × F
hf : Integrable f μ
hE : ¬CompleteSpace E
⊢ ¬CompleteSpace (E × F)

Tactic:
have : ¬(CompleteSpace (E × F)) := fun h ↦ hE <| .fst_of_prod (β := F)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : X → E × F
hf : Integrable f μ
hE : ¬CompleteSpace E
this : ¬CompleteSpace (E × F)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ).1 (∫ (x : X), (f x).1 ∂μ)

Tactic:
simp [integral, *]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace E
f : X → E × F
hf : Integrable f μ
rw : Eq.{u_4 + 1} (α := F) (∫ (x : X), (f x).swap ∂μ).1 (∫ (x : X), (f x).2 ∂μ)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), f x ∂μ).2 (∫ (x : X), (f x).2 ∂μ)

Tactic:
rw [← Prod.fst_swap, swap_integral]

Premises used: Prod.fst_swap, swap_integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace E
f : X → E × F
hf : Integrable f μ
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (f x).swap ∂μ).1 (∫ (x : X), (f x).2 ∂μ)

Tactic:
fst_integral <| hf.snd.prodMk hf.fst

Premises used: MeasureTheory.Integrable.fst, MeasureTheory.Integrable.snd, fst_integral, MeasureTheory.Integrable.prodMk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace E
f : X → E × F
hf : Integrable f μ
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (f x).swap ∂μ).1 (∫ (x : X), (f x).2 ∂μ)

Tactic:
exact fst_integral <| hf.snd.prodMk hf.fst

Premises used: MeasureTheory.Integrable.fst, MeasureTheory.Integrable.snd, fst_integral, MeasureTheory.Integrable.prodMk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
f : X → E
g : X → F
hf : Integrable f μ
hg : Integrable g μ
⊢ Eq (α := E × F) (∫ (x : X), (f x, g x) ∂μ) (∫ (x : X), f x ∂μ, ∫ (x : X), g x ∂μ)

Tactic:
have := hf.prodMk hg
  Prod.ext (fst_integral this) (snd_integral this)

Premises used: snd_integral, fst_integral, Prod.ext, MeasureTheory.Integrable.prodMk