awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n₁ n₂ : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n₁}(Ω₁, F)
pos :
  ∀ (h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂),
    (⇑(((TestFunction.limitCLM 𝕜
                    (fun (f : 𝓓^{n₁}(Ω₁, F)) ↦
                      { toFun := (⇑f : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ :
                        𝓓^{n₂}(Ω₂, F) })
                    (fun (K : Compacts E) (K_sub_Ω₁ : (↑K : Set E) ⊆ (↑Ω₁ : Set E)) ↦
                      ofSupportedInCLM 𝕜 ⋯ ∘SL ContDiffMapSupportedIn.monoCLM 𝕜)
                    ⋯ :
                  𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)) :
                (a : 𝓓^{n₁}(Ω₁, F)) → 𝓓^{n₂}(Ω₂, F))
              f :
            𝓓^{n₂}(Ω₂, F)) :
        (a : E) → F) =
      (⇑f : (a : E) → F)
⊢ (⇑(((TestFunction.limitCLM 𝕜
                  (fun (f : 𝓓^{n₁}(Ω₁, F)) ↦
                    if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then
                      { toFun := (⇑f : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ :
                        𝓓^{n₂}(Ω₂, F) }
                    else 0)
                  (fun (K : Compacts E) (K_sub_Ω₁ : (↑K : Set E) ⊆ (↑Ω₁ : Set E)) ↦
                    if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then ofSupportedInCLM 𝕜 ⋯ ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 else 0)
                  ⋯ :
                𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)) :
              (a : 𝓓^{n₁}(Ω₁, F)) → 𝓓^{n₂}(Ω₂, F))
            f :
          𝓓^{n₂}(Ω₂, F)) :
      (a : E) → F) =
    (⇑(if n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then f else 0) : (a : E) → F)
have neg : ∀ (h : ¬(n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂)),
  (⇑(((TestFunction.limitCLM 𝕜 (fun (f : 𝓓^{n₁}(Ω₁, F)) ↦ 0)
                  (fun (K : Compacts E) (K_sub_Ω₁ : (↑K : Set E) ⊆ (↑Ω₁ : Set E)) ↦ 0) sorry :
                𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)) :
              (a : 𝓓^{n₁}(Ω₁, F)) → 𝓓^{n₂}(Ω₂, F))
            f :
          𝓓^{n₂}(Ω₂, F)) :
      (a : E) → F) =
    (⇑0 : (a : E) → F)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n₁ n₂ : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
H : ¬(n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂)
⊢ Eq (α := 𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)) (monoCLM 𝕜 : 𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F))
    (0 : 𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F))
have h : ∀ (x : 𝓓^{n₁}(Ω₁, F)) (a : E),
  ((((monoCLM 𝕜 : 𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)) : (a : 𝓓^{n₁}(Ω₁, F)) → 𝓓^{n₂}(Ω₂, F)) x : 𝓓^{n₂}(Ω₂, F)) :
        (a : E) → F)
      a =
    (((0 : (a : 𝓓^{n₁}(Ω₁, F)) → 𝓓^{n₂}(Ω₂, F)) x : 𝓓^{n₂}(Ω₂, F)) : (a : E) → F) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
