awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
x : E
⊢ ContMDiffAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' := TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) n
      (fun (x : E) ↦ ⟨x, V x⟩) x ↔
    ContDiffAt 𝕜 n V x

Tactic:
simp only [← contMDiffWithinAt_univ, ← contDiffWithinAt_univ,
    contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt]

Premises used: contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, contDiffWithinAt_univ, contMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
⊢ ContMDiffOn 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' := TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) n
      (fun (x : E) ↦ ⟨x, V x⟩) s ↔
    ContDiffOn 𝕜 n V s

Tactic:
simp only [ContMDiffOn, ContDiffOn, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt]

Premises used: contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, ContDiffOn, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
⊢ (ContMDiff 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' := TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) n
      fun (x : E) ↦ ⟨x, V x⟩) ↔
    ContDiff 𝕜 n V

Tactic:
simp only [← contMDiffOn_univ, ← contDiffOn_univ, contMDiffOn_vectorSpace_iff_contDiffOn]

Premises used: contMDiffOn_univ, contDiffOn_univ, contMDiffOn_vectorSpace_iff_contDiffOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
erw :
  VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
        (VectorBundleCore.indexAt (tangentBundleCore I' H') y) (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)
        y ∘SL
      ϕ ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
          (VectorBundleCore.indexAt (tangentBundleCore I H) x₀) (VectorBundleCore.indexAt (tangentBundleCore I H) x) x =
    ϕ
