awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ∞
inst_6 : SMulCommClass ℝ 𝕜 F
K : Compacts E
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
⊢ Eq (α := (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}(Ω, F)) (⇑(ofSupportedInCLM 𝕜 K_sub_Ω) : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}(Ω, F))
    (ofSupportedIn K_sub_Ω)

Tactic:
rfl

Premises used: TestFunction.ofSupportedIn, 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 : ℕ∞
V : Type u_6
inst_6 : AddCommGroup V
inst_7 : Module ℝ V
t : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul ℝ V
inst_10 : LocallyConvexSpace ℝ V
inst_11 : Algebra ℝ 𝕜
inst_12 : IsScalarTower ℝ 𝕜 F
inst_13 : Module 𝕜 V
inst_14 : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
simp_rw :
  Continuous[_, t]
      (⇑((↑ℝ :
              {S : Type u_1} →
                {M : Type (max u_3 u_4)} →
                  {M₂ : Type u_6} →
                    [inst : Semiring ℝ] →
                      [inst_15 : Semiring S] →
                        [inst_16 : AddCommMonoid M] →
                          [inst_17 : AddCommMonoid M₂] →
                            [inst_18 : Module ℝ M] →
                              [inst_19 : Module ℝ M₂] →
                                [inst_20 : Module S M] →
                                  [inst_21 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
            f) :
        (a : 𝓓^{n}(Ω, F)) → V) ↔
    ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
      Continuous[_, t]
        ((⇑((↑ℝ :
                  {S : Type u_1} →
                    {M : Type (max u_3 u_4)} →
                      {M₂ : Type u_6} →
                        [inst : Semiring ℝ] →
                          [inst_15 : Semiring S] →
                            [inst_16 : AddCommMonoid M] →
                              [inst_17 : AddCommMonoid M₂] →
                                [inst_18 : Module ℝ M] →
                                  [inst_19 : Module ℝ M₂] →
                                    [inst_20 : Module S M] →
                                      [inst_21 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                f) :
            (a : 𝓓^{n}(Ω, F)) → V) ∘
          ofSupportedIn K_sub_Ω)
⊢ Continuous[_, t] (⇑f : (a : 𝓓^{n}(Ω, F)) → V) ↔
    ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
      Continuous[_, t] ((⇑f : (a : 𝓓^{n}(Ω, F)) → V) ∘ ofSupportedIn K_sub_Ω)

Tactic:
simp_rw [← f.coe_restrictScalars ℝ]

Premises used: Real, LinearMap.coe_restrictScalars
-- 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 : ℕ∞
V : Type u_6
inst_6 : AddCommGroup V
inst_7 : Module ℝ V
t : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul ℝ V
inst_10 : LocallyConvexSpace ℝ V
inst_11 : Algebra ℝ 𝕜
inst_12 : IsScalarTower ℝ 𝕜 F
inst_13 : Module 𝕜 V
inst_14 : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
⊢ IsTopologicalAddGroup 𝓓^{n}(Ω, F)

Tactic:
have : @IsTopologicalAddGroup _ (induced (f.restrictScalars ℝ) t) _ :=
    topologicalAddGroup_induced _
-- 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 : ℕ∞
V : Type u_6
inst_6 : AddCommGroup V
inst_7 : Module ℝ V
t : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul ℝ V
inst_10 : LocallyConvexSpace ℝ V
inst_11 : Algebra ℝ 𝕜
inst_12 : IsScalarTower ℝ 𝕜 F
inst_13 : Module 𝕜 V
inst_14 : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
this : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
⊢ ContinuousSMul ℝ 𝓓^{n}(Ω, F)

Tactic:
have : @ContinuousSMul ℝ _ _ _ (induced (f.restrictScalars ℝ) t) := continuousSMul_induced _
-- 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 : ℕ∞
V : Type u_6
inst_6 : AddCommGroup V
inst_7 : Module ℝ V
t : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul ℝ V
inst_10 : LocallyConvexSpace ℝ V
inst_11 : Algebra ℝ 𝕜
inst_12 : IsScalarTower ℝ 𝕜 F
inst_13 : Module 𝕜 V
inst_14 : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
this_1 : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
this : ContinuousSMul ℝ 𝓓^{n}(Ω, F)
⊢ LocallyConvexSpace ℝ 𝓓^{n}(Ω, F)

Tactic:
have : @LocallyConvexSpace ℝ _ _ _ _ _ (induced (f.restrictScalars ℝ) t) := .induced _
-- 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 : ℕ∞
V : Type u_6
inst_9 : AddCommGroup V
inst_10 : Module ℝ V
t : TopologicalSpace V
inst_11 : IsTopologicalAddGroup V
inst_12 : ContinuousSMul ℝ V
inst_13 : LocallyConvexSpace ℝ V
inst_14 : Algebra ℝ 𝕜
inst_15 : IsScalarTower ℝ 𝕜 F
inst_16 : Module 𝕜 V
inst_17 : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
map_add : ∀ (f g : 𝓓^{n}(Ω, F)), toFun (f + g) = toFun f + toFun g
map_smul : ∀ (c : 𝕜) (f : 𝓓^{n}(Ω, F)), toFun (c • f) = c • toFun f
cont : ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)), Continuous[_, t] (toFun ∘ ofSupportedIn K_sub_Ω)
Φ : 𝓓^{n}(Ω, F) →ₗ[𝕜] V := { toFun := toFun, map_add' := map_add, map_smul' := map_smul }
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
    Continuous[_, t] ((⇑Φ : (a : 𝓓^{n}(Ω, F)) → V) ∘ ofSupportedIn K_sub_Ω)
⊢ Continuous[_, t] (⇑Φ : (a : 𝓓^{n}(Ω, F)) → V)

Tactic:
rwa [TestFunction.continuous_iff_continuous_comp]

Premises used: TestFunction.continuous_iff_continuous_comp
-- 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 : ℕ∞
V : Type u_6
inst_9 : AddCommGroup V
inst_10 : Module ℝ V
t : TopologicalSpace V
inst_11 : IsTopologicalAddGroup V
inst_12 : ContinuousSMul ℝ V
inst_13 : LocallyConvexSpace ℝ V
inst_14 : Algebra ℝ 𝕜
inst_15 : IsScalarTower ℝ 𝕜 F
inst_16 : Module 𝕜 V
inst_17 : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → (↑K : Set E) ⊆ (↑Ω : Set E) → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) (f : 𝓓^{n}_{K}(E, F)),
    toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω : (a : 𝓓^{n}_{K}(E, F)) → V) f
