awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite.{u_7, u_4} (X := M) fun (i : ι) ↦ {x : M | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀
y : M
hy : Membership.mem (γ := Set M) Set.univ y
⊢ HasFiniteSupport.{u_7, u_6} (M := V y) fun (i : ι) ↦ t i y
have choose : ∀ (U : Set M) (hu : U ∈ nhds y)
  (hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ U).Nonempty}),
  HasFiniteSupport.{u_7, u_6} (M := V y) fun (i : ι) ↦ t i y
Tactic: choose U hu hfin using ht y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite.{u_7, u_4} (X := M) fun (i : ι) ↦ {x : M | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀
y : M
hy : Membership.mem (γ := Set M) Set.univ y
U : Set M
hu : U ∈ nhds y
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ U).Nonempty}
x : ι
hx : Membership.mem (γ := Set ι) {x : ι | t x y ≠ 0} x
⊢ Membership.mem (γ := Set ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ U).Nonempty} x
have hx₁ : t x y ≠ 0
Tactic: rw [Set.mem_setOf] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite.{u_7, u_4} (X := M) fun (i : ι) ↦ {x : M | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀
y : M
hy : Membership.mem (γ := Set M) Set.univ y
U : Set M
hu : U ∈ nhds y
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ U).Nonempty}
x : ι
hx : t x y ≠ 0
⊢ ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) x ∩ U).Nonempty
have h : y ∈ (fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) x ∩ U
Tactic: use y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite.{u_7, u_4} (X := M) fun (i : ι) ↦ {x : M | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀
y : M
hy : Membership.mem (γ := Set M) Set.univ y
U : Set M
hu : U ∈ nhds y
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ U).Nonempty}
⊢ HasFiniteSupport.{u_7, u_6} (M := V y) fun (i : ι) ↦ t i y
have this : Subset.{u_7} (α := Set ι) {x : ι | t x y ≠ 0} {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ U).Nonempty}
Tactic: have : {x | t x y ≠ 0} ⊆ {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ U).Nonempty} := by
    intro x hx
    rw [Set.mem_setOf] at hx ⊢
    use y
    simpa using ⟨hx, mem_of_mem_nhds hu⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite.{u_7, u_4} (X := M) fun (i : ι) ↦ {x : M | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) x₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀
have ht'₁ : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) Set.univ x₀
Tactic: simp_rw [← contMDiffWithinAt_univ] at ht' ⊢
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : Cₛ^n⟮I; F, V⟯
⊢ (⇑(HSMul.hSMul (α := ℕ) 0 s) : (a : M) → V a) = HSMul.hSMul (α := ℕ) 0 (⇑s : (a : M) → V a)
have zero : (⇑(HSMul.hSMul (α := ℕ) 0 s) : (a : M) → V a) = 0
Tactic: simp_rw [zero_smul]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : Cₛ^n⟮I; F, V⟯
k : ℕ
ih : (⇑(k • s) : (a : M) → V a) = k • (⇑s : (a : M) → V a)
⊢ (⇑((k + 1) • s) : (a : M) → V a) = (k + 1) • (⇑s : (a : M) → V a)
have succ : (⇑((k + 1) • s) : (a : M) → V a) = (⇑(k • s) : (a : M) → V a) + (⇑s : (a : M) → V a)
Tactic: simp_rw [succ_nsmul, ← ih]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : Cₛ^n⟮I; F, V⟯
k : ℕ
⊢ (⇑(k • s) : (a : M) → V a) = k • (⇑s : (a : M) → V a)
have zero : (⇑(HSMul.hSMul (α := ℕ) 0 s) : (a : M) → V a) = HSMul.hSMul (α := ℕ) 0 (⇑s : (a : M) → V a)
Tactic: induction k with
  | zero => simp_rw [zero_smul]; rfl
  | succ k ih => simp_rw [succ_nsmul, ← ih]; rfl
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : Cₛ^n⟮I; F, V⟯
k : ℕ
zero : (⇑(HSMul.hSMul (α := ℕ) 0 s) : (a : M) → V a) = HSMul.hSMul (α := ℕ) 0 (⇑s : (a : M) → V a)
⊢ (⇑(k • s) : (a : M) → V a) = k • (⇑s : (a : M) → V a)
have succ : ∀ (k : ℕ) (ih : (⇑(k • s) : (a : M) → V a) = k • (⇑s : (a : M) → V a)),
  (⇑((k + 1) • s) : (a : M) → V a) = (k + 1) • (⇑s : (a : M) → V a)
