awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst_11 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_12 : NormedAddCommGroup F₁
inst_13 : NormedSpace 𝕜 F₁
inst_14 : NormedSpace ℝ F₁
inst_15 : NormedAddCommGroup F₂
inst_16 : NormedSpace 𝕜 F₂
inst_17 : NormedAddCommGroup F₃
inst_18 : NormedSpace 𝕜 F₃
inst_19 : SMulCommClass ℝ 𝕜 F₁
inst_20 : NormedSpace ℝ F₃
inst_21 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
c : 𝕜
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
pos :
  ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((c • (⇑f : (a : E) → F₁)) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₁ :
  ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) (c • (f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
⊢ ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((c • f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
have pos₂ : ∫ (x : E),
    (HSMul.hSMul (β := F₂ →L[𝕜] F₃) c ((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) :
        (a : F₂) → F₃)
      (φ x) ∂μ =
  HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
    (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
Tactic: simp_rw [coe_smul, Pi.smul_apply, map_smul, ContinuousLinearMap.smul_apply,
        integral_smul c, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst_11 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_12 : NormedAddCommGroup F₁
inst_13 : NormedSpace 𝕜 F₁
inst_14 : NormedSpace ℝ F₁
inst_15 : NormedAddCommGroup F₂
inst_16 : NormedSpace 𝕜 F₂
inst_17 : NormedAddCommGroup F₃
inst_18 : NormedSpace 𝕜 F₃
inst_19 : SMulCommClass ℝ 𝕜 F₁
inst_20 : NormedSpace ℝ F₃
inst_21 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
c : 𝕜
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
pos :
  ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((c • (⇑f : (a : E) → F₁)) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₁ :
  ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) (c • (f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₂ :
  ∫ (x : E),
      (HSMul.hSMul (β := F₂ →L[𝕜] F₃) c ((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) :
          (a : F₂) → F₃)
        (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
⊢ ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((c • f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
have pos₃ : ∫ (x : E),
    HSMul.hSMul (β := F₃) c
      ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ∂μ =
  HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
    (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
Tactic: simp_rw [coe_smul, Pi.smul_apply, map_smul, ContinuousLinearMap.smul_apply,
        integral_smul c, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst_11 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_12 : NormedAddCommGroup F₁
inst_13 : NormedSpace 𝕜 F₁
inst_14 : NormedSpace ℝ F₁
inst_15 : NormedAddCommGroup F₂
inst_16 : NormedSpace 𝕜 F₂
inst_17 : NormedAddCommGroup F₃
inst_18 : NormedSpace 𝕜 F₃
inst_19 : SMulCommClass ℝ 𝕜 F₁
inst_20 : NormedSpace ℝ F₃
inst_21 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
c : 𝕜
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
pos :
  ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((c • (⇑f : (a : E) → F₁)) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₁ :
  ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) (c • (f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₂ :
  ∫ (x : E),
      (HSMul.hSMul (β := F₂ →L[𝕜] F₃) c ((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) :
          (a : F₂) → F₃)
        (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
pos₃ :
  ∫ (x : E),
      HSMul.hSMul (β := F₃) c
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
⊢ ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((c • f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
have pos₄ : HSMul.hSMul (β := F₃) c
    (∫ (a : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) a) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ a) ∂μ) =
  HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
    (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
Tactic: simp_rw [coe_smul, Pi.smul_apply, map_smul, ContinuousLinearMap.smul_apply,
        integral_smul c, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
⊢ Eq.{u_7 + 1} (α := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃)
    (∫ (x : E) in (↑K : Set E),
        (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ :
      F₃)
have rw : ∀ x ∉ (↑K : Set E),
  Eq.{u_7 + 1} (α := F₃)
    ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
Tactic: rw [integralAgainstBilinLM_eq_integral hφ, setIntegral_eq_integral_of_forall_compl_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
x : E
hx : x ∉ (↑K : Set E)
⊢ Eq.{u_7 + 1} (α := F₃)
    ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
have rw : Eq.{u_7 + 1} (α := F₃) (((B : (a : F₁) → F₂ →L[𝕜] F₃) (0 x) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
Tactic: rw [f.zero_on_compl hx, Pi.zero_apply, map_zero, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
x : E
hx : x ∉ (↑K : Set E)
rw : Eq.{u_7 + 1} (α := F₃) (((B : (a : F₁) → F₂ →L[𝕜] F₃) (0 x) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
⊢ Eq.{u_7 + 1} (α := F₃)
    ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
have rw₁ : Eq.{u_7 + 1} (α := F₃) (((B : (a : F₁) → F₂ →L[𝕜] F₃) 0 : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
Tactic: rw [f.zero_on_compl hx, Pi.zero_apply, map_zero, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
x : E
hx : x ∉ (↑K : Set E)
rw : Eq.{u_7 + 1} (α := F₃) (((B : (a : F₁) → F₂ →L[𝕜] F₃) (0 x) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
rw₁ : Eq.{u_7 + 1} (α := F₃) (((B : (a : F₁) → F₂ →L[𝕜] F₃) 0 : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
⊢ Eq.{u_7 + 1} (α := F₃)
    ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
have rw₂ : Eq.{u_7 + 1} (α := F₃) ((0 : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
Tactic: rw [f.zero_on_compl hx, Pi.zero_apply, map_zero, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
x : E
hx : x ∉ (↑K : Set E)
rw : Eq.{u_7 + 1} (α := F₃) (((B : (a : F₁) → F₂ →L[𝕜] F₃) (0 x) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
rw₁ : Eq.{u_7 + 1} (α := F₃) (((B : (a : F₁) → F₂ →L[𝕜] F₃) 0 : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
rw₂ : Eq.{u_7 + 1} (α := F₃) ((0 : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
⊢ Eq.{u_7 + 1} (α := F₃)
    ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
have rw₃ : Eq.{u_7 + 1} (α := F₃) 0 0
Tactic: rw [f.zero_on_compl hx, Pi.zero_apply, map_zero, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
⊢ norm.{u_7} (E := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
have pos : ∀ (hφ : IntegrableOn φ (↑K : Set E) μ),
  norm.{u_7} (E := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
Tactic: by_cases hφ : IntegrableOn φ K μ
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
pos :
  ∀ (hφ : IntegrableOn φ (↑K : Set E) μ),
    norm.{u_7} (E := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
      HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
⊢ norm.{u_7} (E := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
have neg : ∀ (hφ : ¬IntegrableOn φ (↑K : Set E) μ),
  norm.{u_7} (E := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
Tactic: by_cases hφ : IntegrableOn φ K μ
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
⊢ ∀ᵐ (x : E) ∂μ.restrict (↑K : Set E),
    norm.{u_7} (E := F₃)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
      HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
have h : ∀ (x : E),
  norm.{u_7} (E := F₃)
      ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
Tactic: filter_upwards [] with x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
x : E
⊢ norm.{u_7} (E := F₃)
      ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
have h : norm (E := F₂ →L[𝕜] F₃) ((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) * ‖φ x‖ ≤
  HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
Tactic: grw [ContinuousLinearMap.le_opNorm, ContinuousLinearMap.le_opNorm, norm_apply_le_seminorm 𝕜,
        mul_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
x : E
h :
  norm (E := F₂ →L[𝕜] F₃) ((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) * ‖φ x‖ ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
⊢ norm.{u_7} (E := F₃)
      ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
have h₁ : ‖B‖ * ‖(f : (a : E) → F₁) x‖ * ‖φ x‖ ≤
  HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
Tactic: grw [ContinuousLinearMap.le_opNorm, ContinuousLinearMap.le_opNorm, norm_apply_le_seminorm 𝕜,
        mul_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
x : E
h :
  norm (E := F₂ →L[𝕜] F₃) ((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) * ‖φ x‖ ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
h₁ :
  ‖B‖ * ‖(f : (a : E) → F₁) x‖ * ‖φ x‖ ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
⊢ norm.{u_7} (E := F₃)
      ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
have h₂ : HMul.hMul (β := ℝ) ‖B‖ ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) * ‖φ x‖ ≤
  HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
Tactic: grw [ContinuousLinearMap.le_opNorm, ContinuousLinearMap.le_opNorm, norm_apply_le_seminorm 𝕜,
        mul_comm, mul_assoc]