f g : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport (⇑f : (a : E) → F) ∪ tsupport (⇑g : (a : E) → F), isCompact' := ⋯ }
⊢ (↑K : Set E) ⊆ (↑Ω : Set E)

Tactic:
have K_sub_Ω : (K : Set E) ⊆ Ω := union_subset f.tsupport_subset g.tsupport_subset
-- 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 : ℕ∞
V : Type u_6
inst_9 : AddCommGroup V
inst_10 : Module ℝ V
t : TopologicalSpace V
inst_11 : IsTopologicalAddGroup V
inst_12 : ContinuousSMul ℝ V
inst_13 : LocallyConvexSpace ℝ V
inst_14 : Algebra ℝ 𝕜
inst_15 : IsScalarTower ℝ 𝕜 F
inst_16 : Module 𝕜 V
inst_17 : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → (↑K : Set E) ⊆ (↑Ω : Set E) → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) (f : 𝓓^{n}_{K}(E, F)),
    toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω : (a : 𝓓^{n}_{K}(E, F)) → V) f
f g : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport (⇑f : (a : E) → F) ∪ tsupport (⇑g : (a : E) → F), isCompact' := ⋯ }
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
f_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
g_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
change :
  toFun (ofSupportedIn K_sub_Ω (f_K + g_K)) = toFun (ofSupportedIn K_sub_Ω f_K) + toFun (ofSupportedIn K_sub_Ω g_K)
⊢ toFun (f + g) = toFun f + toFun g

Tactic:
change toFun (ofSupportedIn K_sub_Ω (f_K + g_K)) =
      toFun (ofSupportedIn K_sub_Ω f_K) + toFun (ofSupportedIn K_sub_Ω g_K)

Premises used: TestFunction.ofSupportedIn, HAdd.hAdd
-- 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 : ℕ∞
V : Type u_6
inst_9 : AddCommGroup V
inst_10 : Module ℝ V
t : TopologicalSpace V
inst_11 : IsTopologicalAddGroup V
inst_12 : ContinuousSMul ℝ V
inst_13 : LocallyConvexSpace ℝ V
inst_14 : Algebra ℝ 𝕜
inst_15 : IsScalarTower ℝ 𝕜 F
inst_16 : Module 𝕜 V
inst_17 : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → (↑K : Set E) ⊆ (↑Ω : Set E) → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) (f : 𝓓^{n}_{K}(E, F)),
    toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω : (a : 𝓓^{n}_{K}(E, F)) → V) f
f g : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport (⇑f : (a : E) → F) ∪ tsupport (⇑g : (a : E) → F), isCompact' := ⋯ }
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
f_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
g_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
⊢ toFun (ofSupportedIn K_sub_Ω (f_K + g_K)) = toFun (ofSupportedIn K_sub_Ω f_K) + toFun (ofSupportedIn K_sub_Ω g_K)

