awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)) → 𝓓^{n₂}(Ω₂, F) :=
  fun (f : 𝓓^{n₁}(Ω₁, F)) ↦
    if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then
      { toFun := (⇑f : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
    else 0
x : Compacts E
h_1 : (↑x : Set E) ⊆ (↑Ω₁ : Set E)
x_1 : 𝓓^{n₁}_{x}(E, F)
a : E
h :
  (if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then
          { toFun := (⇑x_1 : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ :
            𝓓^{n₂}(Ω₂, F) }
        else 0 :
        (a : E) → F)
      a =
    (((if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then ofSupportedInCLM 𝕜 ⋯ ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 else 0 :
              (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F))
            x_1 :
          𝓓^{n₂}(Ω₂, F)) :
        (a : E) → F)
      a
⊢ (Φ (ofSupportedIn h_1 x_1) : (a : E) → F) a =
    ((((fun (K : Compacts E) (K_sub_Ω₁ : (↑K : Set E) ⊆ (↑Ω₁ : Set E)) ↦
                  (if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then ofSupportedInCLM 𝕜 ⋯ ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 else 0 :
                    𝓓^{n₁}_{K}(E, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)))
                x h_1 :
              (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F))
            x_1 :
          𝓓^{n₂}(Ω₂, F)) :
        (a : E) → F)
      a

Tactic:
dsimp [Φ]
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)) → 𝓓^{n₂}(Ω₂, F) :=
  fun (f : 𝓓^{n₁}(Ω₁, F)) ↦
    if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then
      { toFun := (⇑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 : E
pos :
  ∀ (h_1 : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂),
    ({ toFun := (⇑x_1 : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ : 𝓓^{n₂}(Ω₂, F) } :
          (a : E) → F)
        a =
      (((ofSupportedInCLM 𝕜 ⋯ ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 : (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F)) x_1 :
            𝓓^{n₂}(Ω₂, F)) :
          (a : E) → F)
        a
neg :
  ∀ (h : ¬(n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂)),
    (0 : (a : E) → F) a = (((0 : (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F)) x_1 : 𝓓^{n₂}(Ω₂, F)) : (a : E) → F) a
⊢ (if h_1 : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then
          { toFun := (⇑x_1 : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ :
            𝓓^{n₂}(Ω₂, F) }
        else 0 :
        (a : E) → F)
      a =
    (((if h_1 : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then ofSupportedInCLM 𝕜 ⋯ ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 else 0 :
              (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F))
            x_1 :
          𝓓^{n₂}(Ω₂, F)) :
        (a : E) → F)
      a

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)) → 𝓓^{n₂}(Ω₂, F) :=
  fun (f : 𝓓^{n₁}(Ω₁, F)) ↦
    if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then
      { toFun := (⇑f : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
    else 0
x : Compacts E
h_1 : (↑x : Set E) ⊆ (↑Ω₁ : Set E)
x_1 : 𝓓^{n₁}_{x}(E, F)
a : E
h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂
⊢ ({ toFun := (⇑x_1 : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ : 𝓓^{n₂}(Ω₂, F) } :
        (a : E) → F)
      a =
    (((ofSupportedInCLM 𝕜 ⋯ ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 : (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F)) x_1 :
          𝓓^{n₂}(Ω₂, F)) :
        (a : E) → F)
      a

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)) → 𝓓^{n₂}(Ω₂, F) :=
  fun (f : 𝓓^{n₁}(Ω₁, F)) ↦
    if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then
      { toFun := (⇑f : (a : E) → F), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
    else 0
x : Compacts E
h_1 : (↑x : Set E) ⊆ (↑Ω₁ : Set E)
x_1 : 𝓓^{n₁}_{x}(E, F)
a : E
h : ¬(n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂)
⊢ (0 : (a : E) → F) a = (((0 : (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F)) x_1 : 𝓓^{n₂}(Ω₂, F)) : (a : E) → F) a

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)
rw :
  (⇑(((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)
⊢ (⇑(((monoCLM 𝕜 : 𝓓^{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)

Tactic:
rw [monoCLM]

Premises used: TestFunction.monoCLM
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)
neg :
  ∀ (h : ¬(n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂)),
    (⇑(((TestFunction.limitCLM 𝕜 (fun (f : 𝓓^{n₁}(Ω₁, F)) ↦ 0)
                    (fun (K : Compacts E) (K_sub_Ω₁ : (↑K : Set E) ⊆ (↑Ω₁ : Set E)) ↦ 0) ⋯ :
                  𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)) :
                (a : 𝓓^{n₁}(Ω₁, F)) → 𝓓^{n₂}(Ω₂, F))
              f :
            𝓓^{n₂}(Ω₂, F)) :
        (a : E) → F) =
      (⇑0 : (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)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)
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)

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)
h : ¬(n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂)
⊢ (⇑(((TestFunction.limitCLM 𝕜 (fun (f : 𝓓^{n₁}(Ω₁, F)) ↦ 0)
                  (fun (K : Compacts E) (K_sub_Ω₁ : (↑K : Set E) ⊆ (↑Ω₁ : Set E)) ↦ 0) ⋯ :
                𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)) :
              (a : 𝓓^{n₁}(Ω₁, F)) → 𝓓^{n₂}(Ω₂, F))
            f :
          𝓓^{n₂}(Ω₂, F)) :
      (a : E) → F) =
    (⇑0 : (a : E) → F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₁ ∧ Ω₁ ≤ Ω₂)
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
⊢ Eq (α := 𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)) (monoCLM 𝕜 : 𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F))
    (0 : 𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F))

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.TestFunction
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₁ ∧ Ω₁ ≤ Ω₂)
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:
simp [H]
-- Module: Mathlib.Analysis.Distribution.TestFunction
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
𝕜' : Type u_6
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedSpace 𝕜' F
inst_10 : Algebra ℝ 𝕜'
inst_11 : IsScalarTower ℝ 𝕜' F
⊢ Eq (α := (a : 𝓓^{n₁}(Ω₁, F)) → 𝓓^{n₂}(Ω₂, F))
    (⇑(monoCLM 𝕜 : 𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)) : (a : 𝓓^{n₁}(Ω₁, F)) → 𝓓^{n₂}(Ω₂, F))
    (⇑(monoCLM 𝕜' : 𝓓^{n₁}(Ω₁, F) →L[𝕜'] 𝓓^{n₂}(Ω₂, F)) : (a : 𝓓^{n₁}(Ω₁, F)) → 𝓓^{n₂}(Ω₂, F))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
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_1 : (↑x : Set E) ⊆ (↑Ω : Set E)
x_1 : 𝓓^{n}_{x}(E, F)
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.TestFunction
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_1 : (↑x : Set E) ⊆ (↑Ω : Set E)
x_1 : 𝓓^{n}_{x}(E, F)
a x_2 : E
h :
  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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp [Φ]
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)
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)
⊢ 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)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Distribution.TestFunction
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_1 : (↑x : Set E) ⊆ (↑Ω : Set E)
x_1 : 𝓓^{n}_{x}(E, F)
a x_2 : E
h : 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)

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Distribution.TestFunction
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_1 : (↑x : Set E) ⊆ (↑Ω : Set E)
x_1 : 𝓓^{n}_{x}(E, F)
a x_2 : E
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:
simp [h]
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)
h : k + 1 ≤ n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)
h : ¬k + 1 ≤ n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
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)
hk : k + 1 ≤ n
⊢ (⇑(((fderivCLM 𝕜 n k : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F)) f :
          𝓓^{k}(Ω, E →L[ℝ] F)) :
      (a : E) → E →L[ℝ] F) =
    fderiv ℝ (⇑f : (a : E) → F)

Tactic:
simp [hk]
-- Module: Mathlib.Analysis.Distribution.TestFunction
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
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
⊢ 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))

Tactic:
ext : 2
-- Module: Mathlib.Analysis.Distribution.TestFunction
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
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:
simp [not_le_of_gt hk]

Premises used: not_le_of_gt