Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: case fst
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace 𝕜 E
inst✝¹⁷ : TopologicalSpace H
inst✝¹⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
inst✝¹³ : TopologicalSpace H'
inst✝¹² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : ChartedSpace H' M'
G : Type u_8
G' : Type u_9
F : Type u_10
F' : Type u_11
N : Type u_12
N' : Type u_13
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : NormedAddCommGroup F'
inst✝⁶ : NormedSpace 𝕜 F'
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace N
inst✝³ : TopologicalSpace G'
inst✝² : TopologicalSpace N'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
inst✝¹ : ChartedSpace G N
inst✝ : ChartedSpace G' N'
f : M → N
g : M' → N'
x : M
x' : M'
p : E × E'
⊢ (writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) p).1 =
    (Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g) p).1

pp: case snd
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace 𝕜 E
inst✝¹⁷ : TopologicalSpace H
inst✝¹⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
inst✝¹³ : TopologicalSpace H'
inst✝¹² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : ChartedSpace H' M'
G : Type u_8
G' : Type u_9
F : Type u_10
F' : Type u_11
N : Type u_12
N' : Type u_13
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : NormedAddCommGroup F'
inst✝⁶ : NormedSpace 𝕜 F'
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace N
inst✝³ : TopologicalSpace G'
inst✝² : TopologicalSpace N'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
inst✝¹ : ChartedSpace G N
inst✝ : ChartedSpace G' N'
f : M → N
g : M' → N'
x : M
x' : M'
p : E × E'
⊢ (writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) p).2 =
    (Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g) p).2

Tactic:
<;>

Goal state after:
case fst
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace 𝕜 E
inst✝¹⁷ : TopologicalSpace H
inst✝¹⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
inst✝¹³ : TopologicalSpace H'
inst✝¹² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : ChartedSpace H' M'
G : Type u_8
G' : Type u_9
F : Type u_10
F' : Type u_11
N : Type u_12
N' : Type u_13
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : NormedAddCommGroup F'
inst✝⁶ : NormedSpace 𝕜 F'
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace N
inst✝³ : TopologicalSpace G'
inst✝² : TopologicalSpace N'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
inst✝¹ : ChartedSpace G N
inst✝ : ChartedSpace G' N'
f : M → N
g : M' → N'
x : M
x' : M'
p : E × E'
⊢ (writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) p).1 =
    (Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g) p).1

case snd
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace 𝕜 E
inst✝¹⁷ : TopologicalSpace H
inst✝¹⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
inst✝¹³ : TopologicalSpace H'
inst✝¹² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : ChartedSpace H' M'
G : Type u_8
G' : Type u_9
F : Type u_10
F' : Type u_11
N : Type u_12
N' : Type u_13
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : NormedAddCommGroup F'
inst✝⁶ : NormedSpace 𝕜 F'
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace N
inst✝³ : TopologicalSpace G'
inst✝² : TopologicalSpace N'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
inst✝¹ : ChartedSpace G N
inst✝ : ChartedSpace G' N'
f : M → N
g : M' → N'
x : M
x' : M'
p : E × E'
⊢ (writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) p).2 =
    (Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g) p).2