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 : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
⊢ (ContDiffMapSupportedIn.seminorm ℝ E F' n K i : (a : 𝓓^{n}_{K}(E, F')) → ℝ)
      ((postcompLM T' : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F')) f : 𝓓^{n}_{K}(E, F')) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
have rw : (↑i : ℕ∞) ≤ n →
  ∀ x ∈ K,
    norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
        (iteratedFDeriv ℝ i
          (⇑((postcompLM T' : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F')) f : 𝓓^{n}_{K}(E, F')) : (a : E) → F') x) ≤
      HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
Tactic: rw [ContDiffMapSupportedIn.seminorm_le_iff ℝ (by positivity)]
-- 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 : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
hi : (↑i : ℕ∞) ≤ n
x : E
hx : x ∈ K
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (iteratedFDeriv ℝ i
        (⇑((postcompLM T' : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F')) f : 𝓓^{n}_{K}(E, F')) : (a : E) → F') x) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
have rw : norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
    (iteratedFDeriv ℝ i ((⇑T' : (a : F) → F') ∘ (⇑f : (a : E) → F)) x) ≤
  HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
Tactic: rw [postcompLM_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 : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
hi : (↑i : ℕ∞) ≤ n
x : E
hx : x ∈ K
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (iteratedFDeriv ℝ i ((⇑T' : (a : F) → F') ∘ (⇑f : (a : E) → F)) x) =
    norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (T'.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x))
have rw : norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
    (T'.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x)) =
  norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
    (T'.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x))
Tactic: rw [T'.iteratedFDeriv_comp_left f.contDiff.contDiffAt (mod_cast hi)]
-- 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 : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
hi : (↑i : ℕ∞) ≤ n
x : E
hx : x ∈ K
⊢ ‖T'‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
have h₁ : 0 ≤ ‖T'‖
Tactic: grw [norm_iteratedFDeriv_apply_le_seminorm ℝ hi]
-- 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 : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
hi : (↑i : ℕ∞) ≤ n
x : E
hx : x ∈ K
h₁ : 0 ≤ ‖T'‖
⊢ ‖T'‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
have grw : HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ) ≤
  HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
Tactic: grw [norm_iteratedFDeriv_apply_le_seminorm ℝ hi]
-- 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 : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
hi : (↑i : ℕ∞) ≤ n
x : E
hx : x ∈ K
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (iteratedFDeriv ℝ i ((⇑T' : (a : F) → F') ∘ (⇑f : (a : E) → F)) x) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
have ℝ : norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
    (iteratedFDeriv ℝ i ((⇑T' : (a : F) → F') ∘ (⇑f : (a : E) → F)) x) =
  norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
    (T'.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x))
Tactic: calc
      ‖iteratedFDeriv ℝ i (T' ∘ f) x‖
  _ = ‖T'.compContinuousMultilinearMap (iteratedFDeriv ℝ i f x)‖ := by
        rw [T'.iteratedFDeriv_comp_left f.contDiff.contDiffAt (mod_cast hi)]
  _ ≤ ‖T'‖ * ‖iteratedFDeriv ℝ i f x‖ := T'.norm_compContinuousMultilinearMap_le _
  _ ≤ ‖T'‖ * N[ℝ]_{K, n, i} f := by grw [norm_iteratedFDeriv_apply_le_seminorm ℝ hi]
-- 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 : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
hi : (↑i : ℕ∞) ≤ n
x : E
hx : x ∈ K
ℝ :
  norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (iteratedFDeriv ℝ i ((⇑T' : (a : F) → F') ∘ (⇑f : (a : E) → F)) x) =
    norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (T'.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x))
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (iteratedFDeriv ℝ i ((⇑T' : (a : F) → F') ∘ (⇑f : (a : E) → F)) x) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
have ℝ₁ : ‖T'‖ *
    norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
  HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
Tactic: calc
      ‖iteratedFDeriv ℝ i (T' ∘ f) x‖
  _ = ‖T'.compContinuousMultilinearMap (iteratedFDeriv ℝ i f x)‖ := by
        rw [T'.iteratedFDeriv_comp_left f.contDiff.contDiffAt (mod_cast hi)]
  _ ≤ ‖T'‖ * ‖iteratedFDeriv ℝ i f x‖ := T'.norm_compContinuousMultilinearMap_le _
  _ ≤ ‖T'‖ * N[ℝ]_{K, n, i} f := by grw [norm_iteratedFDeriv_apply_le_seminorm ℝ hi]
-- 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
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
⊢ Continuous (X := 𝓓^{n}_{K}(E, F)) (Y := 𝓓^{n}_{K}(E, F')) (⇑(postcompLM T) : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F'))
have refine : ∀ (i : ℕ) (f : 𝓓^{n}_{K}(E, F)),
  (ContDiffMapSupportedIn.seminorm 𝕜 E F' n K i : (a : 𝓓^{n}_{K}(E, F')) → ℝ)
      ((postcompLM T : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F')) f : 𝓓^{n}_{K}(E, F')) ≤
    HMul.hMul (β := ℝ) ‖T‖
      ((Finset.sup {i} (ContDiffMapSupportedIn.seminorm 𝕜 E F n K) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
Tactic: refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (ContDiffMapSupportedIn.withSeminorms ..) _ (.of_real fun i ↦ ⟨{i}, ‖T‖, fun f ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
⊢ LE.le (α := ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
        ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)
have pos : ∀ (H : n₂ ≤ n₁ ∧ K₁ ≤ K₂),
  LE.le (α := ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
        ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)
Tactic: by_cases H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
pos :
  ∀ (H : n₂ ≤ n₁ ∧ K₁ ≤ K₂),
    LE.le (α := ℝ)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
          ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
        ℝ)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)
⊢ LE.le (α := ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
        ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)
have neg : ∀ (H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)),
  LE.le (α := ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
        ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)
Tactic: by_cases H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
⊢ LE.le (α := ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
        ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)
have pos : (↑i : ℕ∞) ≤ n₂ →
  ∀ x ∈ K₂,
    norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
      (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f
Tactic: simp (discharger := positivity) only [ContDiffMapSupportedIn.seminorm_le_iff, monoLM_apply, H,
      and_self, ↓reduceIte]
-- 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
⊢ Continuous (X := 𝓓^{n₁}_{K₁}(E, F)) (Y := 𝓓^{n₂}_{K₂}(E, F))
    (⇑(monoLM 𝕜) : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F))
have refine : ∀ (i : ℕ) (f : 𝓓^{n₁}_{K₁}(E, F)),
  LE.le (α := (fun (a : 𝓓^{n₁}_{K₁}(E, F)) ↦ ℝ) f)
    ((fun (f : Seminorm 𝕜 𝓓^{n₁}_{K₁}(E, F)) ↦ ((⇑f : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ))
      (Seminorm.comp (𝕜₂ := 𝕜) (E₂ := 𝓓^{n₂}_{K₂}(E, F)) (σ₁₂ := RingHom.id 𝕜)
        (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) (monoLM 𝕜))
      f)
    ((fun (f : Seminorm 𝕜 𝓓^{n₁}_{K₁}(E, F)) ↦ ((⇑f : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ))
      (HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 𝓓^{n₁}_{K₁}(E, F)) 1
        (Finset.sup {i} (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁)))
      f)
Tactic: refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms _ _ _ _ _)
      (ContDiffMapSupportedIn.withSeminorms _ _ _ _ _) _ (fun i ↦ ⟨{i}, 1, fun f ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
⊢ Eq (α := 𝓓^{n₁}_{K₁}(E, F) →L[𝕜] 𝓓^{n₂}_{K₂}(E, F)) (monoCLM 𝕜) 0
have h : ∀ (x : 𝓓^{n₁}_{K₁}(E, F)) (a : E),
  (((monoCLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) x : 𝓓^{n₂}_{K₂}(E, F)) : (a : E) → F) a =
    (((0 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) x : 𝓓^{n₂}_{K₂}(E, F)) : (a : E) → F) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
⊢ LE.le (α := ℝ)
    (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i : Seminorm 𝕜 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
          (a : 𝓓^{k}_{K}(E, E →L[ℝ] F)) → ℝ)
        ((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
have pos : ∀ (hk : k + 1 ≤ n),
  LE.le (α := ℝ)
    (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i : Seminorm 𝕜 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
          (a : 𝓓^{k}_{K}(E, E →L[ℝ] F)) → ℝ)
        ((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
Tactic: by_cases! hk : k + 1 ≤ n
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
pos :
  ∀ (hk : k + 1 ≤ n),
    LE.le (α := ℝ)
      (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i : Seminorm 𝕜 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
            (a : 𝓓^{k}_{K}(E, E →L[ℝ] F)) → ℝ)
          ((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
        ℝ)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
⊢ LE.le (α := ℝ)
    (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i : Seminorm 𝕜 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
          (a : 𝓓^{k}_{K}(E, E →L[ℝ] F)) → ℝ)
        ((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
have neg : ∀ (hk : n < k + 1),
  LE.le (α := ℝ)
    (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i : Seminorm 𝕜 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
          (a : 𝓓^{k}_{K}(E, E →L[ℝ] F)) → ℝ)
        ((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
Tactic: by_cases! hk : k + 1 ≤ n
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ LE.le (α := ℝ)
    (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i : Seminorm 𝕜 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
          (a : 𝓓^{k}_{K}(E, E →L[ℝ] F)) → ℝ)
        ((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
have pos : (↑i : ℕ∞) ≤ k →
  ∀ x ∈ K,
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) (E →L[ℝ] F))
        (iteratedFDeriv ℝ i
          (⇑((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
            (a : E) → E →L[ℝ] F)
          x) ≤
      (ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f
Tactic: rw [ContDiffMapSupportedIn.seminorm_le_iff 𝕜 (apply_nonneg ..)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
hi : (↑i : ℕ∞) ≤ k
x : E
hx : x ∈ K
⊢ norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) (E →L[ℝ] F))
      (iteratedFDeriv ℝ i
        (⇑((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
          (a : E) → E →L[ℝ] F)
        x) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f
have hi' : HAdd.hAdd (α := ℕ∞) (↑i : ℕ∞) 1 ≤ n
Tactic: have hi' : i + 1 ≤ n := (add_le_add_left hi 1).trans hk
-- 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
⊢ Continuous (X := 𝓓^{n}_{K}(E, F)) (Y := 𝓓^{k}_{K}(E, E →L[ℝ] F))
    (⇑(fderivLM 𝕜 n k) : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F))
have refine : ∀ (i : ℕ) (f : 𝓓^{n}_{K}(E, F)),
  LE.le (α := (fun (a : 𝓓^{n}_{K}(E, F)) ↦ ℝ) f)
    ((fun (f : Seminorm 𝕜 𝓓^{n}_{K}(E, F)) ↦ ((⇑f : (a : 𝓓^{n}_{K}(E, F)) → ℝ) : (a : 𝓓^{n}_{K}(E, F)) → ℝ))
      (Seminorm.comp (𝕜₂ := 𝕜) (E₂ := 𝓓^{k}_{K}(E, E →L[ℝ] F)) (σ₁₂ := RingHom.id 𝕜)
        (ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i) (fderivLM 𝕜 n k))
      f)
    ((fun (f : Seminorm 𝕜 𝓓^{n}_{K}(E, F)) ↦ ((⇑f : (a : 𝓓^{n}_{K}(E, F)) → ℝ) : (a : 𝓓^{n}_{K}(E, F)) → ℝ))
      (HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 𝓓^{n}_{K}(E, F)) 1
        (Finset.sup {i + 1} (ContDiffMapSupportedIn.seminorm 𝕜 E F n K)))
      f)
Tactic: refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (ContDiffMapSupportedIn.withSeminorms ..) _ (fun i ↦ ⟨{i+1}, 1, fun f ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
μ_finite : IsFiniteMeasure (μ.restrict (↑K : Set E))
f : 𝓓^{n}_{K}(E, F)
⊢ Integrable (⇑f : (a : E) → F) μ
have rw : IntegrableOn (⇑f : (a : E) → F) (↑K : Set E) μ
Tactic: rw [← integrableOn_iff_integrable_of_support_subset f.support_subset]