Tactic: induction k with
  | zero => simp_rw [zero_smul]; rfl
  | succ k ih => simp_rw [succ_nsmul, ← ih]; rfl
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : Cₛ^n⟮I; F, V⟯
z : ℤ
⊢ (⇑(z • s) : (a : M) → V a) = z • (⇑s : (a : M) → V a)
have ofNat : ∀ (n_1 : ℕ), (⇑(Int.ofNat n_1 • s) : (a : M) → V a) = Int.ofNat n_1 • (⇑s : (a : M) → V a)
Tactic: rcases z with n | n
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : Cₛ^n⟮I; F, V⟯
z : ℤ
ofNat : ∀ (n_1 : ℕ), (⇑(Int.ofNat n_1 • s) : (a : M) → V a) = Int.ofNat n_1 • (⇑s : (a : M) → V a)
⊢ (⇑(z • s) : (a : M) → V a) = z • (⇑s : (a : M) → V a)
have negSucc : ∀ (n_1 : ℕ), (⇑(Int.negSucc n_1 • s) : (a : M) → V a) = Int.negSucc n_1 • (⇑s : (a : M) → V a)
Tactic: rcases z with n | n
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n_1 : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : Cₛ^n_1⟮I; F, V⟯
n : ℕ
⊢ (⇑(Int.ofNat n • s) : (a : M) → V a) = Int.ofNat n • (⇑s : (a : M) → V a)
have ofNat : n • (⇑s : (a : M) → V a) = Int.ofNat n • (⇑s : (a : M) → V a)
Tactic: refine (coe_nsmul s n).trans ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
n_1 : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : Cₛ^n_1⟮I; F, V⟯
n : ℕ
⊢ (⇑(Int.negSucc n • s) : (a : M) → V a) = Int.negSucc n • (⇑s : (a : M) → V a)
have negSucc : -((n + 1) • (⇑s : (a : M) → V a)) = Int.negSucc n • (⇑s : (a : M) → V a)
Tactic: refine (congr_arg Neg.neg (coe_nsmul s (n + 1))).trans ?_
-- 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
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 : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) cov (s i)
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : Membership.mem (γ := optParam (Set M) Set.univ) (⋃ (i : ι), s i) x
⊢ cov (σ + σ') x = cov σ x + cov σ' x
have obtain : ∀ (i : ι) (hxsi : Membership.mem (γ := Set M) ((fun (i : ι) ↦ s i) i) x), cov (σ + σ') x = cov σ x + cov σ' x
Tactic: obtain ⟨si, ⟨i, rfl⟩, hxsi⟩ := hx
Cleared hypotheses: 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
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 : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) cov (s i)
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hf' : MDiffAt g x
hx : Membership.mem (γ := optParam (Set M) Set.univ) (⋃ (i : ι), s i) x
⊢ cov (g • σ) x = g x • cov σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)
have obtain : ∀ (i : ι) (hxsi : Membership.mem (γ := Set M) ((fun (i : ι) ↦ s i) i) x),
  cov (g • σ) x = g x • cov σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)
Tactic: obtain ⟨si, ⟨i, rfl⟩, hxsi⟩ := hx
Cleared hypotheses: hx
-- 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 ∈ s, σ x = σ' x
⊢ cov σ x = cov σ' x
have hxs' : x ∈ s
Tactic: have hxs' : x ∈ s := mem_of_mem_nhds hxs
-- 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 ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0
⊢ cov σ x = cov σ' x
have hψx : ψ x = 1
Tactic: have hψx : ψ x = 1 := by simp [ψ, hxs']
-- 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
hxs' : x ∈ s
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
x' : M
⊢ (ψ • σ) x' = (ψ • σ') x'
have dsimp : HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if x' ∈ s then 1 else 0) (σ x') =
  HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if x' ∈ s then 1 else 0) (σ' x')
Tactic: dsimp [ψ]
-- 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
hxs' : x ∈ s
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
x' : M
⊢ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if x' ∈ s then 1 else 0) (σ x') =
    HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if x' ∈ s then 1 else 0) (σ' x')
have pos : ∀ (hx's : x' ∈ s), HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ x') = HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ' x')
Tactic: split_ifs with hx's
-- 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
hxs' : x ∈ s
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
x' : M
pos : ∀ (hx's : x' ∈ s), HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ x') = HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ' x')
⊢ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if x' ∈ s then 1 else 0) (σ x') =
    HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if x' ∈ s then 1 else 0) (σ' x')
have neg : ∀ (hx's : x' ∉ s), HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 0 (σ x') = HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 0 (σ' x')
Tactic: split_ifs with hx's