Tactic:
simp [toFun_eq_T]
-- 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 : ℕ∞
V : Type u_6
inst_9 : AddCommGroup V
inst_10 : Module ℝ V
t : TopologicalSpace V
inst_11 : IsTopologicalAddGroup V
inst_12 : ContinuousSMul ℝ V
inst_13 : LocallyConvexSpace ℝ V
inst_14 : Algebra ℝ 𝕜
inst_15 : IsScalarTower ℝ 𝕜 F
inst_16 : Module 𝕜 V
inst_17 : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → (↑K : Set E) ⊆ (↑Ω : Set E) → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) (f : 𝓓^{n}_{K}(E, F)),
    toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω : (a : 𝓓^{n}_{K}(E, F)) → V) f
toFun_add : ∀ (f g : 𝓓^{n}(Ω, F)), toFun (f + g) = toFun f + toFun g
c : 𝕜
f : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport (⇑f : (a : E) → F), isCompact' := ⋯ }
⊢ (↑K : Set E) ⊆ (↑Ω : Set E)

Tactic:
have K_sub_Ω : (K : Set E) ⊆ Ω := f.tsupport_subset
-- 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 : ℕ∞
V : Type u_6
inst_9 : AddCommGroup V
inst_10 : Module ℝ V
t : TopologicalSpace V
inst_11 : IsTopologicalAddGroup V
inst_12 : ContinuousSMul ℝ V
inst_13 : LocallyConvexSpace ℝ V
inst_14 : Algebra ℝ 𝕜
inst_15 : IsScalarTower ℝ 𝕜 F
inst_16 : Module 𝕜 V
inst_17 : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → (↑K : Set E) ⊆ (↑Ω : Set E) → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) (f : 𝓓^{n}_{K}(E, F)),
    toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω : (a : 𝓓^{n}_{K}(E, F)) → V) f
toFun_add : ∀ (f g : 𝓓^{n}(Ω, F)), toFun (f + g) = toFun f + toFun g
c : 𝕜
f : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport (⇑f : (a : E) → F), isCompact' := ⋯ }
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
f_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
change : toFun (ofSupportedIn K_sub_Ω (c • f_K)) = c • toFun (ofSupportedIn K_sub_Ω f_K)
⊢ toFun (c • f) = c • toFun f

Tactic:
change toFun (ofSupportedIn K_sub_Ω (c • f_K)) = c • toFun (ofSupportedIn K_sub_Ω f_K)

Premises used: TestFunction.ofSupportedIn, HSMul.hSMul
-- 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 : ℕ∞
V : Type u_6
inst_9 : AddCommGroup V
inst_10 : Module ℝ V
t : TopologicalSpace V
inst_11 : IsTopologicalAddGroup V
inst_12 : ContinuousSMul ℝ V
inst_13 : LocallyConvexSpace ℝ V
inst_14 : Algebra ℝ 𝕜
inst_15 : IsScalarTower ℝ 𝕜 F
inst_16 : Module 𝕜 V
inst_17 : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → (↑K : Set E) ⊆ (↑Ω : Set E) → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) (f : 𝓓^{n}_{K}(E, F)),
    toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω : (a : 𝓓^{n}_{K}(E, F)) → V) f
toFun_add : ∀ (f g : 𝓓^{n}(Ω, F)), toFun (f + g) = toFun f + toFun g
c : 𝕜
f : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport (⇑f : (a : E) → F), isCompact' := ⋯ }
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
f_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
⊢ toFun (ofSupportedIn K_sub_Ω (c • f_K)) = c • toFun (ofSupportedIn K_sub_Ω f_K)

Tactic:
simp [toFun_eq_T]
-- 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 : ℕ∞
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)) → E →ᵇ F)
    (⇑(toBoundedContinuousFunctionCLM 𝕜 : 𝓓^{n}(Ω, F) →L[𝕜] E →ᵇ F) : (a : 𝓓^{n}(Ω, F)) → E →ᵇ F)
    (⇑(toBoundedContinuousFunctionCLM 𝕜' : 𝓓^{n}(Ω, F) →L[𝕜'] E →ᵇ F) : (a : 𝓓^{n}(Ω, F)) → E →ᵇ F)

Tactic:
rfl

Premises used: 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 : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f g : 𝓓^{n}(Ω, F)
⊢ Eq (α := E →ᵇ F)
      (((toBoundedContinuousFunctionCLM 𝕜 : 𝓓^{n}(Ω, F) →L[𝕜] E →ᵇ F) : (a : 𝓓^{n}(Ω, F)) → E →ᵇ F) f : E →ᵇ F)
      (((toBoundedContinuousFunctionCLM 𝕜 : 𝓓^{n}(Ω, F) →L[𝕜] E →ᵇ F) : (a : 𝓓^{n}(Ω, F)) → E →ᵇ F) g : E →ᵇ F) →
    f = g

