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
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 : ℝ)
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 : ℝ)
⊢ 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‖ * HMul.hMul (β := ℝ) ‖B‖ ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) ≤
  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 : ℝ)
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 : ℝ)
h₃ :
  ‖φ x‖ * HMul.hMul (β := ℝ) ‖B‖ ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) ≤
    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₄ : ‖φ x‖ * HMul.hMul (β := ℝ) ‖B‖ ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) ≤
  ‖φ x‖ * HMul.hMul (β := ℝ) ‖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 (hypothesis)
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) μ
⊢ 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 h : ∀ᵐ (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 : ℝ)
Tactic: have h : ∀ᵐ x ∂(μ.restrict K), ‖B (f x) (φ x)‖ ≤ ‖φ x‖ * ‖B‖ * N[𝕜]_{K, n, 0} f := by
      filter_upwards [] with x
      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) μ
h :
  ∀ᵐ (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 : ℝ)
⊢ 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 : norm.{u_7} (E := 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) ∂μ) ≤
  HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
Tactic: rw [integralAgainstBilinLM_eq_setIntegral hφ]
-- 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) μ
h :
  ∀ᵐ (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 : ℝ)
⊢ norm.{u_7} (E := 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) ∂μ) ≤
    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 : ∫ (x : E) in (↑K : Set E),
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, 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: apply le_trans (norm_integral_le_of_norm_le ((hφ.norm.mul_const _).mul_const _) h)
-- 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) μ
h :
  ∀ᵐ (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 : ℝ)
⊢ ∫ (x : E) in (↑K : Set E),
      HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, 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 : HMul.hMul (α := ℝ) (β := ℝ) (∫ (a : E) in (↑K : Set E), ‖φ a‖ * ‖B‖ ∂μ : ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, 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: rw [integral_mul_const, integral_mul_const]
-- 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) μ
h :
  ∀ᵐ (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 : ℝ)
pos :
  HMul.hMul (α := ℝ) (β := ℝ) (∫ (a : E) in (↑K : Set E), ‖φ a‖ * ‖B‖ ∂μ : ℝ)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, 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 : ℝ)
⊢ ∫ (x : E) in (↑K : Set E),
      HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, 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₁ : HMul.hMul (β := ℝ) ((∫ (a : E) in (↑K : Set E), ‖φ a‖ ∂μ) * ‖B‖)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) ≤
  HMul.hMul (β := ℝ) ((∫ (a : E) in (↑K : Set E), ‖φ a‖ ∂μ) * ‖B‖)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
Tactic: rw [integral_mul_const, integral_mul_const]
-- 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) μ
⊢ 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 : 0 ≤
  HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
Tactic: simp only [integralAgainstBilinLM, hφ, ↓reduceIte, LinearMap.coe_mk, AddHom.coe_mk, norm_zero]
-- 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₂
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(integralAgainstBilinLM B μ φ) : (a : 𝓓^{n}_{K}(E, F₁)) → F₃)
have refine : ∀ (x : Fin 1) (f : 𝓓^{n}_{K}(E, F₁)),
  (normSeminorm 𝕜 F₃ : (a : F₃) → ℝ) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((Finset.sup {0} (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K) : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
Tactic: refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (norm_withSeminorms 𝕜 _) _
      (.of_real fun _ ↦ ⟨{0}, (∫ x in K, ‖φ x‖ ∂μ) * ‖B‖, fun f ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (hypothesis)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
⊢ ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
have hmzero : init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0 = m 0
Tactic: have hmzero : init m 0 = m 0 := by simp only [init_def, castSucc_zero]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (hypothesis)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0 = m 0
⊢ ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
have hmtail : tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n) = m (last n.succ)
Tactic: have hmtail : tail m (last n) = m (last n.succ) := by
      simp only [tail_def, succ_last]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0 = m 0
hmtail : tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n) = m (last n.succ)
⊢ ∂_{m 0} (∂^{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} f) =
    ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n)} f))
have e_a : ∂^{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} f =
  ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
    (∂_{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n)} f)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0 = m 0
hmtail : tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n) = m (last n.succ)
⊢ ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n)} f)) =
    ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
have rw : ∂_{m 0}
    (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last n.succ)} f)) =
  ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
Tactic: rw [hmtail, iteratedLineDerivOp_succ_left, hmzero, tail_init_eq_init_tail]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0 = m 0
hmtail : tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n) = m (last n.succ)
rw :
  ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{m (last n.succ)} f)) =
    ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
⊢ ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n)} f)) =
    ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
have rw₁ : ∂_{m 0}
    (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last n.succ)} f)) =
  ∂_{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0}
    (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) (init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last (n + 1))} f))
Tactic: rw [hmtail, iteratedLineDerivOp_succ_left, hmzero, tail_init_eq_init_tail]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0 = m 0
hmtail : tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n) = m (last n.succ)
rw :
  ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{m (last n.succ)} f)) =
    ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
rw₁ :
  ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{m (last n.succ)} f)) =
    ∂_{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0}
      (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) (init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last (n + 1))} f))
⊢ ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n)} f)) =
    ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
have rw₂ : ∂_{m 0}
    (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last n.succ)} f)) =
  ∂_{m 0}
    (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) (init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last (n + 1))} f))
Tactic: rw [hmtail, iteratedLineDerivOp_succ_left, hmzero, tail_init_eq_init_tail]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.DerivNotation (goal)
Goal:
V : Type u_11
E : Type u_12
inst : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init (α := fun (i : Fin (n + 1)) ↦ V) m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0 = m 0
hmtail : tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n) = m (last n.succ)
rw :
  ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{m (last n.succ)} f)) =
    ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
rw₁ :
  ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{m (last n.succ)} f)) =
    ∂_{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m 0}
      (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) (init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last (n + 1))} f))
rw₂ :
  ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{m (last n.succ)} f)) =
    ∂_{m 0}
      (∂^{tail (α := fun (i : Fin (n + 1)) ↦ V) (init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last (n + 1))} f))
⊢ ∂_{m 0}
      (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)}
        (∂_{tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m (last n)} f)) =
    ∂^{init (α := fun (i : Fin (n + 1 + 1)) ↦ V) m} (∂_{m (last (n + 1))} f)
have rw₃ : ∂_{m 0}
    (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last n.succ)} f)) =
  ∂_{m 0}
    (∂^{init (α := fun (i : Fin (n + 1)) ↦ V) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ V) m)} (∂_{m (last (n + 1))} f))
Tactic: rw [hmtail, iteratedLineDerivOp_succ_left, hmzero, tail_init_eq_init_tail]