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
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 φ μ
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)
have h_ind : ∀ (c : E) ⦃s : Set X⦄,
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      (fun (φ : X → E) ↦
          Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
        (s.indicator fun (x : X) ↦ c)
Tactic: apply φ_int.induction (P := fun φ => ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ))
-- 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
𝕜' : 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 φ μ
h_ind :
  ∀ (c : E) ⦃s : Set X⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        (fun (φ : X → E) ↦
            Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
              ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
          (s.indicator fun (x : X) ↦ c)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)
have h_add : ∀ ⦃f g : X → E⦄,
  Disjoint (Function.support f) (Function.support g) →
    Integrable f μ →
      Integrable g μ →
        (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 →
            (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 + g)
Tactic: apply φ_int.induction (P := fun φ => ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ))
-- 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
𝕜' : 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 φ μ
h_ind :
  ∀ (c : E) ⦃s : Set X⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        (fun (φ : X → E) ↦
            Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
              ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
          (s.indicator fun (x : X) ↦ c)
h_add :
  ∀ ⦃f g : X → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          (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 →
              (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 + g)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)
have h_closed : IsClosed (X := ↥(Lp E 1 μ))
  {f : ↥(Lp E 1 μ) |
    (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 : X →ₘ[μ] E) : X → E)}
Tactic: apply φ_int.induction (P := fun φ => ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ))
-- 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
𝕜' : 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 φ μ
h_ind :
  ∀ (c : E) ⦃s : Set X⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        (fun (φ : X → E) ↦
            Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
              ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
          (s.indicator fun (x : X) ↦ c)
h_add :
  ∀ ⦃f g : X → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          (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 →
              (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 + g)
h_closed :
  IsClosed (X := ↥(Lp E 1 μ))
    {f : ↥(Lp E 1 μ) |
      (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 : X →ₘ[μ] E) : X → E)}
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)
have h_ae : ∀ ⦃f g : X → E⦄,
  f =ᶠ[ae μ] 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: apply φ_int.induction (P := fun φ => ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ))
-- 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
𝕜' : 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 φ μ
e : E
s : Set X
s_meas : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) x) ∂μ : F)
    ((L : (a : E) → F) (∫ (x : X), s.indicator (fun (x : X) ↦ e) x ∂μ) : F)
have h_ind : Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) x) ∂μ)
  (∫ (x : X), s.indicator (fun (x : X) ↦ (L : (a : E) → F) e) x ∂μ)
Tactic: rw [integral_indicator_const e s_meas, ← @smul_one_smul E ℝ 𝕜 _ _ _ _ _ (μ.real s) e,
      map_smulₛₗ, hσ, map_one, smul_assoc, one_smul,
      ← integral_indicator_const (L e) s_meas]
-- 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
𝕜' : 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 φ μ
e : E
s : Set X
s_meas : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) x) ∂μ)
    (∫ (x : X), s.indicator (fun (x : X) ↦ (L : (a : E) → F) e) x ∂μ)
have h_ind : ∀ (a : X),
  Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
    (s.indicator (fun (x : X) ↦ (L : (a : E) → F) e) a : F)
Tactic: congr 1 with a
-- 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
𝕜' : 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 φ μ
e : E
s : Set X
s_meas : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : X
⊢ Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
    (s.indicator (fun (x : X) ↦ (L : (a : E) → F) e) a : F)
have h_ind : Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
  (s.indicator (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑L : (a : E) → F) fun (x : X) ↦ e) a : F)
Tactic: rw [← Function.comp_def L, Set.indicator_comp_of_zero L.map_zero, Function.comp_apply]
-- 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
𝕜' : 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 φ μ
e : E
s : Set X
s_meas : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : X
h_ind :
  Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
    (s.indicator (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑L : (a : E) → F) fun (x : X) ↦ e) a : F)
⊢ Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
    (s.indicator (fun (x : X) ↦ (L : (a : E) → F) e) a : F)
have h_ind₁ : Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
  (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑L : (a : E) → F) (s.indicator fun (x : X) ↦ e) a : F)
Tactic: rw [← Function.comp_def L, Set.indicator_comp_of_zero L.map_zero, Function.comp_apply]
-- 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
𝕜' : 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 φ μ
e : E
s : Set X
s_meas : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : X
h_ind :
  Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
    (s.indicator (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑L : (a : E) → F) fun (x : X) ↦ e) a : F)
h_ind₁ :
  Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
    (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑L : (a : E) → F) (s.indicator fun (x : X) ↦ e) a : F)
⊢ Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
    (s.indicator (fun (x : X) ↦ (L : (a : E) → F) e) a : F)
have h_ind₂ : Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
  ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
Tactic: rw [← Function.comp_def L, Set.indicator_comp_of_zero L.map_zero, Function.comp_apply]
-- 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
𝕜' : 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) (g x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), g x ∂μ) : F)
have h : Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (g x) ∂μ) (∫ (x : X), (L : (a : E) → F) (f x) ∂μ)
Tactic: convert! hf using 1
-- 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
𝕜' : 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) ∂μ)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (g x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), g x ∂μ) : F)
have h₁ : Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (∫ (x : X), g x ∂μ) : F) ((L : (a : E) → F) (∫ (x : X), f x ∂μ) : F)
Tactic: convert! hf using 1
-- 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
𝕜' : 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) ((L : (a : E) → F) (∫ (x : X), g x ∂μ) : F) ((L : (a : E) → F) (∫ (x : X), f x ∂μ) : F)
have h : Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (∫ (a : X), f a ∂μ) : F) ((L : (a : E) → F) (∫ (x : X), f x ∂μ) : F)
Tactic: rw [integral_congr_ae hfg.symm]
-- 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
H : Type u_8
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)
have 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)
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
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)
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)
have 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)
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
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)
have 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)
Tactic: rcases subsingleton_or_nontrivial H with hH | hH
-- 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
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)
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)
have 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)
Tactic: rcases subsingleton_or_nontrivial H with hH | hH
-- 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
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
⊢ Eq.{u_3 + 1} (α := E) ((∫ (x : X), φ x ∂μ : (a : H) → E) v : E) (∫ (x : X), (φ x : (a : H) → E) v ∂μ : E)
have this : ¬CompleteSpace (H →L[𝕜] E)
Tactic: have : ¬(CompleteSpace (H →L[𝕜] E)) := by
        rwa [SeparatingDual.completeSpace_continuousLinearMap_iff]
-- 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
⊢ 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 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)
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
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)
⊢ 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 : ∀ (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: 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
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)
have 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)
Tactic: by_cases! hm : ∀ i, m i ≠ 0