Tactic:
simp [toBoundedContinuousFunctionCLM]

Premises used: TestFunction.toBoundedContinuousFunctionCLM
-- 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 : ℕ∞
⊢ ContinuousEval 𝓓^{n}(Ω, F) E F

Tactic:
ContinuousEval.of_continuous_forget
    (toBoundedContinuousFunctionCLM ℝ).continuous

Premises used: Real, ContinuousLinearMap.continuous, ContinuousEval.of_continuous_forget, TestFunction.toBoundedContinuousFunctionCLM
-- 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 : ℕ∞
⊢ T3Space 𝓓^{n}(Ω, F)

Tactic:
suffices T2Space 𝓓^{n}(Ω, F) from inferInstance
  .of_injective_continuous (injective_toBoundedContinuousFunctionCLM ℝ)
    (ContinuousLinearMap.continuous _)

Premises used: Real, T2Space.of_injective_continuous, inferInstance, ContinuousLinearMap.continuous, TestFunction.injective_toBoundedContinuousFunctionCLM, TestFunction.toBoundedContinuousFunctionCLM
-- 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
inst_11 : IsScalarTower ℝ 𝕜 F'
T : F →L[𝕜] F'
Φ : (f : 𝓓^{n}(Ω, F)) → 𝓓^{n}(Ω, F') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : Compacts E
h_1 : (↑x : Set E) ⊆ (↑Ω : Set E)
x_1 : 𝓓^{n}_{x}(E, F)
h :
  ∀ (a : E),
    (Φ (ofSupportedIn h_1 x_1) : (a : E) → F') a =
      (((((fun (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) ↦
                      (ofSupportedInCLM 𝕜 K_sub_Ω ∘SL ContDiffMapSupportedIn.postcompCLM T :
                        𝓓^{n}_{K}(E, F) →L[𝕜] 𝓓^{n}(Ω, F')))
                    x h_1 :
                  𝓓^{n}_{x}(E, F) →L[𝕜] 𝓓^{n}(Ω, F')) :
                (a : 𝓓^{n}_{x}(E, F)) → 𝓓^{n}(Ω, F'))
              x_1 :
            𝓓^{n}(Ω, F')) :
          (a : E) → F')
        a
⊢ Φ (ofSupportedIn h_1 x_1) =
    (((fun (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) ↦
              (ofSupportedInCLM 𝕜 K_sub_Ω ∘SL ContDiffMapSupportedIn.postcompCLM T :
                𝓓^{n}_{K}(E, F) →L[𝕜] 𝓓^{n}(Ω, F')))
            x h_1 :
          𝓓^{n}_{x}(E, F) →L[𝕜] 𝓓^{n}(Ω, F')) :
        (a : 𝓓^{n}_{x}(E, F)) → 𝓓^{n}(Ω, F'))
      x_1

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
inst_11 : IsScalarTower ℝ 𝕜 F'
T : F →L[𝕜] F'
Φ : (f : 𝓓^{n}(Ω, F)) → 𝓓^{n}(Ω, F') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : Compacts E
h : (↑x : Set E) ⊆ (↑Ω : Set E)
x_1 : 𝓓^{n}_{x}(E, F)
a : E
⊢ (Φ (ofSupportedIn h x_1) : (a : E) → F') a =
    (((((fun (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)) ↦
                    (ofSupportedInCLM 𝕜 K_sub_Ω ∘SL ContDiffMapSupportedIn.postcompCLM T :
                      𝓓^{n}_{K}(E, F) →L[𝕜] 𝓓^{n}(Ω, F')))
                  x h :
                𝓓^{n}_{x}(E, F) →L[𝕜] 𝓓^{n}(Ω, F')) :
              (a : 𝓓^{n}_{x}(E, F)) → 𝓓^{n}(Ω, F'))
            x_1 :
          𝓓^{n}(Ω, F')) :
        (a : E) → F')
      a

Tactic:
simp [Φ]
-- 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
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n : ℕ∞
inst_9 : Algebra ℝ 𝕜
inst_10 : IsScalarTower ℝ 𝕜 F
inst_11 : IsScalarTower ℝ 𝕜 F'
T : F →L[𝕜] F'
f : 𝓓^{n}(Ω, F)
⊢ (⇑(((postcompCLM T : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{n}(Ω, F')) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{n}(Ω, F')) f : 𝓓^{n}(Ω, F')) :
      (a : E) → F') =
    (⇑T : (a : F) → F') ∘ (⇑f : (a : E) → 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)) → 𝓓^{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)
h :
  ∀ (a : E),
    (Φ (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
⊢ Φ (ofSupportedIn h_1 x_1) =
    ((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

Tactic:
ext