awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H_1 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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
H : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : HasMFDerivAt I 𝓘(𝕜, 𝕜) ψ x 0
⊢ cov (ψ • σ) x = ψ x • cov σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% ψ x) (σ x)

Tactic:
have := hcov.leibniz hσ hψ'.mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H_1 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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
H : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : HasMFDerivAt I 𝓘(𝕜, 𝕜) ψ x 0
this : cov (ψ • σ) x = ψ x • cov σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% ψ x) (σ x)
⊢ cov σ x = cov (ψ • σ) x

Tactic:
simp [hcov.leibniz hσ hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]

Premises used: HasMFDerivAt.mfderiv, mvfderiv, IsCovariantDerivativeOn.leibniz, HasMFDerivAt.mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H_1 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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
H : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : HasMFDerivAt I 𝓘(𝕜, 𝕜) ψ x 0
this : cov (ψ • σ) x = ψ x • cov σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% ψ x) (σ x)
rw rw₁ : cov (ψ • σ') x = cov (ψ • σ') x
⊢ cov (ψ • σ) x = cov (ψ • σ') x

Tactic:
rw [funext H]

Premises used: funext
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H_1 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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
H : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : HasMFDerivAt I 𝓘(𝕜, 𝕜) ψ x 0
this : cov (ψ • σ) x = ψ x • cov σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% ψ x) (σ x)
⊢ cov (ψ • σ') x = cov σ' x

Tactic:
simp [hcov.leibniz hσ' hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]

Premises used: HasMFDerivAt.mfderiv, mvfderiv, IsCovariantDerivativeOn.leibniz, HasMFDerivAt.mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H_1 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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
H : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : HasMFDerivAt I 𝓘(𝕜, 𝕜) ψ x 0
this : cov (ψ • σ) x = ψ x • cov σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% ψ x) (σ x)
calc : cov σ x = cov (ψ • σ) x
calc₁ : cov (ψ • σ) x = cov (ψ • σ') x
calc₂ : cov (ψ • σ') x = cov σ' x
⊢ cov σ x = cov σ' x

Tactic:
calc cov σ x
    _ = cov ((ψ : M → 𝕜) • σ) x := by
      simp [hcov.leibniz hσ hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]
    _ = cov ((ψ : M → 𝕜) • σ') x := by rw [funext H]
    _ = cov σ' x := by
      simp [hcov.leibniz hσ' hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]

Premises used: HSMul.hSMul
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
have have₁ have₂ have₃ : ∀ (hxs' : x ∈ s), cov σ x = cov σ' x
have₄ :
  ∀ (hxs' : x ∈ s),
    let ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0;
    ∀ (hψx : ψ x = 1), cov σ x = cov σ' x
have₅ :
  ∀ (hxs' : x ∈ s),
    let ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0;
    ∀ (hψx : ψ x = 1) (H_1 : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'), cov σ x = cov σ' x
have₆ :
  ∀ (hxs' : x ∈ s),
    let ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0;
    ∀ (hψx : ψ x = 1) (H_1 : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x') (hψ' : HasMFDerivAt I 𝓘(𝕜, 𝕜) ψ x 0),
      cov σ x = cov σ' x
have₇ :
  ∀ (hxs' : x ∈ s),
    let ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0;
    ∀ (hψx : ψ x = 1) (H_1 : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x') (hψ' : HasMFDerivAt I 𝓘(𝕜, 𝕜) ψ x 0)
      (this : cov (ψ • σ) x = ψ x • cov σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% ψ x) (σ x)), cov σ x = cov σ' x
⊢ cov σ x = cov σ' x

Tactic:
classical
  have hxs' : x ∈ s := mem_of_mem_nhds hxs
  let ψ (x' : M) : 𝕜 := if x' ∈ s then 1 else 0
  have hψx : ψ x = 1 := by simp [ψ, hxs']
  -- Observe that `ψ • σ = ψ • σ'` as dependent functions.
  have H (x' : M) : ((ψ : M → 𝕜) • σ) x' = ((ψ : M → 𝕜) • σ') x' := by
    dsimp [ψ]
    split_ifs with hx's
    · simpa using hσσ' _ hx's
    · simp
  have hψ' : HasMFDerivAt I 𝓘(𝕜) ψ x 0 := by
    have : HasMFDerivAt I 𝓘(𝕜, 𝕜) (fun (_x : M) ↦ (1 : 𝕜)) x 0 := hasMFDerivAt_const ..
    refine this.congr_of_eventuallyEq ?_
    apply Filter.eventuallyEq_of_mem hxs
    intro t ht
    simp [ψ, ht]
  have := hcov.leibniz hσ hψ'.mdifferentiableAt
  -- Then, it's a chain of (dependent) equalities.
  calc cov σ x
    _ = cov ((ψ : M → 𝕜) • σ) x := by
      simp [hcov.leibniz hσ hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]
    _ = cov ((ψ : M → 𝕜) • σ') x := by rw [funext H]
    _ = cov σ' x := by
      simp [hcov.leibniz hσ' hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ᶠ (x : M) in 𝓝 x, σ x = σ' x
⊢ ∃ v ∈ 𝓝 x, ∀ y ∈ v, σ y = σ' y

Tactic:
rw [eventually_iff_exists_mem] at hσσ'

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∃ v ∈ 𝓝 x, ∀ y ∈ v, σ y = σ' y
choose : ∀ (s' : Set M) (hs' : s' ∈ 𝓝 x) (b : ∀ y ∈ s', σ y = σ' y), cov σ x = cov σ' x
⊢ cov σ x = cov σ' x

Tactic:
choose s' hs' b using hσσ'
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
s' : Set M
hs' : s' ∈ 𝓝 x
b : ∀ y ∈ s', σ y = σ' y
⊢ cov σ x = cov σ' x

Tactic:
(hcov.mono inter_subset_left).congr_of_eqOn hσ hσ' (inter_mem hxs hs') fun x hx ↦ b x hx.2

Premises used: Filter.inter_mem, IsCovariantDerivativeOn.congr_of_eqOn, Set.inter_subset_left, And.right, IsCovariantDerivativeOn.mono
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
s' : Set M
hs' : s' ∈ 𝓝 x
b : ∀ y ∈ s', σ y = σ' y
⊢ cov σ x = cov σ' x

Tactic:
exact (hcov.mono inter_subset_left).congr_of_eqOn hσ hσ' (inter_mem hxs hs') fun x hx ↦ b x hx.2

Premises used: Filter.inter_mem, IsCovariantDerivativeOn.congr_of_eqOn, Set.inter_subset_left, And.right, IsCovariantDerivativeOn.mono
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
inst_15 : VectorBundle 𝕜 F V
hcov : IsCovariantDerivativeOn F (V := V) cov s
x : M
hx : x ∈ s
⊢ cov 0 x = 0

Tactic:
simpa using (hcov.add (mdifferentiableAt_zeroSection ..)
    (mdifferentiableAt_zeroSection ..) : cov (0 + 0) x = _)

Premises used: IsCovariantDerivativeOn.add, Bundle.mdifferentiableAt_zeroSection
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
σ : (x : M) → V x
x : M
a : 𝕜
hσ : MDiffAt (T% σ) x
hx : x ∈ s
⊢ cov (a • σ) x = a • cov σ x

Tactic:
simpa [mvfderiv] using hcov.leibniz (g := fun _ ↦ a) hσ mdifferentiableAt_const

Premises used: mvfderiv, IsCovariantDerivativeOn.leibniz, mdifferentiableAt_const
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
s : Set M
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
hcov : IsCovariantDerivativeOn F (V := V) cov s
cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
hcov' : IsCovariantDerivativeOn F (V := V) cov' s
g : M → 𝕜
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : x ∈ s
simp :
  g x • cov σ x + g x • cov σ' x + ((1 - g x) • cov' σ x + (1 - g x) • cov' σ' x) =
    g x • cov σ x + (1 - g x) • cov' σ x + (g x • cov σ' x + (1 - g x) • cov' σ' x)
⊢ (g • cov (σ + σ') + (1 - g) • cov' (σ + σ')) x = (g • cov σ + (1 - g) • cov' σ) x + (g • cov σ' + (1 - g) • cov' σ') x

Tactic:
simp [hcov.add hσ hσ', hcov'.add hσ hσ']

Premises used: IsCovariantDerivativeOn.add
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
s : Set M
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
hcov : IsCovariantDerivativeOn F (V := V) cov s
cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
hcov' : IsCovariantDerivativeOn F (V := V) cov' s
g : M → 𝕜
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : x ∈ s
⊢ g x • cov σ x + g x • cov σ' x + ((1 - g x) • cov' σ x + (1 - g x) • cov' σ' x) =
    g x • cov σ x + (1 - g x) • cov' σ x + (g x • cov σ' x + (1 - g x) • cov' σ' x)

Tactic:
module
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
s : Set M
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
hcov : IsCovariantDerivativeOn F (V := V) cov s
cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
hcov' : IsCovariantDerivativeOn F (V := V) cov' s
g : M → 𝕜
σ : (x : M) → V x
g_1 : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hφ : MDiffAt g_1 x
hx : x ∈ s
simp :
  g x • g_1 x • cov σ x +
        HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (g x)
          (ContinuousLinearMap.smulRight (S := 𝕜) (d% g_1 x) (σ x)) +
      ((1 - g x) • g_1 x • cov' σ x +
        HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (1 - g x)
          (ContinuousLinearMap.smulRight (S := 𝕜) (d% g_1 x) (σ x))) =
    g_1 x • g x • cov σ x + g_1 x • (1 - g x) • cov' σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% g_1 x) (σ x)
⊢ (g • cov (g_1 • σ) + (1 - g) • cov' (g_1 • σ)) x =
    g_1 x • (g • cov σ + (1 - g) • cov' σ) x + ContinuousLinearMap.smulRight (S := 𝕜) (d% g_1 x) (σ x)

Tactic:
simp [hcov.leibniz hσ hφ, hcov'.leibniz hσ hφ]

Premises used: IsCovariantDerivativeOn.leibniz
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
s : Set M
cov : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
hcov : IsCovariantDerivativeOn F (V := V) cov s
cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
hcov' : IsCovariantDerivativeOn F (V := V) cov' s
g : M → 𝕜
σ : (x : M) → V x
g_1 : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hφ : MDiffAt g_1 x
hx : x ∈ s
⊢ g x • g_1 x • cov σ x +
        HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (g x)
          (ContinuousLinearMap.smulRight (S := 𝕜) (d% g_1 x) (σ x)) +
      ((1 - g x) • g_1 x • cov' σ x +
        HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (1 - g x)
          (ContinuousLinearMap.smulRight (S := 𝕜) (d% g_1 x) (σ x))) =
    g_1 x • g x • cov σ x + g_1 x • (1 - g x) • cov' σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% g_1 x) (σ x)

Tactic:
module