hx :
  x ∈
    VectorBundleCore.baseSet (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
      (VectorBundleCore.indexAt (tangentBundleCore I H) x₀)
hy :
  y ∈
    VectorBundleCore.baseSet (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
      (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)
⊢ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ

Tactic:
erw [VectorBundleCore.inCoordinates_eq]

Premises used: VectorBundleCore.inCoordinates_eq
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ x ∈
    VectorBundleCore.baseSet (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
      (VectorBundleCore.indexAt (tangentBundleCore I H) x₀)

Tactic:
trivial
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ x ∈
    VectorBundleCore.baseSet (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
      (VectorBundleCore.indexAt (tangentBundleCore I H) x₀)

Tactic:
try trivial
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ y ∈
    VectorBundleCore.baseSet (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
      (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)

Tactic:
trivial
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ y ∈
    VectorBundleCore.baseSet (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
      (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)

Tactic:
try trivial
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
simp_rw :
  VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H') (achart H' y) (achart H' y₀)
        y ∘SL
      ϕ ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H) (achart H x₀) (achart H x)
          x =
    ϕ
simp_rw₁ : ContinuousLinearMap.id 𝕜 E' ∘SL ϕ ∘SL ContinuousLinearMap.id 𝕜 E = ϕ
simp_rw₂ : ϕ ∘SL ContinuousLinearMap.id 𝕜 E = ϕ
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
        (VectorBundleCore.indexAt (tangentBundleCore I' H') y) (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)
        y ∘SL
      ϕ ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
          (VectorBundleCore.indexAt (tangentBundleCore I H) x₀) (VectorBundleCore.indexAt (tangentBundleCore I H) x) x =
    ϕ

Tactic:
simp_rw [tangentBundleCore_indexAt, tangentBundleCore_coordChange_model_space,
    ContinuousLinearMap.id_comp, ContinuousLinearMap.comp_id]

Premises used: tangentBundleCore_coordChange_model_space, ContinuousLinearMap.id_comp, ContinuousLinearMap.comp_id, tangentBundleCore_indexAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_9
f : N → H
g : N → H'
ϕ : N → E →L[𝕜] E'
x₀ : N
⊢ inTangentCoordinates I I' f g ϕ x₀ = ϕ

Tactic:
simp +unfoldPartialApp only [inTangentCoordinates,
    inCoordinates_tangent_bundle_core_model_space]

Premises used: inTangentCoordinates, inCoordinates_tangent_bundle_core_model_space
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
N : Type u_9
f : N → M
g : N → M'
ϕ : N → E →L[𝕜] E'
x₀ x : N
hx : f x ∈ (toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (toPartialEquiv (chartAt H' (g x₀))).source
⊢ inTangentCoordinates I I' f g ϕ x₀ x =
    VectorBundleCore.coordChange (ι := (↑(atlas H' M') : Type (max u_5 u_7))) (tangentBundleCore I' M')
        (achart H' (g x)) (achart H' (g x₀)) (g x) ∘SL
      ϕ x ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M)
          (achart H (f x₀)) (achart H (f x)) (f x)

Tactic:
(tangentBundleCore I M).inCoordinates_eq (tangentBundleCore I' M') (ϕ x) hx hy

Premises used: VectorBundleCore.Fiber, inTangentCoordinates, FiberBundleCore.Fiber, VectorBundleCore.moduleFiber._aux_1, VectorBundleCore.topologicalSpaceFiber._aux_1, tangentBundleCore, VectorBundleCore.addCommGroupFiber._aux_4, TangentSpace, VectorBundleCore.inCoordinates_eq, instTopologicalSpaceTangentSpace._aux_1, VectorBundleCore.addCommGroupFiber._aux_1, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- 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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
⊢ ψ x = 1

Tactic:
simp [ψ, hσσ'.self_of_nhds]

Premises used: Filter.Eventually.self_of_nhds
-- 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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
⊢ ψ x = 1

Tactic:
have hψx : ψ x = 1 := by simp [ψ, hσσ'.self_of_nhds]
-- 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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
dsimp :
  HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if σ x' = σ' x' then 1 else 0) (σ x') =
    HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if σ x' = σ' x' then 1 else 0) (σ' x')
⊢ (ψ • σ) x' = (ψ • σ') x'

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
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
pos :
  ∀ (hx' : σ x' = σ' x'), HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ x') = HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ' x')
neg :
  ∀ (hx' : ¬σ x' = σ' x'),
    HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 0 (σ x') = HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 0 (σ' x')
⊢ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if σ x' = σ' x' then 1 else 0) (σ x') =
    HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if σ x' = σ' x' then 1 else 0) (σ' x')

Tactic:
split_ifs with hx'
-- 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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
hx' : σ x' = σ' x'
⊢ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ x') = HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ' x')

Tactic:
simp [hx']
-- 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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
hx' : ¬σ x' = σ' x'
⊢ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 0 (σ x') = HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 0 (σ' x')

Tactic:
simp [hx']
-- 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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
⊢ ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'

Tactic:
have (x' : M) : (ψ • σ) x' = (ψ • σ') x' := by
    dsimp [ψ]
    split_ifs with hx' <;> simp [hx']
-- 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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
⊢ (MDiffAt fun (_x : M) ↦ 1) x

Tactic:
have : MDiffAt (fun (_x : M) ↦ (1 : 𝕜)) x := mdifferentiableAt_const
-- 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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this_1 : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
this : (MDiffAt fun (_x : M) ↦ 1) x
x' : M
hx' : σ x' = σ' x'
⊢ ψ x' = (fun (_x : M) ↦ (1 : 𝕜)) x'

Tactic:
simp [ψ, hx']
-- 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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this_1 : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
this : (MDiffAt fun (_x : M) ↦ 1) x
⊢ MDiffAt ψ x

Tactic:
exact this.congr_of_eventuallyEq (hσσ'.mono fun x' hx' ↦ by simp [ψ, hx'])

Premises used: MDifferentiableAt.congr_of_eventuallyEq, Filter.Eventually.mono
-- 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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
⊢ MDiffAt ψ x

Tactic:
have hψ' : MDiffAt ψ x := by
    have : MDiffAt (fun (_x : M) ↦ (1 : 𝕜)) x := mdifferentiableAt_const
    exact this.congr_of_eventuallyEq (hσσ'.mono fun x' hx' ↦ by simp [ψ, hx'])
-- 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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : MDiffAt ψ x
⊢ Φ σ = Φ (ψ • σ)

Tactic:
simp [hΦ.smul hψ' hσ, hψx]

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
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : MDiffAt ψ x
rw rw₁ : Φ (ψ • σ') = Φ (ψ • σ')
⊢ Φ (ψ • σ) = Φ (ψ • σ')

Tactic:
rw [funext this]

Premises used: funext