Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: case pos
𝕜 : Type u_1
𝕂 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
F' : Type u_5
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
inst✝² : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
Φ : 𝓓^{n}(Ω, F) → 𝓓^{k}(Ω, E →L[ℝ] F) :=
  fun f ↦
    if hk : k + 1 ≤ n then { toFun := fderiv ℝ ⇑f, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
    else 0
x✝³ : Compacts E
x✝² : ↑x✝³ ⊆ ↑Ω
x✝¹ : 𝓓^{n}_{x✝³}(E, F)
a✝ x✝ : E
h : k + 1 ≤ n
⊢ ({ toFun := fderiv ℝ ⇑(ofSupportedIn x✝² x✝¹), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ } a✝)
      x✝ =
    ((ofSupportedIn x✝² ((ContDiffMapSupportedIn.fderivCLM 𝕜 n k) x✝¹)) a✝) x✝

pp: case neg
𝕜 : Type u_1
𝕂 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
F' : Type u_5
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
inst✝² : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
Φ : 𝓓^{n}(Ω, F) → 𝓓^{k}(Ω, E →L[ℝ] F) :=
  fun f ↦
    if hk : k + 1 ≤ n then { toFun := fderiv ℝ ⇑f, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
    else 0
x✝³ : Compacts E
x✝² : ↑x✝³ ⊆ ↑Ω
x✝¹ : 𝓓^{n}_{x✝³}(E, F)
a✝ x✝ : E
h : ¬k + 1 ≤ n
⊢ (0 a✝) x✝ = ((ofSupportedIn x✝² ((ContDiffMapSupportedIn.fderivCLM 𝕜 n k) x✝¹)) a✝) x✝

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u_1
𝕂 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
F' : Type u_5
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
inst✝² : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
Φ : 𝓓^{n}(Ω, F) → 𝓓^{k}(Ω, E →L[ℝ] F) :=
  fun f ↦
    if hk : k + 1 ≤ n then { toFun := fderiv ℝ ⇑f, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
    else 0
x✝³ : Compacts E
x✝² : ↑x✝³ ⊆ ↑Ω
x✝¹ : 𝓓^{n}_{x✝³}(E, F)
a✝ x✝ : E
h : k + 1 ≤ n
⊢ ({ toFun := fderiv ℝ ⇑(ofSupportedIn x✝² x✝¹), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ } a✝)
      x✝ =
    ((ofSupportedIn x✝² ((ContDiffMapSupportedIn.fderivCLM 𝕜 n k) x✝¹)) a✝) x✝

case neg
𝕜 : Type u_1
𝕂 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
F' : Type u_5
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
inst✝² : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
Φ : 𝓓^{n}(Ω, F) → 𝓓^{k}(Ω, E →L[ℝ] F) :=
  fun f ↦
    if hk : k + 1 ≤ n then { toFun := fderiv ℝ ⇑f, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
    else 0
x✝³ : Compacts E
x✝² : ↑x✝³ ⊆ ↑Ω
x✝¹ : 𝓓^{n}_{x✝³}(E, F)
a✝ x✝ : E
h : ¬k + 1 ≤ n
⊢ (0 a✝) x✝ = ((ofSupportedIn x✝² ((ContDiffMapSupportedIn.fderivCLM 𝕜 n k) x✝¹)) a✝) x✝