awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
inst_16 : CompleteSpace 𝕜
inst_17 : FiniteDimensional 𝕜 F
inst_18 : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
x_mem : x ∈ t.baseSet
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5) 𝕜 F := Basis.ofVectorSpace 𝕜 F
s : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5) → (x : M) → V x := t.localFrame (V := V) b
c : (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)) →
  (x : M) → LinearMap.{u_1, u_1, u_6, u_1} (RingHom.id 𝕜) (V x) 𝕜 :=
  Trivialization.localFrame_coeff I (V := V) t b
hs : ∀ (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)), MDiffAt (T% s) x
hc :
  ∀ {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x) (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)),
    MDiffAt
        ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜) (c i) :
              ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
            (a : (x : M) → V x) → M → 𝕜)
          σ)
      x
hΦ_eq :
  ∀ {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x),
    Φ σ =
      Φ fun (x' : M) ↦
        ∑ i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5),
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((c i x' : (a : V x') → 𝕜) (σ x') : 𝕜) (s i x')
⊢ ∀ (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)),
    (MDiffAt fun (x : M) ↦ ⟨x, HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((c i x : (a : V x) → 𝕜) (σ x) : 𝕜) (s i x)⟩) x

Tactic:
fun i ↦ (hc hσ i).smul_section (hs i)

Premises used: MDifferentiableAt.smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
inst_16 : CompleteSpace 𝕜
inst_17 : FiniteDimensional 𝕜 F
inst_18 : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
x_mem : x ∈ t.baseSet
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5) 𝕜 F := Basis.ofVectorSpace 𝕜 F
s : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5) → (x : M) → V x := t.localFrame (V := V) b
c : (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)) →
  (x : M) → LinearMap.{u_1, u_1, u_6, u_1} (RingHom.id 𝕜) (V x) 𝕜 :=
  Trivialization.localFrame_coeff I (V := V) t b
hs : ∀ (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)), MDiffAt (T% s) x
hc :
  ∀ {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x) (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)),
    MDiffAt
        ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜) (c i) :
              ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
            (a : (x : M) → V x) → M → 𝕜)
          σ)
      x
hΦ_eq :
  ∀ {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x),
    Φ σ =
      Φ fun (x' : M) ↦
        ∑ i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5),
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((c i x' : (a : V x') → 𝕜) (σ x') : 𝕜) (s i x')
⊢ ∀ (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)),
    (MDiffAt fun (x : M) ↦ ⟨x, HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((c i x : (a : V x) → 𝕜) (σ x) : 𝕜) (s i x)⟩) x

Tactic:
exact fun i ↦ (hc hσ i).smul_section (hs i)

