-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
/-- In the tangent bundle to the model space, the second projection is `C^n`. -/
lemma contMDiff_snd_tangentBundle_modelSpace {n : ℕ∞} :
    ContMDiff I.tangent 𝓘(𝕜, E) n (fun (p : TangentBundle I H) ↦ p.2)

Proof state:
case h.e'_11.h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
e_10✝ : instTopologicalSpaceModelProd H E = instTopologicalSpaceProd
⊢ chartedSpaceSelf (ModelProd H E) = prodChartedSpace H H E E

case hg.convert_11
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
⊢ ChartedSpace H H

Tactic:
rw [chartedSpaceSelf_prod]

Result:
case h.e'_11.h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
e_10✝ : instTopologicalSpaceModelProd H E = instTopologicalSpaceProd
⊢ chartedSpaceSelf (ModelProd H E) = chartedSpaceSelf (H × E)

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
⊢ ContMDiff I.tangent 𝓘(𝕜, E) (↑n) (_root_.id Prod.snd ∘ ⇑(tangentBundleModelSpaceHomeomorph I))

Tactic:
apply ContMDiff.comp (I' := I.prod 𝓘(𝕜, E))

Result:
case hg
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
⊢ ContMDiff (I.prod 𝓘(𝕜, E)) 𝓘(𝕜, E) (↑n) (_root_.id Prod.snd)

case hf
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
⊢ ContMDiff I.tangent (I.prod 𝓘(𝕜, E)) ↑n ⇑(tangentBundleModelSpaceHomeomorph I)

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
⊢ ContMDiff I.tangent 𝓘(𝕜, E) ↑n fun p => p.snd

Tactic:
change ContMDiff I.tangent 𝓘(𝕜, E) n
  ((id Prod.snd : ModelProd H E → E) ∘ (tangentBundleModelSpaceHomeomorph I))

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
⊢ ContMDiff I.tangent 𝓘(𝕜, E) (↑n) (_root_.id Prod.snd ∘ ⇑(tangentBundleModelSpaceHomeomorph I))

Proof state:
case hf
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
⊢ ContMDiff I.tangent (I.prod 𝓘(𝕜, E)) ↑n ⇑(tangentBundleModelSpaceHomeomorph I)

Tactic:
exact contMDiff_tangentBundleModelSpaceHomeomorph

Result:
no goals

Proof state:
case h.e'_11.h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
e_10✝ : instTopologicalSpaceModelProd H E = instTopologicalSpaceProd
⊢ chartedSpaceSelf (ModelProd H E) = chartedSpaceSelf (H × E)

Tactic:
rfl

Result:
no goals

Proof state:
case hg
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
⊢ ContMDiff (I.prod 𝓘(𝕜, E)) 𝓘(𝕜, E) (↑n) (_root_.id Prod.snd)

Tactic:
convert contMDiff_snd

Result:
case h.e'_11.h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
e_10✝ : instTopologicalSpaceModelProd H E = instTopologicalSpaceProd
⊢ chartedSpaceSelf (ModelProd H E) = prodChartedSpace H H E E

case hg.convert_11
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
⊢ ChartedSpace H H