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
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) → ((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 I F' (V := V') (Φ σ) x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : T2Space.{u_8} (V' x)
this_4 : FiniteDimensional.{u_1, u_8} 𝕜 (V' x)
this_5 : IsTopologicalAddGroup.{u_6} (V x)
this_6 : IsTopologicalAddGroup.{u_8} (V' x)
this_7 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_8} 𝕜 (V' x)
v : V x
w₁ w₂ : V' x
rw :
  Φ (extend F (E := V) v) (extend F' (E := V') (w₁ + w₂)) =
    Φ (extend F (E := V) v) (extend F' (E := V') w₁ + extend F' (E := V') w₂)
⊢ Φ (extend F (E := V) v) (extend F' (E := V') (w₁ + w₂)) =
    Φ (extend F (E := V) v) (extend F' (E := V') w₁) + Φ (extend F (E := V) v) (extend F' (E := V') w₂)

Tactic:
rw [← (hΦ₂ _ (mdifferentiableAt_extend ..)).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) → ((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 I F' (V := V') (Φ σ) x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : T2Space.{u_8} (V' x)
this_4 : FiniteDimensional.{u_1, u_8} 𝕜 (V' x)
this_5 : IsTopologicalAddGroup.{u_6} (V x)
this_6 : IsTopologicalAddGroup.{u_8} (V' x)
this_7 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_8} 𝕜 (V' x)
v : V x
w₁ w₂ : V' x
hσσ' : extend F (E := V) v x = extend F (E := V) v x
hττ' : extend F' (E := V') (w₁ + w₂) x = (extend F' (E := V') w₁ + extend F' (E := V') w₂) x
⊢ Φ (extend F (E := V) v) (extend F' (E := V') (w₁ + w₂)) =
    Φ (extend F (E := V) v) (extend F' (E := V') w₁ + extend F' (E := V') w₂)

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

Premises used: mdifferentiableAt_add_section, FiberBundle.mdifferentiableAt_extend, 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) → ((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 I F' (V := V') (Φ σ) x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : T2Space.{u_8} (V' x)
this_4 : FiniteDimensional.{u_1, u_8} 𝕜 (V' x)
this_5 : IsTopologicalAddGroup.{u_6} (V x)
this_6 : IsTopologicalAddGroup.{u_8} (V' x)
this_7 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_8} 𝕜 (V' x)
v : V x
w₁ w₂ : V' x
⊢ extend F (E := V) v x = extend F (E := V) v x

Tactic:
rfl
-- 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) → ((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 I F' (V := V') (Φ σ) x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : T2Space.{u_8} (V' x)
this_4 : FiniteDimensional.{u_1, u_8} 𝕜 (V' x)
this_5 : IsTopologicalAddGroup.{u_6} (V x)
this_6 : IsTopologicalAddGroup.{u_8} (V' x)
this_7 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_8} 𝕜 (V' x)
v : V x
w₁ w₂ : V' x
⊢ extend F' (E := V') (w₁ + w₂) x = (extend F' (E := V') w₁ + extend F' (E := V') w₂) 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) → ((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 I F' (V := V') (Φ σ) x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : T2Space.{u_8} (V' x)
this_4 : FiniteDimensional.{u_1, u_8} 𝕜 (V' x)
this_5 : IsTopologicalAddGroup.{u_6} (V x)
this_6 : IsTopologicalAddGroup.{u_8} (V' x)
this_7 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_8} 𝕜 (V' x)
c : 𝕜
v : V x
w : V' x
rw :
  Φ (extend F (E := V) v) (extend F' (E := V') (c • w)) =
    Φ (extend F (E := V) v) (HSMul.hSMul (α := M → 𝕜) (fun (x : M) ↦ c) (extend F' (E := V') w))
⊢ Φ (extend F (E := V) v) (extend F' (E := V') (c • w)) = c • Φ (extend F (E := V) v) (extend F' (E := V') w)

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

Premises used: mdifferentiable_const, FiberBundle.mdifferentiableAt_extend, 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
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) → ((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 I F' (V := V') (Φ σ) x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : T2Space.{u_8} (V' x)
this_4 : FiniteDimensional.{u_1, u_8} 𝕜 (V' x)
this_5 : IsTopologicalAddGroup.{u_6} (V x)
this_6 : IsTopologicalAddGroup.{u_8} (V' x)
this_7 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_8} 𝕜 (V' x)
c : 𝕜
v : V x
w : V' x
hσσ' : extend F (E := V) v x = extend F (E := V) v x
hττ' : extend F' (E := V') (c • w) x = HSMul.hSMul (α := M → 𝕜) (fun (x : M) ↦ c) (extend F' (E := V') w) x
⊢ Φ (extend F (E := V) v) (extend F' (E := V') (c • w)) =
    Φ (extend F (E := V) v) (HSMul.hSMul (α := M → 𝕜) (fun (x : M) ↦ c) (extend F' (E := V') w))

Tactic:
apply TensorialAt.pointwise₂ hΦ₁ hΦ₂ (mdifferentiableAt_extend ..)
        (mdifferentiableAt_extend ..) (mdifferentiableAt_extend ..) <|
        mdifferentiableAt_const.smul_section (mdifferentiableAt_extend ..)

Premises used: MDifferentiableAt.smul_section, FiberBundle.mdifferentiableAt_extend, mdifferentiableAt_const, 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) → ((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 I F' (V := V') (Φ σ) x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : T2Space.{u_8} (V' x)
this_4 : FiniteDimensional.{u_1, u_8} 𝕜 (V' x)
this_5 : IsTopologicalAddGroup.{u_6} (V x)
this_6 : IsTopologicalAddGroup.{u_8} (V' x)
this_7 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_8} 𝕜 (V' x)
c : 𝕜
v : V x
w : V' x
⊢ extend F (E := V) v x = extend F (E := V) v x

Tactic:
rfl
-- 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) → ((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 I F' (V := V') (Φ σ) x
this_1 : T2Space.{u_6} (V x)
this_2 : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
this_3 : T2Space.{u_8} (V' x)
this_4 : FiniteDimensional.{u_1, u_8} 𝕜 (V' x)
this_5 : IsTopologicalAddGroup.{u_6} (V x)
this_6 : IsTopologicalAddGroup.{u_8} (V' x)
this_7 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul.{u_1, u_8} 𝕜 (V' x)
c : 𝕜
v : V x
w : V' x
⊢ extend F' (E := V') (c • w) x = HSMul.hSMul (α := M → 𝕜) (fun (x : M) ↦ c) (extend F' (E := V') w) 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
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) → ((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 I F' (V := V') (Φ σ) x
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
τ : (x : M) → V' x
hτ : MDiffAt (T% τ) x
⊢ extend F (E := V) (σ x) x = σ 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
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) → ((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 I F' (V := V') (Φ σ) x
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
τ : (x : M) → V' x
hτ : MDiffAt (T% τ) x
⊢ extend F' (E := V') (τ x) x = τ 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
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) → ((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 I F' (V := V') (Φ σ) x
σ : V x
τ : V' x
⊢ ((((mkHom₂ (V := V) (V' := V') Φ x hΦ₁ hΦ₂ :
                V x →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (V' x) A) :
              (a : V x) → V' x →L[𝕜] A)
            σ :
          ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (V' x) A) :
        (a : V' x) → A)
      τ =
    Φ (extend F (E := V) σ) (extend F' (E := V') τ)

Tactic:
rfl

Premises used: rfl