-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
lemma contMDiff_of_contMDiff_inl {f : M → N}
    (h : ContMDiff I J n ((@Sum.inl N N') ∘ f)) : ContMDiff I J n f

Proof state:
𝕜 : 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
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
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
f : M → N
h : ContMDiff I J n (Sum.inl ∘ f)
a✝ : Nontrivial N
inhabited_h : Inhabited N
⊢ ContMDiff I J n f

Tactic:
let aux : N ⊕ N' → N := Sum.elim (@id N) (fun _ ↦ inhabited_h.default)

Result:
𝕜 : 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
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
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
f : M → N
h : ContMDiff I J n (Sum.inl ∘ f)
a✝ : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun x => default
⊢ ContMDiff I J n f

Proof state:
𝕜 : 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
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
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J n (Sum.inl ∘ f) univ
a✝ : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun x => default
this : aux ∘ Sum.inl ∘ f = f
⊢ ContMDiffOn I J n (aux ∘ Sum.inl ∘ f) univ

Tactic:
apply (contMDiff_id.sumElim contMDiff_const).contMDiffOn (s := @Sum.inl N N' '' univ).comp h

Result:
𝕜 : 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
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
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J n (Sum.inl ∘ f) univ
a✝ : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun x => default
this : aux ∘ Sum.inl ∘ f = f
⊢ univ ⊆ Sum.inl ∘ f ⁻¹' (Sum.inl '' univ)