-- Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
theorem tangentMap_tangentBundle_pure [Is : IsManifold I 1 M]
    (p : TangentBundle I M) :
    tangentMap I I.tangent (zeroSection E (TangentSpace I)) p = ⟨⟨p.proj, 0⟩, ⟨p.2, 0⟩⟩

Proof state:
case mk.e_a.refine_1
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x
B :
  (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)
y : E
hy : y ∈ range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target
⊢ (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm y))), 0) = (y, 0)

Tactic:
simp only [mfld_simps] at hy

Result:
case mk.e_a.refine_1
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x
B :
  (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)
y : E
hy : y ∈ range ↑I ∧ ↑I.symm y ∈ (chartAt H x).target
⊢ (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm y))), 0) = (y, 0)

Proof state:
case hs
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x
⊢ UniqueDiffWithinAt 𝕜 (range ↑I) (↑I (↑(chartAt H x) x))

Tactic:
exact ModelWithCorners.uniqueDiffWithinAt_image I

Result:
no goals

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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))

Tactic:
apply IsOpen.mem_nhds

Result:
case hs
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ IsOpen (↑I.symm ⁻¹' (chartAt H x).target)

case 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ ↑I (↑(chartAt H x) x) ∈ ↑I.symm ⁻¹' (chartAt H x).target

Proof state:
case mk.e_a.refine_2
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x
B :
  (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)
⊢ (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm (↑I (↑(chartAt H x) x))))), 0) =
    (↑I (↑(chartAt H x) x), 0)

Tactic:
simp only [Prod.mk.inj_iff, mfld_simps]

Result:
no goals

Proof state:
case mk
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x
B :
  (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)
⊢ (fderivWithin 𝕜 (fun x_1 => (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm x_1))), 0))
        (range ↑I) (↑I (↑(ChartedSpace.chartAt x) x)))
      v =
    (v, 0)

Tactic:
rw [← fderivWithin_inter N, ← B]

Result:
case mk
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x
B :
  (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)
⊢ (fderivWithin 𝕜 (fun x_1 => (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm x_1))), 0))
        (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x)))
      v =
    (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v

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
Is : IsManifold I 1 M
p : TangentBundle I M
⊢ tangentMap I I.tangent (zeroSection E (TangentSpace I)) p =
    { proj := { proj := p.proj, snd := 0 }, snd := (p.snd, 0) }

Tactic:
rcases p with ⟨x, v⟩

Result:
case mk
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ tangentMap I I.tangent (zeroSection E (TangentSpace I)) { proj := x, snd := v } =
    { proj := { proj := { proj := x, snd := v }.proj, snd := 0 }, snd := ({ proj := x, snd := v }.snd, 0) }

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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x
⊢ ((fderiv 𝕜 (fun x' => x') (↑I (↑(chartAt H x) x))).prod (fderiv 𝕜 (fun x' => 0) (↑I (↑(chartAt H x) x)))) v = (v, 0)

Tactic:
simp

Result:
no goals