awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases! hm : ∀ i, m i ≠ 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (hypothesis)
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
⊢ 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)
have this : ¬CompleteSpace (ContinuousMultilinearMap 𝕜 M E)
Tactic: have : ¬ CompleteSpace (ContinuousMultilinearMap 𝕜 M E) := by
        rwa [SeparatingDual.completeSpace_continuousMultilinearMap_iff _ _ hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ 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)
have 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)
Tactic: rcases hm with ⟨i, hi⟩
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ Eq.{u_5 + 1} (α := Fₗ) (∫ (x : X), (L : (a : E) → Fₗ) (φ x) ∂μ : Fₗ) ((L : (a : E) → Fₗ) (∫ (x : X), φ x ∂μ) : Fₗ)
have pos : ∀ (h : Integrable φ μ),
  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 φ μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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ₗ)
⊢ Eq.{u_5 + 1} (α := Fₗ) (∫ (x : X), (L : (a : E) → Fₗ) (φ x) ∂μ : Fₗ) ((L : (a : E) → Fₗ) (∫ (x : X), φ x ∂μ) : Fₗ)
have neg : ∀ (h : ¬Integrable φ μ),
  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 φ μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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)) μ
have rwa : ¬Integrable.{u_5, u_1} (ε := Fₗ) ((⇑L : (a : E) → Fₗ) ∘ φ) μ
Tactic: rwa [← Function.comp_def,
      LipschitzWith.integrable_comp_iff_of_antilipschitz L.lipschitz hL L.map_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (hypothesis)
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ₗ)
have this : ¬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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (hypothesis)
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
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)
have this : CompleteSpace E ↔ CompleteSpace F
Tactic: have : CompleteSpace E ↔ CompleteSpace F :=
    completeSpace_congr (e := L.toEquiv) L.isUniformEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)
have 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)
Tactic: obtain ⟨_, _⟩ | ⟨_, _⟩ := iff_iff_and_or_not_and_not.mp this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)
have 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)
Tactic: obtain ⟨_, _⟩ | ⟨_, _⟩ := iff_iff_and_or_not_and_not.mp this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ ∫ (x : X), (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) ∂μ +
      HMul.hMul (α := 𝕜) (∫ (x : X), (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) ∂μ) I =
    ∫ (x : X), f x ∂μ
have rw : Eq.{u_6 + 1} (α := 𝕜)
  (∫ (a : X), (↑((re : (a : 𝕜) → ℝ) (f a)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜) ∂μ)
  (∫ (x : X), f x ∂μ)
Tactic: rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ ∫ (x : X), (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) ∂μ +
      HMul.hMul (α := 𝕜) (∫ (x : X), (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) ∂μ) I =
    ∫ (x : X), f x ∂μ
have hf₁ : Integrable.{u_6, u_1} (ε := 𝕜) (fun (x : X) ↦ (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜)) μ
Tactic: rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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)) : 𝕜)) μ
⊢ ∫ (x : X), (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) ∂μ +
      HMul.hMul (α := 𝕜) (∫ (x : X), (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) ∂μ) I =
    ∫ (x : X), f x ∂μ
have hg : Integrable.{u_6, u_1} (ε := 𝕜) (fun (a : X) ↦ HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜)) μ
Tactic: rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Eq.{u_6 + 1} (α := 𝕜)
    (∫ (a : X),
      (↑((re : (a : 𝕜) → ℝ) (f a)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜) ∂μ)
    (∫ (x : X), f x ∂μ)
have e_f : Eq (α := X → 𝕜)
  (fun (a : X) ↦ (↑((re : (a : 𝕜) → ℝ) (f a)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜))
  fun (x : X) ↦ f x
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Eq (α := X → 𝕜)
    (fun (a : X) ↦
      (↑((re : (a : 𝕜) → ℝ) (f a)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f a)) : 𝕜))
    fun (x : X) ↦ f x
have e_f : ∀ (x : X), (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) = f x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
x : X
⊢ (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) = f x
have e_f : (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) + HMul.hMul (α := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) = f x
Tactic: rw [smul_eq_mul, mul_comm, RCLike.re_add_im]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) = f x
have e_f₁ : (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) I = f x
Tactic: rw [smul_eq_mul, mul_comm, RCLike.re_add_im]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ (↑((re : (a : 𝕜) → ℝ) (f x)) : 𝕜) + HSMul.hSMul (α := 𝕜) (β := 𝕜) I (↑((im : (a : 𝕜) → ℝ) (f x)) : 𝕜) = f x
have e_f₂ : f x = f x
Tactic: rw [smul_eq_mul, mul_comm, RCLike.re_add_im]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst_1 : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ (↑(∫ (x : X), (re : (a : 𝕜) → ℝ) (f x) ∂μ) : 𝕜) +
      HMul.hMul (α := 𝕜) (↑(∫ (x : X), (im : (a : 𝕜) → ℝ) (f x) ∂μ) : 𝕜) I =
    ∫ (x : X), f x ∂μ
