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

Goal state before:
pp: case pos.hs
𝕜 : 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'
f f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDiffAt[s] f x
⊢ ↑(extChartAt I' (f₁ x)) ∘
      f₁ ∘ ↑(extChartAt I x).symm =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x]
    ↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm

pp: case hx
𝕜 : 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'
f f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDiffAt[s] f x
⊢ (↑(extChartAt I' (f₁ x)) ∘ f₁ ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) =
    (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)

Tactic:
;

Goal state after:
case pos.hs
𝕜 : 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'
f f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDiffAt[s] f x
⊢ ↑(extChartAt I' (f₁ x)) ∘
      f₁ ∘ ↑(extChartAt I x).symm =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x]
    ↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm

case hx
𝕜 : 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'
f f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDiffAt[s] f x
⊢ (↑(extChartAt I' (f₁ x)) ∘ f₁ ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) =
    (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) 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'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle (I.prod I') (M × M')
⊢ ⟨p.proj.1, (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.proj.1) (TangentSpace I' p.proj.2)) p.snd⟩ =
    ⟨p.proj.1, p.snd.1⟩

Tactic:
;

Goal state after:
𝕜 : 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'
p : TangentBundle (I.prod I') (M × M')
⊢ ⟨p.proj.1, (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.proj.1) (TangentSpace I' p.proj.2)) p.snd⟩ =
    ⟨p.proj.1, p.snd.1⟩
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'
s : Set (M × M')
proj✝ : M × M'
snd✝ : TangentSpace (I.prod I') proj✝
hs : UniqueMDiffAt[s] ⟨proj✝, snd✝⟩.proj
⊢ ⟨⟨proj✝, snd✝⟩.proj.1,
      (ContinuousLinearMap.fst 𝕜 (TangentSpace I ⟨proj✝, snd✝⟩.proj.1) (TangentSpace I' ⟨proj✝, snd✝⟩.proj.2))
        ⟨proj✝, snd✝⟩.snd⟩ =
    ⟨⟨proj✝, snd✝⟩.proj.1, ⟨proj✝, snd✝⟩.snd.1⟩

Tactic:
;

Goal state after:
𝕜 : 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'
s : Set (M × M')
proj✝ : M × M'
snd✝ : TangentSpace (I.prod I') proj✝
hs : UniqueMDiffAt[s] ⟨proj✝, snd✝⟩.proj
⊢ ⟨⟨proj✝, snd✝⟩.proj.1,
      (ContinuousLinearMap.fst 𝕜 (TangentSpace I ⟨proj✝, snd✝⟩.proj.1) (TangentSpace I' ⟨proj✝, snd✝⟩.proj.2))
        ⟨proj✝, snd✝⟩.snd⟩ =
    ⟨⟨proj✝, snd✝⟩.proj.1, ⟨proj✝, snd✝⟩.snd.1⟩
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

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'
f : M → M'
x : M
⊢ mfderiv% f x = mfderiv% f x

Tactic:
;

Goal state after:
𝕜 : 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'
f : M → M'
x : M
⊢ mfderiv% f x = mfderiv% f x
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
x₀ : M
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f univ x₀ ↔
    ContMDiffWithinAt IM IB n (fun x ↦ (f x).proj) univ x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E (f x₀).proj) (f x)).2) univ x₀

Tactic:
;

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
x₀ : M
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f univ x₀ ↔
    ContMDiffWithinAt IM IB n (fun x ↦ (f x).proj) univ x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E (f x₀).proj) (f x)).2) univ x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
⊢ ContMDiffWithinAt IB 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) a x₀ →
    ContMDiffWithinAt IB IB n (fun x ↦ x) a x₀

Tactic:
;

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
⊢ ContMDiffWithinAt IB 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) a x₀ →
    ContMDiffWithinAt IB IB n (fun x ↦ x) a x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
a✝ : ContMDiffWithinAt IB 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) a x₀
⊢ ContMDiffWithinAt IB IB n (fun x ↦ x) a x₀

Tactic:
;

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
a✝ : ContMDiffWithinAt IB 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) a x₀
⊢ ContMDiffWithinAt IB IB n (fun x ↦ x) a 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'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffAt[s] x
⊢ mfderiv% Prod.snd x = ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)

Tactic:
;

Goal state after:
𝕜 : 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'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffAt[s] x
⊢ mfderiv% Prod.snd x = ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
s : (x : B) → E x
x₀ : B
⊢ ContMDiffAt IB 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) x₀ →
    ContMDiffAt IB IB n (fun x ↦ x) x₀

Tactic:
;

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
s : (x : B) → E x
x₀ : B
⊢ ContMDiffAt IB 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) x₀ →
    ContMDiffAt IB IB n (fun x ↦ x) 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'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
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'
x : M
f : M → M' × N'
⊢ MDiffAt[univ] f x ↔ MDiffAt[univ] (Prod.fst ∘ f) x ∧ MDiffAt[univ] (Prod.snd ∘ f) x

Tactic:
;

Goal state after:
𝕜 : 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'
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'
x : M
f : M → M' × N'
⊢ MDiffAt[univ] f x ↔ MDiffAt[univ] (Prod.fst ∘ f) x ∧ MDiffAt[univ] (Prod.snd ∘ f) x
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
s : (x : B) → E x
x₀ : B
a✝ : ContMDiffAt IB 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) x₀
⊢ ContMDiffAt IB IB n (fun x ↦ x) x₀

