mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q : M
⊢ writtenInExtChartAt I I q Sum.inl =ᶠ[𝓝[range ↑I] ↑(extChartAt I q) q] id

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
⊢ ↑I.symm ⁻¹' (chartAt H q').target ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I q') q'

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
hmem : ↑I.symm ⁻¹' (chartAt H q').target ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I q') q'
z : H
hyT : ↑I z ∈ ↑I.symm ⁻¹' (chartAt H q').target
⊢ ?m.212 ∈ (chartAt H q').target

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
⊢ writtenInExtChartAt I I q' Sum.inr =ᶠ[𝓝[range ↑I] ↑(extChartAt I q') q'] id

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q : M
⊢ ContinuousWithinAt Sum.inl s q

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q : M
this : writtenInExtChartAt I I q Sum.inl =ᶠ[𝓝[↑(extChartAt I q).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I q) q] id
⊢ writtenInExtChartAt I I q Sum.inl (↑(extChartAt I q) q) = id (↑(extChartAt I q) q)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q : M
⊢ HasMFDerivAt[s] Sum.inl q (ContinuousLinearMap.id 𝕜 (TangentSpace I q))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
p : M ⊕ M'
q : M
⊢ HasMFDerivAt% Sum.inl q (ContinuousLinearMap.id 𝕜 (TangentSpace I p))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
t : Set M'
⊢ ContinuousWithinAt Sum.inr t q'

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_9
f : N → H
g : N → H'
ϕ : N → E →L[𝕜] E'
x₀ : N
⊢ inTangentCoordinates I I' f g ϕ x₀ = ϕ

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
t : Set M'
this : writtenInExtChartAt I I q' Sum.inr =ᶠ[𝓝[↑(extChartAt I q').symm ⁻¹' t ∩ range ↑I] ↑(extChartAt I q') q'] id
⊢ writtenInExtChartAt I I q' Sum.inr (↑(extChartAt I q') q') = id (↑(extChartAt I q') q')

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffAt[s] p.proj
h's : s ⊆ (trivializationAt F Z p.proj).baseSet
this :
  (↑(extChartAt I p.proj).symm ⁻¹' s ∩ range ↑I) ×ˢ univ ⊆
    ↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm ⁻¹' TotalSpace.proj ⁻¹' s ∩ range ↑(I.prod 𝓘(𝕜, F))
w : F := (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p).2
⊢ ↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p = (↑(extChartAt I p.proj) p.proj, w)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
t : Set M'
⊢ HasMFDerivAt[t] Sum.inr q' (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
p : M ⊕ M'
q' : M'
⊢ HasMFDerivAt% Sum.inr q' (ContinuousLinearMap.id 𝕜 (TangentSpace I p))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁵ : TopologicalSpace H
G : Type u_7
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
α : Sort u_13
h : M ≃ₘ^n⟮I, J⟯ N
f : α → M
⊢ range (⇑h ∘ f) = ⇑h.symm ⁻¹' range f

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
p : M ⊕ M'
q : M
⊢ mfderiv% Sum.inl q = ContinuousLinearMap.id 𝕜 (TangentSpace I p)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
⊢ mfderiv% Sum.inr q' = ContinuousLinearMap.id 𝕜 (TangentSpace I q')

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝³³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³² : NormedAddCommGroup E
inst✝³¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝³⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝²⁹ : TopologicalSpace M
inst✝²⁸ : ChartedSpace H M
E' : Type u_5
inst✝²⁷ : NormedAddCommGroup E'
inst✝²⁶ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝²⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝²⁴ : TopologicalSpace M'
inst✝²³ : ChartedSpace H' M'
E'' : Type u_8
inst✝²² : NormedAddCommGroup E''
inst✝²¹ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝²⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹⁹ : TopologicalSpace M''
inst✝¹⁸ : ChartedSpace H'' M''
F : Type u_11
inst✝¹⁷ : NormedAddCommGroup F
inst✝¹⁶ : NormedSpace 𝕜 F
G : Type u_12
inst✝¹⁵ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace G N
F' : Type u_14
inst✝¹² : NormedAddCommGroup F'
inst✝¹¹ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝¹⁰ : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace G' N'
F₁ : Type u_17
inst✝⁷ : NormedAddCommGroup F₁
inst✝⁶ : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
F₃ : Type u_19
inst✝³ : NormedAddCommGroup F₃
inst✝² : NormedSpace 𝕜 F₃
F₄ : Type u_20
inst✝¹ : NormedAddCommGroup F₄
inst✝ : NormedSpace 𝕜 F₄
s : Set M
x z : M
f g : M → E'
f' g' : TangentSpace I z →L[𝕜] E'
hf : MDiffAt f z
hg : MDiffAt g z
⊢ TangentSpace I z →L[𝕜] TangentSpace 𝓘(𝕜, E') ((f + g) z)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝³³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³² : NormedAddCommGroup E
inst✝³¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝³⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝²⁹ : TopologicalSpace M
inst✝²⁸ : ChartedSpace H M
E' : Type u_5
inst✝²⁷ : NormedAddCommGroup E'
inst✝²⁶ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝²⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝²⁴ : TopologicalSpace M'
inst✝²³ : ChartedSpace H' M'
E'' : Type u_8
inst✝²² : NormedAddCommGroup E''
inst✝²¹ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝²⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹⁹ : TopologicalSpace M''
inst✝¹⁸ : ChartedSpace H'' M''
F : Type u_11
inst✝¹⁷ : NormedAddCommGroup F
inst✝¹⁶ : NormedSpace 𝕜 F
G : Type u_12
inst✝¹⁵ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace G N
F' : Type u_14
inst✝¹² : NormedAddCommGroup F'
inst✝¹¹ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝¹⁰ : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace G' N'
F₁ : Type u_17
inst✝⁷ : NormedAddCommGroup F₁
inst✝⁶ : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
F₃ : Type u_19
inst✝³ : NormedAddCommGroup F₃
inst✝² : NormedSpace 𝕜 F₃
F₄ : Type u_20
inst✝¹ : NormedAddCommGroup F₄
inst✝ : NormedSpace 𝕜 F₄
s : Set M
x z : M
f g : M → E'
f' g' : TangentSpace I z →L[𝕜] E'
hf : MDiffAt[s] f z
hg : MDiffAt[s] g z
hs : UniqueMDiffAt[s] z
⊢ TangentSpace I z →L[𝕜] TangentSpace 𝓘(𝕜, E') ((f + g) z)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffAt[s] p.proj
h's : s ⊆ (trivializationAt F Z p.proj).baseSet
this :
  (↑(extChartAt I p.proj).symm ⁻¹' s ∩ range ↑I) ×ˢ univ ⊆
    ↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm ⁻¹' TotalSpace.proj ⁻¹' s ∩ range ↑(I.prod 𝓘(𝕜, F))
⊢ UniqueMDiffAt[TotalSpace.proj ⁻¹' s] p

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁸ : TopologicalSpace H
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
G : Type u_7
inst✝⁶ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
M' : Type u_10
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
Hfh : ContMDiffWithinAt I I' m (f ∘ ⇑h) s x
⊢ ContMDiffWithinAt J I' m f (⇑h.symm ⁻¹' s) (h x)

Tactic:
rw [← h.symm_apply_apply x] at Hfh

Goal state after:
case mp
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁸ : TopologicalSpace H
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
G : Type u_7
inst✝⁶ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
M' : Type u_10
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
Hfh : ContMDiffWithinAt I I' m (f ∘ ⇑h) s (h.symm (h x))
⊢ ContMDiffWithinAt J I' m f (⇑h.symm ⁻¹' s) (h x)
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
s : Set M
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → TangentSpace I z →L[𝕜] E'
hf : ∀ i ∈ t, HasMFDerivAt[s] (f i) z (f' i)
⊢ HasMFDerivAt[s] (∑ i ∈ t, f i) z (∑ i ∈ t, f' i)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → TangentSpace I z →L[𝕜] E'
hf : ∀ i ∈ t, HasMFDerivAt% (f i) z (f' i)
⊢ HasMFDerivAt% (∑ i ∈ t, f i) z (∑ i ∈ t, f' i)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
z : M
ι : Type
t : Finset ι
f : ι → M → E'
hf : ∀ i ∈ t, MDiffAt (f i) z
⊢ MDiffAt (∑ i ∈ t, f i) z

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁸ : TopologicalSpace H
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
G : Type u_7
inst✝⁶ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
M' : Type u_10
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
⊢ ContMDiffWithinAt I I' m (f ∘ ⇑h) s x ↔ ContMDiffWithinAt J I' m f (⇑h.symm ⁻¹' s) (h x)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁸ : TopologicalSpace H
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
G : Type u_7
inst✝⁶ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
M' : Type u_10
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
hm : m ≤ n
x✝ : M
⊢ x✝ ∈ s → ContMDiffWithinAt I I' m (f ∘ ⇑h) s x✝ ↔
    h.toEquiv x✝ ∈ ⇑h.symm ⁻¹' s → ContMDiffWithinAt J I' m f (⇑h.symm ⁻¹' s) (h.toEquiv x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : TangentSpace I z →L[𝕜] E'
hf : HasMFDerivAt% (-f) z (-f')
⊢ HasMFDerivAt% f z f'

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
s : Set M
z : M
f : M → E'
hf : MDiffAt[s] (-f) z
⊢ MDiffAt[s] f z

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
z : M
f : M → E'
hf : MDiffAt (-f) z
⊢ MDiffAt f z

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁸ : TopologicalSpace H
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
G : Type u_7
inst✝⁶ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
M' : Type u_10
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : M' → M
hm : m ≤ n
s : Set M'
x : M'
Hhf : ContMDiffWithinAt I' J m (⇑h ∘ f) s x
⊢ ContMDiffWithinAt I' I m f s x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁵ : TopologicalSpace H
G : Type u_7
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
hn : n ≠ 0
s : Set M
hs : UniqueMDiff[s]
⊢ UniqueMDiff[⇑h '' s]

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
hn : n ≠ 0
s : Set E
⊢ UniqueDiffOn 𝕜 (⇑h '' s) ↔ UniqueDiffOn 𝕜 s

Tactic:
by

Goal state after: