Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

Goal state before:
pp: 𝕜 : 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
F : Type u_5
inst✝²² : NormedAddCommGroup F
inst✝²¹ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝²⁰ : TopologicalSpace (TotalSpace F V)
inst✝¹⁹ : (x : M) → AddCommGroup (V x)
inst✝¹⁸ : (x : M) → Module 𝕜 (V x)
inst✝¹⁷ : (x : M) → TopologicalSpace (V x)
inst✝¹⁶ : FiberBundle F V
F' : Type u_7
inst✝¹⁵ : NormedAddCommGroup F'
inst✝¹⁴ : NormedSpace 𝕜 F'
V' : M → Type u_8
inst✝¹³ : TopologicalSpace (TotalSpace F' V')
inst✝¹² : (x : M) → AddCommGroup (V' x)
inst✝¹¹ : (x : M) → Module 𝕜 (V' x)
inst✝¹⁰ : (x : M) → TopologicalSpace (V' x)
inst✝⁹ : FiberBundle F' V'
A : Type u_9
inst✝⁸ : AddCommGroup A
inst✝⁷ : Module 𝕜 A
inst✝⁶ : VectorBundle 𝕜 F V
inst✝⁵ : VectorBundle 𝕜 F' V'
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : FiniteDimensional 𝕜 F
inst✝² : FiniteDimensional 𝕜 F'
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : ContMDiffVectorBundle 1 F' V' I
Φ : ((x : M) → V x) → ((x : M) → V' x) → A
x : M
hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x ↦ Φ x τ) x
hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (fun x ↦ Φ σ x) x
σ σ' : (x : M) → V x
τ τ' : (x : M) → V' x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hτ : MDiffAt (T% τ) x
hτ' : MDiffAt (T% τ') x
hσσ' : σ x = σ' x
hττ' : τ x = τ' x
⊢ Φ σ τ = Φ σ' τ

pp: 𝕜 : 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
F : Type u_5
inst✝²² : NormedAddCommGroup F
inst✝²¹ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝²⁰ : TopologicalSpace (TotalSpace F V)
inst✝¹⁹ : (x : M) → AddCommGroup (V x)
inst✝¹⁸ : (x : M) → Module 𝕜 (V x)
inst✝¹⁷ : (x : M) → TopologicalSpace (V x)
inst✝¹⁶ : FiberBundle F V
F' : Type u_7
inst✝¹⁵ : NormedAddCommGroup F'
inst✝¹⁴ : NormedSpace 𝕜 F'
V' : M → Type u_8
inst✝¹³ : TopologicalSpace (TotalSpace F' V')
inst✝¹² : (x : M) → AddCommGroup (V' x)
inst✝¹¹ : (x : M) → Module 𝕜 (V' x)
inst✝¹⁰ : (x : M) → TopologicalSpace (V' x)
inst✝⁹ : FiberBundle F' V'
A : Type u_9
inst✝⁸ : AddCommGroup A
inst✝⁷ : Module 𝕜 A
inst✝⁶ : VectorBundle 𝕜 F V
inst✝⁵ : VectorBundle 𝕜 F' V'
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : FiniteDimensional 𝕜 F
inst✝² : FiniteDimensional 𝕜 F'
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : ContMDiffVectorBundle 1 F' V' I
Φ : ((x : M) → V x) → ((x : M) → V' x) → A
x : M
hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x ↦ Φ x τ) x
hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (fun x ↦ Φ σ x) x
σ σ' : (x : M) → V x
τ τ' : (x : M) → V' x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hτ : MDiffAt (T% τ) x
hτ' : MDiffAt (T% τ') x
hσσ' : σ x = σ' x
hττ' : τ x = τ' x
⊢ Φ σ' τ = Φ σ' τ'

Tactic:
· exact (hΦ₁ _ hτ).pointwise hσ hσ' hσσ'

Goal state after:
𝕜 : 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
F : Type u_5
inst✝²² : NormedAddCommGroup F
inst✝²¹ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝²⁰ : TopologicalSpace (TotalSpace F V)
inst✝¹⁹ : (x : M) → AddCommGroup (V x)
inst✝¹⁸ : (x : M) → Module 𝕜 (V x)
inst✝¹⁷ : (x : M) → TopologicalSpace (V x)
inst✝¹⁶ : FiberBundle F V
F' : Type u_7
inst✝¹⁵ : NormedAddCommGroup F'
inst✝¹⁴ : NormedSpace 𝕜 F'
V' : M → Type u_8
inst✝¹³ : TopologicalSpace (TotalSpace F' V')
inst✝¹² : (x : M) → AddCommGroup (V' x)
inst✝¹¹ : (x : M) → Module 𝕜 (V' x)
inst✝¹⁰ : (x : M) → TopologicalSpace (V' x)
inst✝⁹ : FiberBundle F' V'
A : Type u_9
inst✝⁸ : AddCommGroup A
inst✝⁷ : Module 𝕜 A
inst✝⁶ : VectorBundle 𝕜 F V
inst✝⁵ : VectorBundle 𝕜 F' V'
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : FiniteDimensional 𝕜 F
inst✝² : FiniteDimensional 𝕜 F'
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : ContMDiffVectorBundle 1 F' V' I
Φ : ((x : M) → V x) → ((x : M) → V' x) → A
x : M
hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x ↦ Φ x τ) x
hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (fun x ↦ Φ σ x) x
σ σ' : (x : M) → V x
τ τ' : (x : M) → V' x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hτ : MDiffAt (T% τ) x
hτ' : MDiffAt (T% τ') x
hσσ' : σ x = σ' x
hττ' : τ x = τ' x
⊢ Φ σ' τ = Φ σ' τ'