Tactic:
;

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
s : (x : B) → E x
x₀ : B
a✝ : ContMDiffAt IB 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) x₀
⊢ ContMDiffAt IB IB n (fun x ↦ x) x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
⊢ ↑I '' ((↑i).symm ≫ₕ ↑j).source ⊆ range ↑I

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
⊢ ↑I '' ((↑i).symm ≫ₕ ↑j).source ⊆ range ↑I
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'
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'
s : Set (M × M')
p : M × M'
f : M → N
g : M' → N'
df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)
hf : HasMFDerivAt[Prod.fst '' s] f p.1 df
dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)
hg : HasMFDerivAt[Prod.snd '' s] g p.2 dg
p₀ : E × E'
hp₀ : (↑(chartAt H p.1).symm (↑I.symm p₀.1), ↑(chartAt H' p.2).symm (↑I'.symm p₀.2)) ∈ s
hp₁₁ : ∃ y, ↑I y = p₀.1
hp₁₂ : ∃ y, ↑I' y = p₀.2
⊢ ∃ x, (↑(chartAt H p.1).symm (↑I.symm p₀.1), x) ∈ s

Tactic:
;

Goal state after:
𝕜 : 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'
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'
s : Set (M × M')
p : M × M'
f : M → N
g : M' → N'
df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)
hf : HasMFDerivAt[Prod.fst '' s] f p.1 df
dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)
hg : HasMFDerivAt[Prod.snd '' s] g p.2 dg
p₀ : E × E'
hp₀ : (↑(chartAt H p.1).symm (↑I.symm p₀.1), ↑(chartAt H' p.2).symm (↑I'.symm p₀.2)) ∈ s
hp₁₁ : ∃ y, ↑I y = p₀.1
hp₁₂ : ∃ y, ↑I' y = p₀.2
⊢ ∃ x, (↑(chartAt H p.1).symm (↑I.symm p₀.1), x) ∈ s
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

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 : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hf : MDiffAt[s] f x
h : s ⊆ f ⁻¹' u
hg : MDiffAt[u] g (f x)
⊢ MDiffAt[s] (g ∘ f) x

Tactic:
;

Goal state after:
𝕜 : 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 : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hf : MDiffAt[s] f x
h : s ⊆ f ⁻¹' u
hg : MDiffAt[u] g (f x)
⊢ MDiffAt[s] (g ∘ f) x