inst_9 : Algebra ℝ 𝕜
inst_10 : IsScalarTower ℝ 𝕜 F
Φ : (f : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F) :=
  fun (f : 𝓓^{n}(Ω, F)) ↦
    if hk : k + 1 ≤ n then
      { toFun := fderiv ℝ (⇑f : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
    else 0
x : Compacts E
h : (↑x : Set E) ⊆ (↑Ω : Set E)
x_1 : 𝓓^{n}_{x}(E, F)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
inst_9 : Algebra ℝ 𝕜
inst_10 : IsScalarTower ℝ 𝕜 F
Φ : (f : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F) :=
  fun (f : 𝓓^{n}(Ω, F)) ↦
    if hk : k + 1 ≤ n then
      { toFun := fderiv ℝ (⇑f : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
    else 0
x : Compacts E
h : (↑x : Set E) ⊆ (↑Ω : Set E)
x_1 : 𝓓^{n}_{x}(E, F)
a x_2 : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : Eq.{u_4 + 1} (α := F)
  (((if hk : k + 1 ≤ n then
              { toFun := fderiv ℝ (⇑x_1 : (a : E) → F), contDiff' := sorry, hasCompactSupport' := sorry, tsupport_subset' := sorry :
                𝓓^{k}(Ω, E →L[ℝ] F) }
            else 0 :
            (a : E) → E →L[ℝ] F)
          a :
        (a : E) → F)
      x_2 :
    F)
  (((((ContDiffMapSupportedIn.fderivCLM 𝕜 n k : (a : 𝓓^{n}_{x}(E, F)) → 𝓓^{k}_{x}(E, E →L[ℝ] F)) x_1 :
              𝓓^{k}_{x}(E, E →L[ℝ] F)) :
            (a : E) → E →L[ℝ] F)
          a :
        (a : E) → F)
      x_2 :
    F)
Tactic: dsimp [Φ]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
inst_9 : Algebra ℝ 𝕜
inst_10 : IsScalarTower ℝ 𝕜 F
Φ : (f : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F) :=
  fun (f : 𝓓^{n}(Ω, F)) ↦
    if hk : k + 1 ≤ n then
      { toFun := fderiv ℝ (⇑f : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
    else 0
x : Compacts E
h : (↑x : Set E) ⊆ (↑Ω : Set E)
x_1 : 𝓓^{n}_{x}(E, F)
a x_2 : E
⊢ Eq.{u_4 + 1} (α := F)
    (((if hk : k + 1 ≤ n then
                { toFun := fderiv ℝ (⇑x_1 : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯,
                  tsupport_subset' := ⋯ : 𝓓^{k}(Ω, E →L[ℝ] F) }
              else 0 :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x_2 :
      F)
    (((((ContDiffMapSupportedIn.fderivCLM 𝕜 n k : (a : 𝓓^{n}_{x}(E, F)) → 𝓓^{k}_{x}(E, E →L[ℝ] F)) x_1 :
                𝓓^{k}_{x}(E, E →L[ℝ] F)) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x_2 :
      F)
have pos : ∀ (h_1 : k + 1 ≤ n),
  Eq.{u_4 + 1} (α := F)
    ((({ toFun := fderiv ℝ (⇑x_1 : (a : E) → F), contDiff' := sorry, hasCompactSupport' := sorry, tsupport_subset' := sorry :
                𝓓^{k}(Ω, E →L[ℝ] F) } :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x_2 :
      F)
    (((((ContDiffMapSupportedIn.fderivCLM 𝕜 n k : (a : 𝓓^{n}_{x}(E, F)) → 𝓓^{k}_{x}(E, E →L[ℝ] F)) x_1 :
                𝓓^{k}_{x}(E, E →L[ℝ] F)) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x_2 :
      F)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
inst_9 : Algebra ℝ 𝕜
inst_10 : IsScalarTower ℝ 𝕜 F
Φ : (f : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F) :=
  fun (f : 𝓓^{n}(Ω, F)) ↦
    if hk : k + 1 ≤ n then
      { toFun := fderiv ℝ (⇑f : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
    else 0
x : Compacts E
h : (↑x : Set E) ⊆ (↑Ω : Set E)
x_1 : 𝓓^{n}_{x}(E, F)
a x_2 : E
pos :
  ∀ (h_1 : k + 1 ≤ n),
    Eq.{u_4 + 1} (α := F)
      ((({ toFun := fderiv ℝ (⇑x_1 : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ :
                  𝓓^{k}(Ω, E →L[ℝ] F) } :
                (a : E) → E →L[ℝ] F)
              a :
            (a : E) → F)
          x_2 :
        F)
      (((((ContDiffMapSupportedIn.fderivCLM 𝕜 n k : (a : 𝓓^{n}_{x}(E, F)) → 𝓓^{k}_{x}(E, E →L[ℝ] F)) x_1 :
                  𝓓^{k}_{x}(E, E →L[ℝ] F)) :
                (a : E) → E →L[ℝ] F)
              a :
            (a : E) → F)
          x_2 :
        F)
⊢ Eq.{u_4 + 1} (α := F)
    (((if hk : k + 1 ≤ n then
                { toFun := fderiv ℝ (⇑x_1 : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯,
                  tsupport_subset' := ⋯ : 𝓓^{k}(Ω, E →L[ℝ] F) }
              else 0 :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x_2 :
      F)
    (((((ContDiffMapSupportedIn.fderivCLM 𝕜 n k : (a : 𝓓^{n}_{x}(E, F)) → 𝓓^{k}_{x}(E, E →L[ℝ] F)) x_1 :
                𝓓^{k}_{x}(E, E →L[ℝ] F)) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x_2 :
      F)
have neg : ∀ (h : ¬k + 1 ≤ n),
  Eq.{u_4 + 1} (α := F) (((0 : (a : E) → E →L[ℝ] F) a : (a : E) → F) x_2 : F)
    (((((ContDiffMapSupportedIn.fderivCLM 𝕜 n k : (a : 𝓓^{n}_{x}(E, F)) → 𝓓^{k}_{x}(E, E →L[ℝ] F)) x_1 :
                𝓓^{k}_{x}(E, E →L[ℝ] F)) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x_2 :
      F)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
hk : n < k + 1
⊢ Eq (α := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F)) (fderivCLM 𝕜 n k : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F))
    (0 : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F))
have h : ∀ (x : 𝓓^{n}(Ω, F)) (a : E),
  ((((fderivCLM 𝕜 n k : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F)) x :
          𝓓^{k}(Ω, E →L[ℝ] F)) :
        (a : E) → E →L[ℝ] F)
      a =
    (((0 : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F)) x : 𝓓^{k}(Ω, E →L[ℝ] F)) : (a : E) → E →L[ℝ] F) a
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
K : Compacts E
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
f : 𝓓^{n}_{K}(E, F)
⊢ Eq (α := 𝓓^{k}(Ω, E →L[ℝ] F))
    (((fderivCLM 𝕜 n k : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F))
        (ofSupportedIn K_sub_Ω f) :
      𝓓^{k}(Ω, E →L[ℝ] F))
    (ofSupportedIn K_sub_Ω
        ((ContDiffMapSupportedIn.fderivCLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f) :
      𝓓^{k}(Ω, E →L[ℝ] F))
have h : ∀ (a x : E),
  Eq.{u_4 + 1} (α := F)
    ((((((fderivCLM 𝕜 n k : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F))
                  (ofSupportedIn K_sub_Ω f) :
                𝓓^{k}(Ω, E →L[ℝ] F)) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x :
      F)
    (((ofSupportedIn K_sub_Ω
                ((ContDiffMapSupportedIn.fderivCLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x :
      F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
⊢ ((((lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) f : 𝓓^{k}(Ω, F)) :
        (a : E) → F)
      x =
    if k + 1 ≤ n then lineDeriv ℝ (⇑f : (a : E) → F) x v else 0
have rw : (((if k + 1 ≤ n then fderiv ℝ (⇑f : (a : E) → F) else 0) x : E →L[ℝ] F) : (a : E) → F) v =
  if k + 1 ≤ n then lineDeriv ℝ (⇑f : (a : E) → F) x v else 0
Tactic: rw [lineDerivCLM_eq_fderivCLM, fderivCLM_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
⊢ (((if k + 1 ≤ n then fderiv ℝ (⇑f : (a : E) → F) else 0) x : E →L[ℝ] F) : (a : E) → F) v =
    if k + 1 ≤ n then lineDeriv ℝ (⇑f : (a : E) → F) x v else 0
have pos : ∀ (hk : k + 1 ≤ n), (fderiv ℝ (⇑f : (a : E) → F) x : (a : E) → F) v = lineDeriv ℝ (⇑f : (a : E) → F) x v
Tactic: split_ifs with hk
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
pos : ∀ (hk : k + 1 ≤ n), (fderiv ℝ (⇑f : (a : E) → F) x : (a : E) → F) v = lineDeriv ℝ (⇑f : (a : E) → F) x v
⊢ (((if k + 1 ≤ n then fderiv ℝ (⇑f : (a : E) → F) else 0) x : E →L[ℝ] F) : (a : E) → F) v =
    if k + 1 ≤ n then lineDeriv ℝ (⇑f : (a : E) → F) x v else 0
have neg : ∀ (hk : ¬k + 1 ≤ n), Eq.{u_4 + 1} (α := F) ((0 x : (a : E) → F) v : F) (0 : F)
Tactic: split_ifs with hk
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
⊢ (fderiv ℝ (⇑f : (a : E) → F) x : (a : E) → F) v = lineDeriv ℝ (⇑f : (a : E) → F) x v
have hk' : 0 < (↑n : ℕ∞ω)
Tactic: have hk' : 0 < (n : ℕ∞ω) := mod_cast (ENat.add_one_pos.trans_le hk)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
hk' : 0 < (↑n : ℕ∞ω)
⊢ (fderiv ℝ (⇑f : (a : E) → F) x : (a : E) → F) v = lineDeriv ℝ (⇑f : (a : E) → F) x v
have pos : Eq.{u_4 + 1} (α := F) ((fderiv ℝ (⇑f : (a : E) → F) x : (a : E) → F) v : F)
  ((fderiv ℝ (⇑f : (a : E) → F) x : (a : E) → F) v : F)
Tactic: rw [(f.contDiff.differentiable hk'.ne').differentiableAt.lineDeriv_eq_fderiv]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
v : E
hk : n < k + 1
⊢ Eq (α := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) (lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
    (0 : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
have h : ∀ (x : 𝓓^{n}(Ω, F)) (a : E),
  ((((lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) :
        (a : E) → F)
      a =
    (((0 : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) : (a : E) → F) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
v₁ v₂ : E
⊢ lineDerivCLM 𝕜 (v₁ + v₂) =
    HAdd.hAdd (α := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) (β := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
      (lineDerivCLM 𝕜 v₁ : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) (lineDerivCLM 𝕜 v₂ : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
have h : ∀ (x : 𝓓^{n}(Ω, F)) (a : E),
  ((((lineDerivCLM 𝕜 (v₁ + v₂) : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) :
        (a : E) → F)
      a =
    (((HAdd.hAdd (α := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) (β := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
                (lineDerivCLM 𝕜 v₁ : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
                (lineDerivCLM 𝕜 v₂ : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) :
              (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F))
            x :
          𝓓^{k}(Ω, F)) :
        (a : E) → F)
      a
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
c : ℝ
v : E
⊢ lineDerivCLM 𝕜 (c • v) =
    HSMul.hSMul (β := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) c (lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
have h : ∀ (x : 𝓓^{n}(Ω, F)) (a : E),
  ((((lineDerivCLM 𝕜 (c • v) : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) :
        (a : E) → F)
      a =
    (((HSMul.hSMul (β := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) c (lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) :
              (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F))
            x :
          𝓓^{k}(Ω, F)) :
        (a : E) → F)
      a
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F₁)
this :
  IntegrableOn.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (tsupport (⇑f : (a : E) → F₁)) μ
⊢ Integrable.{u_8, u_3} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) μ
have rwa : (support.{u_3, u_8} (M := F₃) fun (x : E) ↦
    (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
  tsupport (⇑f : (a : E) → F₁)
Tactic: rwa [integrableOn_iff_integrable_of_support_subset] at this
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F₁)
this :
  IntegrableOn.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (tsupport (⇑f : (a : E) → F₁)) μ
⊢ (support.{u_3, u_8} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
    tsupport (⇑f : (a : E) → F₁)
have refine : (support.{u_3, u_8} (M := F₃) fun (x : E) ↦
    (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
  support (⇑f : (a : E) → F₁)
Tactic: refine subset_trans ?_ (subset_tsupport f)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F₁)
⊢ Integrable.{u_8, u_3} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) μ
have suffices : IntegrableOn.{u_3, u_8} (ε := F₃)
  (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
  (tsupport (⇑f : (a : E) → F₁)) μ
Tactic: suffices IntegrableOn (fun x ↦ B (f x) (φ x)) (tsupport f) μ by
    rwa [integrableOn_iff_integrable_of_support_subset] at this
    refine subset_trans ?_ (subset_tsupport f)
    exact fun x hx hfx ↦ hx (by simp [hfx])
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F₁)
⊢ IntegrableOn.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (tsupport (⇑f : (a : E) → F₁)) μ
have hφ₁ : IntegrableOn φ (tsupport (⇑f : (a : E) → F₁)) μ
Tactic: replace hφ := hφ.integrableOn_compact_subset f.tsupport_subset f.hasCompactSupport
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}(Ω, F₁)
hφ : IntegrableOn φ (tsupport (⇑f : (a : E) → F₁)) μ
⊢ IntegrableOn.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (tsupport (⇑f : (a : E) → F₁)) μ
have rw : ∀ (hφ : MemLp φ 1 (μ.restrict (tsupport (⇑f : (a : E) → F₁)))),
  MemLp.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) 1
    (μ.restrict (tsupport (⇑f : (a : E) → F₁)))
Tactic: rw [IntegrableOn, ← memLp_one_iff_integrable] at hφ ⊢
Cleared hypotheses: hφ