have rw : ∫ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ
⊢ (↑(∫ (x : X), (re : (a : 𝕜) → ℝ) (f x) ∂μ) : 𝕜) +
      HMul.hMul (α := 𝕜) (↑(∫ (x : X), (im : (a : 𝕜) → ℝ) (f x) ∂μ) : 𝕜) I =
    ∫ (x : X), f x ∂μ
have rw₁ : ∫ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ
⊢ (↑(∫ (x : X), (re : (a : 𝕜) → ℝ) (f x) ∂μ) : 𝕜) +
      HMul.hMul (α := 𝕜) (↑(∫ (x : X), (im : (a : 𝕜) → ℝ) (f x) ∂μ) : 𝕜) I =
    ∫ (x : X), f x ∂μ
have rw₂ : Eq.{u_6 + 1} (α := 𝕜) (∫ (x : X), f x ∂μ) (∫ (x : X), f x ∂μ)
Tactic: rw [← integral_ofReal, ← integral_ofReal, integral_coe_re_add_coe_im hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ).1 (∫ (x : X), (f x).1 ∂μ)
have pos : ∀ (hE : CompleteSpace E), Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ).1 (∫ (x : X), (f x).1 ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ).1 (∫ (x : X), (f x).1 ∂μ)
have neg : ∀ (hE : ¬CompleteSpace E), Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ).1 (∫ (x : X), (f x).1 ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (hypothesis)
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 ∂μ)
have this : ¬CompleteSpace (E × F)
Tactic: have : ¬(CompleteSpace (E × F)) := fun h ↦ hE <| .fst_of_prod (β := F)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ).2 (∫ (x : X), (f x).2 ∂μ)
have rw : Eq.{u_4 + 1} (α := F) (∫ (x : X), (f x).swap ∂μ).1 (∫ (x : X), (f x).2 ∂μ)
Tactic: rw [← Prod.fst_swap, swap_integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
⊢ ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
have pos : ∀ (hf : Integrable f μ), ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
pos : ∀ (hf : Integrable f μ), ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
⊢ ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
have neg : ∀ (hf : ¬Integrable f μ), ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
⊢ ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
have pos : ∀ (hc : c = 0), ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
pos : ∀ (hc : c = 0), ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
⊢ ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
have neg : ∀ (hc : ¬c = 0), ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
⊢ ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
have neg : ¬Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • c) μ
Tactic: rw [integral_undef hf, integral_undef, zero_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
⊢ ¬Integrable f μ
have neg : ¬False
Tactic: simp_rw [hf, not_false_eq_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ
have pos : ∀ (hA : CompleteSpace A), ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ
Tactic: by_cases hA : CompleteSpace A
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
pos : ∀ (hA : CompleteSpace A), ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ
⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ
have neg : ∀ (hA : ¬CompleteSpace A), ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ
Tactic: by_cases hA : CompleteSpace A
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
hA : CompleteSpace A
⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ
have pos : Eq (α := A)
  (∫ (x : X), (((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (f x) ∂μ : A)
  ((((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (∫ (x : X), f x ∂μ) : A)
Tactic: change ∫ x, ContinuousLinearMap.mul ℝ _ c (f x) ∂μ = ContinuousLinearMap.mul ℝ _ c (∫ x, f x ∂μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
hA : CompleteSpace A
⊢ Eq (α := A)
    (∫ (x : X), (((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (f x) ∂μ : A)
    ((((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (∫ (x : X), f x ∂μ) : A)
have pos : Eq (α := A)
  ((((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (∫ (x : X), f x ∂μ) : A)
  ((((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (∫ (x : X), f x ∂μ) : A)
Tactic: rw [ContinuousLinearMap.integral_comp_comm _ hf]