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 : ℕ∞ω
M' : Type u_13
inst✝⁷ : TopologicalSpace M'
inst✝⁶ : ChartedSpace H M'
M'' : Type u_14
inst✝⁵ : TopologicalSpace M''
inst✝⁴ : ChartedSpace H M''
N : Type u_15
J✝ : Type u_16
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace H N'
⊢ ContMDiff I I n ⇑(Equiv.sumAssoc M M' M'').symm

Tactic:
apply ContMDiff.sumElim

Goal state after:
case hf
𝕜 : 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 : ℕ∞ω
M' : Type u_13
inst✝⁷ : TopologicalSpace M'
inst✝⁶ : ChartedSpace H M'
M'' : Type u_14
inst✝⁵ : TopologicalSpace M''
inst✝⁴ : ChartedSpace H M''
N : Type u_15
J✝ : Type u_16
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace H N'
⊢ ContMDiff I I n (Sum.inl ∘ Sum.inl)

case hg
𝕜 : 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 : ℕ∞ω
M' : Type u_13
inst✝⁷ : TopologicalSpace M'
inst✝⁶ : ChartedSpace H M'
M'' : Type u_14
inst✝⁵ : TopologicalSpace M''
inst✝⁴ : ChartedSpace H M''
N : Type u_15
J✝ : Type u_16
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace H N'
⊢ ContMDiff I I n (Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr)