Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
⊢ extDerivWithin (fun x ↦ (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x)) univ x =
    (extDerivWithin ω univ (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x)

Tactic:
apply extDerivWithin_pullback (r := r)

Goal state after:
case hω
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
⊢ DifferentiableWithinAt 𝕜 ω univ (f x)

case hf
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
⊢ ContDiffWithinAt 𝕜 r f univ x

case hr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
⊢ minSmoothness 𝕜 2 ≤ r

case hs
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
⊢ UniqueDiffOn 𝕜 univ

case hxc
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior univ)

case hxs
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
⊢ x ∈ univ

case hst
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
r : WithTop ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
⊢ MapsTo f univ univ