awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ∞
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)
⊢ LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F)) (topologicalSpace Ω F n)
      (induced
        (⇑((↑ℝ :
                {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)
        t) ↔
    ∀ (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_Ω)
have this₁ : ContinuousSMul ℝ 𝓓^{n}(Ω, F)
Tactic: have : @ContinuousSMul ℝ _ _ _ (induced (f.restrictScalars ℝ) t) := continuousSMul_induced _
-- 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 : ℕ∞
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)
⊢ LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F)) (topologicalSpace Ω F n)
      (induced
        (⇑((↑ℝ :
                {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)
        t) ↔
    ∀ (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_Ω)
have this₁ : LocallyConvexSpace ℝ 𝓓^{n}(Ω, F)
Tactic: have : @LocallyConvexSpace ℝ _ _ _ _ _ (induced (f.restrictScalars ℝ) t) := .induced _
-- 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 : ℕ∞
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 }
⊢ Continuous[_, t] (⇑Φ : (a : 𝓓^{n}(Ω, F)) → V)
have rwa : ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
  Continuous[_, t] ((⇑Φ : (a : 𝓓^{n}(Ω, F)) → V) ∘ ofSupportedIn K_sub_Ω)
Tactic: rwa [TestFunction.continuous_iff_continuous_comp]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (hypothesis)
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' := ⋯ }
⊢ toFun (f + g) = toFun f + toFun g
have K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
Tactic: have K_sub_Ω : (K : Set E) ⊆ Ω := union_subset f.tsupport_subset g.tsupport_subset
-- 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 : ℕ∞
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 (f + g) = toFun f + toFun g
have change : toFun (ofSupportedIn K_sub_Ω (f_K + g_K)) = toFun (ofSupportedIn K_sub_Ω f_K) + toFun (ofSupportedIn K_sub_Ω g_K)
Tactic: change toFun (ofSupportedIn K_sub_Ω (f_K + g_K)) =
      toFun (ofSupportedIn K_sub_Ω f_K) + toFun (ofSupportedIn K_sub_Ω g_K)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (hypothesis)
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' := ⋯ }
⊢ toFun (c • f) = c • toFun f
have K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
Tactic: have K_sub_Ω : (K : Set E) ⊆ Ω := f.tsupport_subset
-- 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 : ℕ∞
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 (c • f) = c • toFun f
have change : toFun (ofSupportedIn K_sub_Ω (c • f_K)) = c • toFun (ofSupportedIn K_sub_Ω f_K)
Tactic: change toFun (ofSupportedIn K_sub_Ω (c • f_K)) = c • toFun (ofSupportedIn K_sub_Ω f_K)
-- 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
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)
⊢ Φ (ofSupportedIn h 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 :
          𝓓^{n}_{x}(E, F) →L[𝕜] 𝓓^{n}(Ω, F')) :
        (a : 𝓓^{n}_{x}(E, F)) → 𝓓^{n}(Ω, F'))
      x_1
have h : ∀ (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: 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)) → 𝓓^{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)
⊢ Φ (ofSupportedIn h 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 :
        (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F))
      x_1
have h : ∀ (a : E),
  (Φ (ofSupportedIn h x_1) : (a : E) → F) a =
    ((((fun (K : Compacts E) (K_sub_Ω₁ : (↑K : Set E) ⊆ (↑Ω₁ : Set E)) ↦
                  (if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then ofSupportedInCLM 𝕜 sorry ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 else 0 :
                    𝓓^{n₁}_{K}(E, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)))
                x h :
              (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F))
            x_1 :
          𝓓^{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)) → 𝓓^{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
⊢ (Φ (ofSupportedIn h 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 :
              (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F))
            x_1 :
          𝓓^{n₂}(Ω₂, F)) :
        (a : E) → F)
      a
have h : (if h_1 : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then
        { toFun := (⇑x_1 : (a : E) → F), contDiff' := sorry, hasCompactSupport' := sorry, tsupport_subset' := sorry :
          𝓓^{n₂}(Ω₂, F) }
      else 0 :
      (a : E) → F)
    a =
  (((if h_1 : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then ofSupportedInCLM 𝕜 sorry ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 else 0 :
            (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F))
          x_1 :
        𝓓^{n₂}(Ω₂, F)) :
      (a : E) → F)
    a
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)) → 𝓓^{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
⊢ (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
have pos : ∀ (h_1 : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂),
  ({ toFun := (⇑x_1 : (a : E) → F), contDiff' := sorry, hasCompactSupport' := sorry, tsupport_subset' := sorry : 𝓓^{n₂}(Ω₂, F) } :
        (a : E) → F)
      a =
    (((ofSupportedInCLM 𝕜 sorry ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 : (a : 𝓓^{n₁}_{x}(E, F)) → 𝓓^{n₂}(Ω₂, F)) x_1 :
          𝓓^{n₂}(Ω₂, F)) :
        (a : E) → F)
      a
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)) → 𝓓^{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
⊢ (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
have 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
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₁ n₂ : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n₁}(Ω₁, 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)
have rw : (⇑(((TestFunction.limitCLM 𝕜
                (fun (f : 𝓓^{n₁}(Ω₁, F)) ↦
                  if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then
                    { toFun := (⇑f : (a : E) → F), contDiff' := sorry, hasCompactSupport' := sorry, tsupport_subset' := sorry :
                      𝓓^{n₂}(Ω₂, F) }
                  else 0)
                (fun (K : Compacts E) (K_sub_Ω₁ : (↑K : Set E) ⊆ (↑Ω₁ : Set E)) ↦
                  if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then ofSupportedInCLM 𝕜 sorry ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 else 0)
                sorry :
              𝓓^{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]
-- 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)
⊢ (⇑(((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 pos : ∀ (h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂),
  (⇑(((TestFunction.limitCLM 𝕜
                  (fun (f : 𝓓^{n₁}(Ω₁, F)) ↦
                    { toFun := (⇑f : (a : E) → F), contDiff' := sorry, hasCompactSupport' := sorry, tsupport_subset' := sorry :
                      𝓓^{n₂}(Ω₂, F) })
                  (fun (K : Compacts E) (K_sub_Ω₁ : (↑K : Set E) ⊆ (↑Ω₁ : Set E)) ↦
                    ofSupportedInCLM 𝕜 sorry ∘SL ContDiffMapSupportedIn.monoCLM 𝕜)
                  sorry :
                𝓓^{n₁}(Ω₁, F) →L[𝕜] 𝓓^{n₂}(Ω₂, F)) :
              (a : 𝓓^{n₁}(Ω₁, F)) → 𝓓^{n₂}(Ω₂, F))
            f :
          𝓓^{n₂}(Ω₂, F)) :
      (a : E) → F) =
    (⇑f : (a : E) → F)
Tactic: split_ifs