-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
/-- A vector field on a vector space is `C^n` in the manifold sense iff it is `C^n` in the vector
space sense. -/
lemma contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt
    {V : Π (x : E), TangentSpace 𝓘(𝕜, E) x} {n : ℕ∞} {s : Set E} {x : E} :
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent n (fun x ↦ (V x : TangentBundle 𝓘(𝕜, E) E)) s x ↔
      ContDiffWithinAt 𝕜 n V s x

Proof state:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
x : E
h : ContDiffWithinAt 𝕜 (↑n) V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (↑n) (fun x => { proj := x, snd := V x }.proj) s x ∧
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (↑n)
      (fun x_1 =>
        (↑(trivializationAt E (TangentSpace 𝓘(𝕜, E)) { proj := x, snd := V x }.proj) { proj := x_1, snd := V x_1 }).2)
      s x

Tactic:
refine ⟨contMDiffWithinAt_id, ?_⟩

Result:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
x : E
h : ContDiffWithinAt 𝕜 (↑n) V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (↑n)
    (fun x_1 =>
      (↑(trivializationAt E (TangentSpace 𝓘(𝕜, E)) { proj := x, snd := V x }.proj) { proj := x_1, snd := V x_1 }).2)
    s x

Proof state:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
x : E
h : ContDiffWithinAt 𝕜 (↑n) V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (↑n) (fun x => { proj := x, snd := V x }) s x

Tactic:
apply (Bundle.contMDiffWithinAt_totalSpace _).2

Result:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
x : E
h : ContDiffWithinAt 𝕜 (↑n) V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (↑n) (fun x => { proj := x, snd := V x }.proj) s x ∧
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (↑n)
      (fun x_1 =>
        (↑(trivializationAt E (TangentSpace 𝓘(𝕜, E)) { proj := x, snd := V x }.proj) { proj := x_1, snd := V x_1 }).2)
      s x

Proof state:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
x : E
h : ContDiffWithinAt 𝕜 (↑n) V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (↑n)
    (fun x_1 =>
      (↑(trivializationAt E (TangentSpace 𝓘(𝕜, E)) { proj := x, snd := V x }.proj) { proj := x_1, snd := V x_1 }).2)
    s x

Tactic:
convert h.contMDiffWithinAt with y

Result:
case h.e'_22.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
x : E
h : ContDiffWithinAt 𝕜 (↑n) V s x
y : E
⊢ (↑(trivializationAt E (TangentSpace 𝓘(𝕜, E)) { proj := x, snd := V x }.proj) { proj := y, snd := V y }).2 = V y

Proof state:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
x : E
h : ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (↑n) (fun x => { proj := x, snd := V x }) s x
⊢ ContDiffWithinAt 𝕜 (↑n) V s x

Tactic:
exact ContMDiffWithinAt.contDiffWithinAt <|
  (contMDiff_snd_tangentBundle_modelSpace E 𝓘(𝕜, E)).contMDiffAt.comp_contMDiffWithinAt _ h

Result:
no goals

Proof state:
case h.e'_22.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
x : E
h : ContDiffWithinAt 𝕜 (↑n) V s x
y : E
⊢ (↑(trivializationAt E (TangentSpace 𝓘(𝕜, E)) { proj := x, snd := V x }.proj) { proj := y, snd := V y }).2 = V y

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
x : E
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (↑n) (fun x => { proj := x, snd := V x }) s x ↔
    ContDiffWithinAt 𝕜 (↑n) V s x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
x : E
h : ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (↑n) (fun x => { proj := x, snd := V x }) s x
⊢ ContDiffWithinAt 𝕜 (↑n) V s x

case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
x : E
h : ContDiffWithinAt 𝕜 (↑n) V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (↑n) (fun x => { proj := x, snd := V x }) s x