Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic

Goal state before:
pp: 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)

pp: 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

pp: 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

pp: 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

pp: 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)

pp: 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

pp: 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

Tactic:
<;>

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