awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
ι : 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 : ι), ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, t i x⟩
⊢ ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, ∑ᶠ (i : ι), t i x⟩

Tactic:
fun x ↦ .finsum_section_of_locallyFinite ht fun i ↦ ht' i x

Premises used: ContMDiffAt.finsum_section_of_locallyFinite, ContMDiff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
toFun : (x : M) → V x
contMDiff_toFun : ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, toFun x⟩
toFun_1 : (x : M) → V x
contMDiff_toFun_1 : ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, toFun_1 x⟩
h : (mk (V := V) toFun contMDiff_toFun).toFun (V := V) = (mk (V := V) toFun_1 contMDiff_toFun_1).toFun (V := V)
⊢ mk (V := V) toFun contMDiff_toFun = mk (V := V) toFun_1 contMDiff_toFun_1

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
s : (x : M) → V x
hs : ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, s x⟩
⊢ (⇑(mk (V := V) s hs) : (a : M) → V a) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
s : Cₛ^n⟮I; F, V⟯
⊢ ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, (s : (a : M) → V a) x⟩

Tactic:
s.contMDiff_toFun

Premises used: ContMDiffSection.contMDiff_toFun
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
s t : Cₛ^n⟮I; F, V⟯
h : (⇑s : (a : M) → V a) = (⇑t : (a : M) → V a)
⊢ s = t

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
⊢ Injective (α := Cₛ^n⟮I; F, V⟯) (DFunLike.coe (β := V))

Tactic:
coe_inj

Premises used: ContMDiffSection.coe_inj, Function.Injective
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
s t : Cₛ^n⟮I; F, V⟯
h : ∀ (x : M), (s : (a : M) → V a) x = (t : (a : M) → V a) x
⊢ s = t

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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 t : Cₛ^n⟮I; F, V⟯
⊢ (⇑(s + t) : (a : M) → V a) = (⇑s : (a : M) → V a) + (⇑t : (a : M) → V a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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 t : Cₛ^n⟮I; F, V⟯
⊢ (⇑(s - t) : (a : M) → V a) = (⇑s : (a : M) → V a) - (⇑t : (a : M) → V a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
⊢ (⇑0 : (a : M) → V a) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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⟯
⊢ (⇑(-s) : (a : M) → V a) = -(⇑s : (a : M) → V a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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⟯
zero : (⇑(HSMul.hSMul (α := ℕ) 0 s) : (a : M) → V a) = 0
⊢ (⇑(HSMul.hSMul (α := ℕ) 0 s) : (a : M) → V a) = HSMul.hSMul (α := ℕ) 0 (⇑s : (a : M) → V a)

Tactic:
simp_rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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) = 0

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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)
succ : (⇑((k + 1) • s) : (a : M) → V a) = (⇑(k • s) : (a : M) → V a) + (⇑s : (a : M) → V a)
⊢ (⇑((k + 1) • s) : (a : M) → V a) = (k + 1) • (⇑s : (a : M) → V a)

Tactic:
simp_rw [succ_nsmul, ← ih]

Premises used: succ_nsmul
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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 • s) : (a : M) → V a) + (⇑s : (a : M) → V a)

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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)
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)
⊢ (⇑(k • s) : (a : M) → V a) = k • (⇑s : (a : M) → V a)

Tactic:
induction k with
  | zero => simp_rw [zero_smul]; rfl
  | succ k ih => simp_rw [succ_nsmul, ← ih]; rfl

Premises used: zero_smul, succ_nsmul
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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)
negSucc : ∀ (n_1 : ℕ), (⇑(Int.negSucc n_1 • s) : (a : M) → V a) = Int.negSucc n_1 • (⇑s : (a : M) → V a)
⊢ (⇑(z • s) : (a : M) → V a) = z • (⇑s : (a : M) → V a)

Tactic:
rcases z with n | n
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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)

Tactic:
(coe_nsmul s n).trans ?_

Premises used: ContMDiffSection.coe_nsmul, zsmulRec, Eq.trans
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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 : ℕ
ofNat : n • (⇑s : (a : M) → V a) = Int.ofNat n • (⇑s : (a : M) → V a)
⊢ (⇑(Int.ofNat n • s) : (a : M) → V a) = Int.ofNat n • (⇑s : (a : M) → V a)

Tactic:
refine (coe_nsmul s n).trans ?_

Premises used: ContMDiffSection.coe_nsmul, Eq.trans
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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 : ℕ
⊢ n • (⇑s : (a : M) → V a) = Int.ofNat n • (⇑s : (a : M) → V a)

Tactic:
simp only [Int.ofNat_eq_natCast, natCast_zsmul]

Premises used: Int.ofNat_eq_natCast, natCast_zsmul
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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)

Tactic:
(congr_arg Neg.neg (coe_nsmul s (n + 1))).trans ?_

Premises used: ContMDiffSection.coe_nsmul, congr_arg, HAdd.hAdd, OfNat.ofNat, Neg.neg, Eq.trans
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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 : ℕ
negSucc : -((n + 1) • (⇑s : (a : M) → V a)) = Int.negSucc n • (⇑s : (a : M) → V a)
⊢ (⇑(Int.negSucc n • 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 ?_

Premises used: ContMDiffSection.coe_nsmul, congr_arg, HAdd.hAdd, OfNat.ofNat, Neg.neg, Eq.trans
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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 : ℕ
⊢ -((n + 1) • (⇑s : (a : M) → V a)) = Int.negSucc n • (⇑s : (a : M) → V a)

Tactic:
simp only [negSucc_zsmul]

Premises used: negSucc_zsmul
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
r : 𝕜
s : Cₛ^n⟮I; F, V⟯
⊢ (⇑(r • s) : (a : M) → V a) = r • (⇑s : (a : M) → V a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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⟯
⊢ (coeAddHom I F n V : (a : Cₛ^n⟮I; F, V⟯) → (x : M) → V x) s = (⇑s : (a : M) → V a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
s : Cₛ^n⟮I; F, V⟯
hn : n ≠ 0
⊢ MDiff fun (x : M) ↦ ⟨x, (s : (a : M) → V a) x⟩

Tactic:
s.contMDiff.mdifferentiable hn

Premises used: ContMDiff.mdifferentiable, ContMDiffSection.contMDiff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
s : Cₛ^∞⟮I; F, V⟯
⊢ Ne (α := ℕ∞ω) ∞ 0

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
s : Cₛ^∞⟮I; F, V⟯
x : M
⊢ (MDiffAt fun (x : M) ↦ ⟨x, (s : (a : M) → V a) x⟩) x

Tactic:
s.mdifferentiable x

Premises used: ContMDiffSection.mdifferentiable
-- 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
ι : 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
obtain : ∀ (i : ι) (hxsi : Membership.mem (γ := Set M) ((fun (i : ι) ↦ s i) i) x), cov (σ + σ') x = cov σ x + cov σ' x
⊢ cov (σ + σ') x = cov σ x + cov σ' x

Tactic:
obtain ⟨si, ⟨i, rfl⟩, hxsi⟩ := hx

Premises used: rfl