-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
lemma ContMDiff.sumElim {f : M → N} {g : M' → N}
    (hf : ContMDiff I J n f) (hg : ContMDiff I J n g) : ContMDiff I J n (Sum.elim f g)

Proof state:
case inl
𝕜 : 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_16
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝² : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt J (Sum.elim f g (Sum.inl x))) ∘ Sum.elim f g ∘ ↑(extChartAt I (Sum.inl x)).symm)
    (range ↑I) (↑(extChartAt I (Sum.inl x)) (Sum.inl x))

Tactic:
have : ContDiffWithinAt 𝕜 n ((extChartAt J (f x)) ∘ f ∘ (extChartAt I x).symm)
    (range I) ((extChartAt I (.inl x : M ⊕ M')) (Sum.inl x)) := by
  let hf' := hf x
  rw [contMDiffAt_iff] at hf'
  simpa using hf'.2

Result:
case inl
𝕜 : 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_16
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝² : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M
this :
  ContDiffWithinAt 𝕜 n (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inl x)) (Sum.inl x))
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt J (Sum.elim f g (Sum.inl x))) ∘ Sum.elim f g ∘ ↑(extChartAt I (Sum.inl x)).symm)
    (range ↑I) (↑(extChartAt I (Sum.inl x)) (Sum.inl x))

Proof state:
case inr
𝕜 : 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_16
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝² : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt J (Sum.elim f g (Sum.inr x))) ∘ Sum.elim f g ∘ ↑(extChartAt I (Sum.inr x)).symm)
    (range ↑I) (↑(extChartAt I (Sum.inr x)) (Sum.inr x))

Tactic:
have : ContDiffWithinAt 𝕜 n ((extChartAt J (g x)) ∘ g ∘ (extChartAt I x).symm)
    (range I) ((extChartAt I (.inr x : M ⊕ M')) (Sum.inr x)) := by
  let hg' := hg x
  rw [contMDiffAt_iff] at hg'
  simpa using hg'.2

Result:
case inr
𝕜 : 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_16
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝² : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n (↑(extChartAt J (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inr x)) (Sum.inr x))
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt J (Sum.elim f g (Sum.inr x))) ∘ Sum.elim f g ∘ ↑(extChartAt I (Sum.inr x)).symm)
    (range ↑I) (↑(extChartAt I (Sum.inr x)) (Sum.inr x))

Proof state:
case inr.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
M' : Type u_16
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝² : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n (↑(extChartAt J (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inr x)) (Sum.inr x))
⊢ (↑(extChartAt J (Sum.elim f g (Sum.inr x))) ∘ Sum.elim f g ∘ ↑(extChartAt I (Sum.inr x)).symm)
      (↑(extChartAt I (Sum.inr x)) (Sum.inr x)) =
    (↑(extChartAt J (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (↑(extChartAt I (Sum.inr x)) (Sum.inr x))

Tactic:
simp only [extChartAt, ChartedSpace.sum_chartAt_inr, Sum.elim_inr]

Result:
case inr.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
M' : Type u_16
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝² : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n (↑(extChartAt J (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inr x)) (Sum.inr x))
⊢ (↑((chartAt H' (g x)).extend J) ∘ Sum.elim f g ∘ ↑(((chartAt H x).lift_openEmbedding ⋯).extend I).symm)
      (↑(((chartAt H x).lift_openEmbedding ⋯).extend I) (Sum.inr x)) =
    (↑((chartAt H' (g x)).extend J) ∘ g ∘ ↑((chartAt H x).extend I).symm)
      (↑(((chartAt H x).lift_openEmbedding ⋯).extend I) (Sum.inr x))