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
⊢ ∀ {σ : (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')

Tactic:
have hΦ_eq {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x) :
      Φ σ = Φ (fun x' ↦ ∑ i, c i x' (σ x') • s i x') :=
    hΦ.local hσ
      (.sum_section fun i ↦ (hc hσ i).smul_section (hs i))
      (t.eventually_eq_localFrame_sum_coeff_smul b x_mem)
-- 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')
rw :
  Eq.{u_9 + 1} (α := A)
    (∑ i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5),
      Φ fun (x' : M) ↦ 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),
      Φ fun (x' : M) ↦ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((c i x' : (a : V x') → 𝕜) (σ' x') : 𝕜) (s i x'))
hσ₁ :
  ∀ (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
hσ₂ :
  ∀ (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:
rw [hΦ_eq hσ, hΦ_eq hσ', hΦ.sum, hΦ.sum]

Premises used: TensorialAt.sum
-- 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')
a :
  ∀ (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)),
    Membership.mem (γ := Finset (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)) Finset.univ i →
      (Φ fun (x' : M) ↦ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((c i x' : (a : V x') → 𝕜) (σ x') : 𝕜) (s i x')) =
        Φ fun (x' : M) ↦ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((c i x' : (a : V x') → 𝕜) (σ' x') : 𝕜) (s i x')
⊢ Eq.{u_9 + 1} (α := A)
    (∑ i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5),
      Φ fun (x' : M) ↦ 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),
      Φ fun (x' : M) ↦ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((c i x' : (a : V x') → 𝕜) (σ' x') : 𝕜) (s i x'))

Tactic:
congr! 1 with i
-- 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)
h : Membership.mem (γ := Finset (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)) Finset.univ i
⊢ Φ
      (HSMul.hSMul (α := M → 𝕜)
        ((((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 → 𝕜)
            σ :
          M → 𝕜)
        (s i)) =
    HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) ((c i x : (a : V x) → 𝕜) (σ x) : 𝕜) (Φ (s i))

Tactic:
hΦ.smul (hc hσ i) (hs i)

Premises used: TensorialAt.smul
-- 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)
h : Membership.mem (γ := Finset (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)) Finset.univ i
rw rw₁ :
  HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) ((c i x : (a : V x) → 𝕜) (σ' x) : 𝕜) (Φ (s i)) =
    HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) ((c i x : (a : V x) → 𝕜) (σ' x) : 𝕜) (Φ (s i))
⊢ HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) ((c i x : (a : V x) → 𝕜) (σ x) : 𝕜) (Φ (s i)) =
    HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) ((c i x : (a : V x) → 𝕜) (σ' x) : 𝕜) (Φ (s i))

Tactic:
rw [hσσ']
-- 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)
h : Membership.mem (γ := Finset (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)) Finset.univ i
⊢ HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) ((c i x : (a : V x) → 𝕜) (σ' x) : 𝕜) (Φ (s i)) =
    Φ
      (HSMul.hSMul (α := M → 𝕜)
        ((((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 → 𝕜)
            σ' :
          M → 𝕜)
        (s i))

Tactic:
hΦ.smul (hc hσ' i) (hs i) |>.symm

Premises used: Eq.symm, TensorialAt.smul
-- 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)
h : Membership.mem (γ := Finset (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)) Finset.univ i
calc :
  HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) ((c i x : (a : V x) → 𝕜) (σ x) : 𝕜) (Φ (s i)) =
    HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) ((c i x : (a : V x) → 𝕜) (σ' x) : 𝕜) (Φ (s i))
⊢ (Φ fun (x' : M) ↦ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((c i x' : (a : V x') → 𝕜) (σ x') : 𝕜) (s i x')) =
    Φ fun (x' : M) ↦ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((c i x' : (a : V x') → 𝕜) (σ' x') : 𝕜) (s i x')

Tactic:
calc Φ ((LinearMap.piApply (c i) σ) • (s i))
        = c i x (σ x) • Φ (s i) := hΦ.smul (hc hσ i) (hs i)
      _ = c i x (σ' x) • Φ (s i) := by rw [hσσ']
      _ = Φ ((LinearMap.piApply (c i) σ') • (s i)) :=
          hΦ.smul (hc hσ' i) (hs i) |>.symm

Premises used: LinearMap.piApply, HSMul.hSMul, Eq.symm, DFunLike.coe, TensorialAt.smul
-- 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