Premises used: MDifferentiableAt.smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
F' : Type u_7
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
V' : M → Type u_8
inst_15 : TopologicalSpace (TotalSpace F' V')
inst_16 : (x : M) → AddCommGroup (V' x)
inst_17 : (x : M) → Module.{u_1, u_8} 𝕜 (V' x)
inst_18 : (x : M) → TopologicalSpace (V' x)
inst_19 : FiberBundle F' V'
A : Type u_9
inst_20 : AddCommGroup A
inst_21 : Module 𝕜 A
inst_22 : VectorBundle 𝕜 F V
inst_23 : VectorBundle 𝕜 F' V'
inst_24 : CompleteSpace 𝕜
inst_25 : FiniteDimensional 𝕜 F
inst_26 : FiniteDimensional 𝕜 F'
inst_27 : ContMDiffVectorBundle 1 F V I
inst_28 : 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.{u_1, u_2, u_3, u_4, u_5, u_6, u_9} I F (V := V) (A := A) (fun (x : (x : M) → V x) ↦ Φ x τ) x
hΦ₂ :
  ∀ (σ : (x : M) → V x),
    MDiffAt (T% σ) x →
      TensorialAt.{u_1, u_2, u_3, u_4, u_7, u_8, u_9} I F' (V := V') (A := A) (fun (x : (x : M) → V' 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
trans : Φ σ τ = Φ σ' τ
trans₁ : Φ σ' τ = Φ σ' τ'
⊢ Φ σ τ = Φ σ' τ'

Tactic:
trans Φ σ' τ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
F' : Type u_7
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
V' : M → Type u_8
inst_15 : TopologicalSpace (TotalSpace F' V')
inst_16 : (x : M) → AddCommGroup (V' x)
inst_17 : (x : M) → Module.{u_1, u_8} 𝕜 (V' x)
inst_18 : (x : M) → TopologicalSpace (V' x)
inst_19 : FiberBundle F' V'
A : Type u_9
inst_20 : AddCommGroup A
inst_21 : Module 𝕜 A
inst_22 : VectorBundle 𝕜 F V
inst_23 : VectorBundle 𝕜 F' V'
inst_24 : CompleteSpace 𝕜
inst_25 : FiniteDimensional 𝕜 F
inst_26 : FiniteDimensional 𝕜 F'
inst_27 : ContMDiffVectorBundle 1 F V I
inst_28 : 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.{u_1, u_2, u_3, u_4, u_5, u_6, u_9} I F (V := V) (A := A) (fun (x : (x : M) → V x) ↦ Φ x τ) x
hΦ₂ :
  ∀ (σ : (x : M) → V x),
    MDiffAt (T% σ) x →
      TensorialAt.{u_1, u_2, u_3, u_4, u_7, u_8, u_9} I F' (V := V') (A := A) (fun (x : (x : M) → V' 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:
(hΦ₁ _ hτ).pointwise hσ hσ' hσσ'

Premises used: TensorialAt.pointwise
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
F' : Type u_7
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
V' : M → Type u_8
inst_15 : TopologicalSpace (TotalSpace F' V')
inst_16 : (x : M) → AddCommGroup (V' x)
inst_17 : (x : M) → Module.{u_1, u_8} 𝕜 (V' x)
inst_18 : (x : M) → TopologicalSpace (V' x)
inst_19 : FiberBundle F' V'
A : Type u_9
inst_20 : AddCommGroup A
inst_21 : Module 𝕜 A
inst_22 : VectorBundle 𝕜 F V
inst_23 : VectorBundle 𝕜 F' V'
inst_24 : CompleteSpace 𝕜
inst_25 : FiniteDimensional 𝕜 F
inst_26 : FiniteDimensional 𝕜 F'
inst_27 : ContMDiffVectorBundle 1 F V I
inst_28 : 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.{u_1, u_2, u_3, u_4, u_5, u_6, u_9} I F (V := V) (A := A) (fun (x : (x : M) → V x) ↦ Φ x τ) x
hΦ₂ :
  ∀ (σ : (x : M) → V x),
    MDiffAt (T% σ) x →
      TensorialAt.{u_1, u_2, u_3, u_4, u_7, u_8, u_9} I F' (V := V') (A := A) (fun (x : (x : M) → V' 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σσ'

Premises used: TensorialAt.pointwise
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
F' : Type u_7
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
V' : M → Type u_8
inst_15 : TopologicalSpace (TotalSpace F' V')
inst_16 : (x : M) → AddCommGroup (V' x)
inst_17 : (x : M) → Module.{u_1, u_8} 𝕜 (V' x)
inst_18 : (x : M) → TopologicalSpace (V' x)
inst_19 : FiberBundle F' V'
A : Type u_9
inst_20 : AddCommGroup A
inst_21 : Module 𝕜 A
inst_22 : VectorBundle 𝕜 F V
inst_23 : VectorBundle 𝕜 F' V'
inst_24 : CompleteSpace 𝕜
inst_25 : FiniteDimensional 𝕜 F
inst_26 : FiniteDimensional 𝕜 F'
inst_27 : ContMDiffVectorBundle 1 F V I
inst_28 : 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.{u_1, u_2, u_3, u_4, u_5, u_6, u_9} I F (V := V) (A := A) (fun (x : (x : M) → V x) ↦ Φ x τ) x
hΦ₂ :
  ∀ (σ : (x : M) → V x),
    MDiffAt (T% σ) x →
      TensorialAt.{u_1, u_2, u_3, u_4, u_7, u_8, u_9} I F' (V := V') (A := A) (fun (x : (x : M) → V' 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:
(hΦ₂ _ hσ').pointwise hτ hτ' hττ'

Premises used: TensorialAt.pointwise
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
F' : Type u_7
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
V' : M → Type u_8
inst_15 : TopologicalSpace (TotalSpace F' V')
inst_16 : (x : M) → AddCommGroup (V' x)
inst_17 : (x : M) → Module.{u_1, u_8} 𝕜 (V' x)
inst_18 : (x : M) → TopologicalSpace (V' x)
inst_19 : FiberBundle F' V'
A : Type u_9
inst_20 : AddCommGroup A
inst_21 : Module 𝕜 A
inst_22 : VectorBundle 𝕜 F V
inst_23 : VectorBundle 𝕜 F' V'
inst_24 : CompleteSpace 𝕜
inst_25 : FiniteDimensional 𝕜 F
inst_26 : FiniteDimensional 𝕜 F'
inst_27 : ContMDiffVectorBundle 1 F V I
inst_28 : 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.{u_1, u_2, u_3, u_4, u_5, u_6, u_9} I F (V := V) (A := A) (fun (x : (x : M) → V x) ↦ Φ x τ) x
hΦ₂ :
  ∀ (σ : (x : M) → V x),
    MDiffAt (T% σ) x →
      TensorialAt.{u_1, u_2, u_3, u_4, u_7, u_8, u_9} I F' (V := V') (A := A) (fun (x : (x : M) → V' 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ττ'

Premises used: TensorialAt.pointwise
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
F' : Type u_7
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
V' : M → Type u_8
inst_15 : TopologicalSpace (TotalSpace F' V')
inst_16 : (x : M) → AddCommGroup (V' x)
inst_17 : (x : M) → Module.{u_1, u_8} 𝕜 (V' x)
inst_18 : (x : M) → TopologicalSpace (V' x)
inst_19 : FiberBundle F' V'
A : Type u_9
inst_20 : AddCommGroup A
inst_21 : Module 𝕜 A
Φ_1 : ((x : M) → V x) → A
x_1 : M
inst_22 : VectorBundle 𝕜 F V
inst_23 : VectorBundle 𝕜 F' V'
inst_24 : CompleteSpace 𝕜
inst_25 : FiniteDimensional 𝕜 F
inst_26 : FiniteDimensional 𝕜 F'
inst_27 : ContMDiffVectorBundle 1 F V I
inst_28 : ContMDiffVectorBundle 1 F' V' I
inst_29 : TopologicalSpace A
inst_30 : IsTopologicalAddGroup A
inst_31 : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : IsTopologicalAddGroup.{u_6} (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
v₁ v₂ : V x
rw : Φ (extend F (E := V) (v₁ + v₂)) = Φ (extend F (E := V) v₁ + extend F (E := V) v₂)
⊢ Φ (extend F (E := V) (v₁ + v₂)) = Φ (extend F (E := V) v₁) + Φ (extend F (E := V) v₂)

Tactic:
rw [← hΦ.add (mdifferentiableAt_extend ..) (mdifferentiableAt_extend ..)]

Premises used: FiberBundle.mdifferentiableAt_extend, TensorialAt.add
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
F' : Type u_7
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
V' : M → Type u_8
inst_15 : TopologicalSpace (TotalSpace F' V')
inst_16 : (x : M) → AddCommGroup (V' x)
inst_17 : (x : M) → Module.{u_1, u_8} 𝕜 (V' x)
inst_18 : (x : M) → TopologicalSpace (V' x)
inst_19 : FiberBundle F' V'
A : Type u_9
inst_20 : AddCommGroup A
inst_21 : Module 𝕜 A
Φ_1 : ((x : M) → V x) → A
x_1 : M
inst_22 : VectorBundle 𝕜 F V
inst_23 : VectorBundle 𝕜 F' V'
inst_24 : CompleteSpace 𝕜
inst_25 : FiniteDimensional 𝕜 F
inst_26 : FiniteDimensional 𝕜 F'
inst_27 : ContMDiffVectorBundle 1 F V I
inst_28 : ContMDiffVectorBundle 1 F' V' I
inst_29 : TopologicalSpace A
inst_30 : IsTopologicalAddGroup A
inst_31 : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : IsTopologicalAddGroup.{u_6} (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
v₁ v₂ : V x
apply : extend F (E := V) (v₁ + v₂) x = (extend F (E := V) v₁ + extend F (E := V) v₂) x
⊢ Φ (extend F (E := V) (v₁ + v₂)) = Φ (extend F (E := V) v₁ + extend F (E := V) v₂)

Tactic:
apply hΦ.pointwise (mdifferentiableAt_extend ..) <|
        mdifferentiableAt_add_section (mdifferentiableAt_extend ..) (mdifferentiableAt_extend ..)

Premises used: TensorialAt.pointwise, mdifferentiableAt_add_section, FiberBundle.mdifferentiableAt_extend
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
F' : Type u_7
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
V' : M → Type u_8
inst_15 : TopologicalSpace (TotalSpace F' V')
inst_16 : (x : M) → AddCommGroup (V' x)
inst_17 : (x : M) → Module.{u_1, u_8} 𝕜 (V' x)
inst_18 : (x : M) → TopologicalSpace (V' x)
inst_19 : FiberBundle F' V'
A : Type u_9
inst_20 : AddCommGroup A
inst_21 : Module 𝕜 A
Φ_1 : ((x : M) → V x) → A
x_1 : M
inst_22 : VectorBundle 𝕜 F V
inst_23 : VectorBundle 𝕜 F' V'
inst_24 : CompleteSpace 𝕜
inst_25 : FiniteDimensional 𝕜 F
inst_26 : FiniteDimensional 𝕜 F'
inst_27 : ContMDiffVectorBundle 1 F V I
inst_28 : ContMDiffVectorBundle 1 F' V' I
inst_29 : TopologicalSpace A
inst_30 : IsTopologicalAddGroup A
inst_31 : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : IsTopologicalAddGroup.{u_6} (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
v₁ v₂ : V x
⊢ extend F (E := V) (v₁ + v₂) x = (extend F (E := V) v₁ + extend F (E := V) v₂) x

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
F' : Type u_7
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
V' : M → Type u_8
inst_15 : TopologicalSpace (TotalSpace F' V')
inst_16 : (x : M) → AddCommGroup (V' x)
inst_17 : (x : M) → Module.{u_1, u_8} 𝕜 (V' x)
inst_18 : (x : M) → TopologicalSpace (V' x)
inst_19 : FiberBundle F' V'
A : Type u_9
inst_20 : AddCommGroup A
inst_21 : Module 𝕜 A
Φ_1 : ((x : M) → V x) → A
x_1 : M
inst_22 : VectorBundle 𝕜 F V
inst_23 : VectorBundle 𝕜 F' V'
inst_24 : CompleteSpace 𝕜
inst_25 : FiniteDimensional 𝕜 F
inst_26 : FiniteDimensional 𝕜 F'
inst_27 : ContMDiffVectorBundle 1 F V I
inst_28 : ContMDiffVectorBundle 1 F' V' I
inst_29 : TopologicalSpace A
inst_30 : IsTopologicalAddGroup A
inst_31 : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : IsTopologicalAddGroup.{u_6} (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
c : 𝕜
v : V x
dsimp : Φ (extend F (E := V) (c • v)) = c • Φ (extend F (E := V) v)
⊢ Φ (extend F (E := V) (c • v)) = HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (Φ (extend F (E := V) v))

Tactic:
dsimp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
F' : Type u_7
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
V' : M → Type u_8
inst_15 : TopologicalSpace (TotalSpace F' V')
inst_16 : (x : M) → AddCommGroup (V' x)
inst_17 : (x : M) → Module.{u_1, u_8} 𝕜 (V' x)
inst_18 : (x : M) → TopologicalSpace (V' x)
inst_19 : FiberBundle F' V'
A : Type u_9
inst_20 : AddCommGroup A
inst_21 : Module 𝕜 A
Φ_1 : ((x : M) → V x) → A
x_1 : M
inst_22 : VectorBundle 𝕜 F V
inst_23 : VectorBundle 𝕜 F' V'
inst_24 : CompleteSpace 𝕜
inst_25 : FiniteDimensional 𝕜 F
inst_26 : FiniteDimensional 𝕜 F'
inst_27 : ContMDiffVectorBundle 1 F V I
inst_28 : ContMDiffVectorBundle 1 F' V' I
inst_29 : TopologicalSpace A
inst_30 : IsTopologicalAddGroup A
inst_31 : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : IsTopologicalAddGroup.{u_6} (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
c : 𝕜
v : V x
rw : Φ (extend F (E := V) (c • v)) = Φ (HSMul.hSMul (α := M → 𝕜) (fun (x : M) ↦ c) (extend F (E := V) v))
⊢ Φ (extend F (E := V) (c • v)) = c • Φ (extend F (E := V) v)

Tactic:
rw [← hΦ.smul (f := fun _ ↦ c) (mdifferentiable_const ..) (mdifferentiableAt_extend ..)]

Premises used: mdifferentiable_const, FiberBundle.mdifferentiableAt_extend, TensorialAt.smul