awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
⊢ cov σ x = cov σ' x
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (hypothesis)
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
⊢ cov σ x = cov σ' x
have hσσ'₁ : ∃ v ∈ 𝓝 x, ∀ y ∈ v, σ y = σ' y
Tactic: rw [eventually_iff_exists_mem] at hσσ'
Cleared hypotheses: hσσ'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
⊢ cov σ x = cov σ' x
have choose : ∀ (s' : Set M) (hs' : s' ∈ 𝓝 x) (b : ∀ y ∈ s', σ y = σ' y), cov σ x = cov σ' x
Tactic: choose s' hs' b using hσσ'
Cleared hypotheses: hσσ'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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 • cov (σ + σ') + (1 - g) • cov' (σ + σ')) x = (g • cov σ + (1 - g) • cov' σ) x + (g • cov σ' + (1 - g) • cov' σ') x
have 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)
Tactic: simp [hcov.add hσ hσ', hcov'.add hσ hσ']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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 • 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)
have 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)
Tactic: simp [hcov.leibniz hσ hφ, hcov'.leibniz hσ hφ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
inst_15 : IsManifold I 1 M
inst_16 : VectorBundle 𝕜 F V
cov cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
u : Set M
f : M → 𝕜
n : ℕ∞ω
hf : ContMDiffOn I 𝓘(𝕜, 𝕜) n f u
Hcov : ContMDiffCovariantDerivativeOn F (V := V) n cov u
Hcov' : ContMDiffCovariantDerivativeOn F (V := V) n cov' u
σ : (x : M) → V x
hσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) (n + 1) (fun (x : M) ↦ ⟨x, σ x⟩) u
⊢ ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
    TotalSpace (E →L[𝕜] F) fun (x : M) ↦
      ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    n (fun (x : M) ↦ ⟨x, (f • cov σ + (1 - f) • cov' σ) x⟩) u
have hs : ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
  TotalSpace (E →L[𝕜] F) fun (x : M) ↦ ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
  n (fun (x : M) ↦ ⟨x, (f • cov σ) x⟩) u
Tactic: apply ContMDiffOn.add_section
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
inst_15 : IsManifold I 1 M
inst_16 : VectorBundle 𝕜 F V
cov cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
u : Set M
f : M → 𝕜
n : ℕ∞ω
hf : ContMDiffOn I 𝓘(𝕜, 𝕜) n f u
Hcov : ContMDiffCovariantDerivativeOn F (V := V) n cov u
Hcov' : ContMDiffCovariantDerivativeOn F (V := V) n cov' u
σ : (x : M) → V x
hσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) (n + 1) (fun (x : M) ↦ ⟨x, σ x⟩) u
hs :
  ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
    TotalSpace (E →L[𝕜] F) fun (x : M) ↦
      ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    n (fun (x : M) ↦ ⟨x, (f • cov σ) x⟩) u
⊢ ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
    TotalSpace (E →L[𝕜] F) fun (x : M) ↦
      ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    n (fun (x : M) ↦ ⟨x, (f • cov σ + (1 - f) • cov' σ) x⟩) u
have ht : ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
  TotalSpace (E →L[𝕜] F) fun (x : M) ↦ ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
  n (fun (x : M) ↦ ⟨x, ((1 - f) • cov' σ) x⟩) u
Tactic: apply ContMDiffOn.add_section
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
ι : Type u_7
s : Finset ι
u : 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)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : x ∈ u
⊢ ∑ i ∈ s, f i x • cov i (σ + σ') x =
    HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
      (∑ i ∈ s, f i x • cov i σ x) (∑ i ∈ s, f i x • cov i σ' x)
have rw : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
  (∑ i ∈ s, f i x • cov i (σ + σ') x) (∑ x_1 ∈ s, (f x_1 x • cov x_1 σ x + f x_1 x • cov x_1 σ' x))
Tactic: rw [← Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
ι : Type u_7
s : Finset ι
u : 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)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : x ∈ u
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    (∑ i ∈ s, f i x • cov i (σ + σ') x) (∑ x_1 ∈ s, (f x_1 x • cov x_1 σ x + f x_1 x • cov x_1 σ' x))
have e_f : Eq (α := ι → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
  (fun (i : ι) ↦ f i x • cov i (σ + σ') x) fun (x_1 : ι) ↦ f x_1 x • cov x_1 σ x + f x_1 x • cov x_1 σ' x
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
ι : Type u_7
s : Finset ι
u : 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)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : x ∈ u
⊢ Eq (α := ι → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    (fun (i : ι) ↦ f i x • cov i (σ + σ') x) fun (x_1 : ι) ↦ f x_1 x • cov x_1 σ x + f x_1 x • cov x_1 σ' x
have e_f : ∀ (i : ι) (x_1 : TangentSpace I x),
  Eq.{u_6 + 1} (α := V x) ((f i x • cov i (σ + σ') x : (a : TangentSpace I x) → V x) x_1 : V x)
    ((f i x • cov i σ x + f i x • cov i σ' x : (a : TangentSpace I x) → V x) x_1 : V x)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
ι : Type u_7
s : Finset ι
u : 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)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : x ∈ u
i : ι
x_1 : TangentSpace I x
⊢ Eq.{u_6 + 1} (α := V x) ((f i x • cov i (σ + σ') x : (a : TangentSpace I x) → V x) x_1 : V x)
    ((f i x • cov i σ x + f i x • cov i σ' x : (a : TangentSpace I x) → V x) x_1 : V x)
have e_f : Eq.{u_6 + 1} (α := V x) ((f i x • cov i (σ + σ') x : (a : TangentSpace I x) → V x) x_1 : V x)
  ((f i x • (cov i σ x + cov i σ' x) : (a : TangentSpace I x) → V x) x_1 : V x)
Tactic: rw [← smul_add, (h i).add hσ hσ' hx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
ι : Type u_7
s : Finset ι
u : 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)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : x ∈ u
i : ι
x_1 : TangentSpace I x
e_f :
  Eq.{u_6 + 1} (α := V x) ((f i x • cov i (σ + σ') x : (a : TangentSpace I x) → V x) x_1 : V x)
    ((f i x • (cov i σ x + cov i σ' x) : (a : TangentSpace I x) → V x) x_1 : V x)
⊢ Eq.{u_6 + 1} (α := V x) ((f i x • cov i (σ + σ') x : (a : TangentSpace I x) → V x) x_1 : V x)
    ((f i x • cov i σ x + f i x • cov i σ' x : (a : TangentSpace I x) → V x) x_1 : V x)
have e_f₁ : Eq.{u_6 + 1} (α := V x) ((f i x • (cov i σ x + cov i σ' x) : (a : TangentSpace I x) → V x) x_1 : V x)
  ((f i x • (cov i σ x + cov i σ' x) : (a : TangentSpace I x) → V x) x_1 : V x)
Tactic: rw [← smul_add, (h i).add hσ hσ' hx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
ι : Type u_7
s : Finset ι
u : 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)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    (∑ i ∈ s, f i x • cov i (g • σ) x)
    (∑ i ∈ s,
      (g x • f i x • cov i σ x +
        HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f i x)
          (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))))
have a : ∀ (i : ι) (hi : i ∈ s),
  f i x • cov i (g • σ) x =
    g x • f i x • cov i σ x +
      HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f i x)
        (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))
Tactic: congr! 1 with i hi
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
ι : Type u_7
s : Finset ι
u : 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)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
i : ι
hi : i ∈ s
⊢ f i x • cov i (g • σ) x =
    g x • f i x • cov i σ x +
      HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f i x)
        (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))
have a : f i x • (g x • cov i σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)) =
  g x • f i x • cov i σ x +
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f i x)
      (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))
Tactic: rw [(h i).leibniz hσ hg]