mathlib-initiative/mathlib-tactics huggingface dataset:
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
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
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' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
⊢ (I.toPartialEquiv ≫ (↑e).toEquiv.toPartialEquiv).source = univ

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
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
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' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range ↑(I.toPartialEquiv ≫ (↑e).toEquiv.toPartialEquiv))
  else range ↑(I.toPartialEquiv ≫ (↑e).toEquiv.toPartialEquiv) = univ

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
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
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' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
⊢ (interior (range ↑(I.toPartialEquiv ≫ (↑e).toEquiv.toPartialEquiv))).Nonempty

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'
H : Type u_5
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
e : E ≃L[𝕜] E'
x : M
⊢ (extChartAt (I.transContinuousLinearEquiv e) x).target = ⇑e.symm ⁻¹' (extChartAt I x).target

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
G' : Type u_8
inst✝⁹ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
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' : Type u_12
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] F
inst✝ : IsManifold I n M
⊢ IsManifold (I.transContinuousLinearEquiv e) n M

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
x : M
f : M → E'
hs : UniqueMDiffAt[s] x
⊢ mfderiv[s] (-f) x = -mfderiv[s] f x

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
⊢ UniqueMDiffAt[TotalSpace.proj ⁻¹' s] 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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
x : M
f : M → E'
⊢ mfderiv% (-f) x = -mfderiv% f 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
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
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' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
e✝ e : E ≃L[𝕜] F
x : M
⊢ ↑(extChartAt I x).symm (↑(extChartAt I x) x) ∈
    ⇑(Equiv.refl M) ⁻¹' (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M) x)).source

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
this : UniqueMDiffAt[TotalSpace.proj ⁻¹' (s ∩ (trivializationAt F Z p.proj).baseSet)] p
⊢ TotalSpace.proj ⁻¹' (s ∩ (trivializationAt F Z p.proj).baseSet) ⊆ TotalSpace.proj ⁻¹' 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
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
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
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' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
e✝ e : E ≃L[𝕜] F
x : M
⊢ ContMDiffAt I (I.transContinuousLinearEquiv e) n (⇑(Equiv.refl M)) 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'
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.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
⊢ UniqueMDiffAt[TotalSpace.proj ⁻¹' s] 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
s : Set M
z : M
F' : Type u_21
inst✝¹ : NormedRing F'
inst✝ : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivAt[s] p z p'
hq : HasMFDerivAt[s] q z q'
⊢ HasFDerivWithinAt (writtenInExtChartAt I 𝓘(𝕜, F') z (p * q)) (p z •> q' + p' <• q z)
    (↑(extChartAt I z).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I z) z)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.SMul

Goal state before:
pp: 𝕜 : Type u_1
inst✝²² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝²¹ : TopologicalSpace H
E : Type u_3
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹⁸ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁷ : NormedAddCommGroup E'
inst✝¹⁶ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝¹⁵ : TopologicalSpace H''
E'' : Type u_7
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝¹² : TopologicalSpace G
inst✝¹¹ : ChartedSpace H G
M : Type u_9
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H' M
G' : Type u_11
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : ChartedSpace H'' G'
inst✝⁶ : Monoid G'
inst✝⁵ : SMul G G'
inst✝⁴ : MulAction G' M
inst✝³ : SMul G M
inst✝² : IsScalarTower G G' M
n : ℕ∞ω
inst✝¹ : ContMDiffSMul I I'' n G G'
inst✝ : ContMDiffSMul I'' I' n G' M
this : ContMDiff (I.prod I') I' n fun p ↦ (p.1 • 1) • p.2
⊢ ContMDiff (I.prod I') I' n fun p ↦ p.1 • p.2

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.SMul

Goal state before:
pp: 𝕜 : Type u_1
inst✝²² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝²¹ : TopologicalSpace H
E : Type u_3
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹⁸ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁷ : NormedAddCommGroup E'
inst✝¹⁶ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝¹⁵ : TopologicalSpace H''
E'' : Type u_7
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝¹² : TopologicalSpace G
inst✝¹¹ : ChartedSpace H G
M : Type u_9
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H' M
G' : Type u_11
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : ChartedSpace H'' G'
inst✝⁶ : Monoid G'
inst✝⁵ : SMul G G'
inst✝⁴ : MulAction G' M
inst✝³ : SMul G M
inst✝² : IsScalarTower G G' M
n : ℕ∞ω
inst✝¹ : ContMDiffSMul I I'' n G G'
inst✝ : ContMDiffSMul I'' I' n G' M
⊢ ContMDiff (I.prod I') I' n fun p ↦ p.1 • p.2

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.SMul

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
E : Type u_3
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹⁵ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝¹² : TopologicalSpace H''
E'' : Type u_7
inst✝¹¹ : NormedAddCommGroup E''
inst✝¹⁰ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H' M
inst✝⁵ : Monoid G
inst✝⁴ : MulAction G M
n : ℕ∞ω
inst✝³ : ContMDiffSMul I I' n G M
G' : Type u_11
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H'' G'
inst✝ : Monoid G'
f : G' →* G
hf : ContMDiff I'' I n ⇑f
⊢ ContMDiffSMul I'' I' n G' M

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
z : M
F' : Type u_21
inst✝¹ : NormedRing F'
inst✝ : NormedAlgebra 𝕜 F'
p : M → F'
hp : MDiffAt[s] p z
n : ℕ
⊢ MDiffAt[s] (p ^ n) z

Tactic:
by

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

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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ mfderiv[range ↑I] ↑(extChartAt I x).symm y ∘SL mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))

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
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
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' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
e✝ e : E ≃L[𝕜] F
x : M
⊢ ↑(extChartAt (I.transContinuousLinearEquiv e) x).symm (↑(extChartAt (I.transContinuousLinearEquiv e) x) x) ∈
    ⇑(Equiv.refl M).symm ⁻¹' (extChartAt I ((Equiv.refl M).symm x)).source

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.SMul

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹¹ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝⁸ : TopologicalSpace H''
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H' M
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H'' N
n : ℕ∞ω
⊢ ContMDiff (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, E)) 𝓘(𝕜, 𝕜 × E) n id

Tactic:
by

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

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
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
this : y = ↑(extChartAt I x).symm (↑(extChartAt I x) y)
⊢ y ∈ (extChartAt I x).source

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
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
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' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
e✝ e : E ≃L[𝕜] F
x : M
⊢ ContMDiffAt (I.transContinuousLinearEquiv e) I n (⇑(Equiv.refl M).symm) 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
s : Set M
z : M
F' : Type u_21
inst✝¹ : NormedCommRing F'
inst✝ : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivAt[s] p z p'
hq : HasMFDerivAt[s] q z q'
⊢ HasMFDerivAt[s] (p * q) z (p z • q' + q z • p')

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.SMul

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹¹ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝⁸ : TopologicalSpace H''
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H' M
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H'' N
n : ℕ∞ω
⊢ ContMDiff (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, E)) 𝓘(𝕜, E) n fun p ↦ p.1 • p.2

Tactic:
by

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

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
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) ∘SL mfderiv% ↑(extChartAt I x) y =
    ContinuousLinearMap.id 𝕜 (TangentSpace I y)

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
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
⊢ ⇑(sumComm I M n M') ∘ Sum.inl = Sum.inr

Tactic:
by

Goal state after: