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
u : Set M
ι : Type u_7
t : ι → (x : M) → V x
s : Finset ι
hs : ∀ i ∈ s, ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u

Tactic:
fun x₀ hx₀ ↦ .sum_section fun i hi ↦ hs i hi x₀ hx₀

Premises used: ContMDiffWithinAt.sum_section, ContMDiffOn
-- 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
s : Finset ι
hs : ∀ i ∈ s, 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 ∈ s, t i x⟩

Tactic:
fun x₀ ↦ .sum_section fun i hi ↦ (hs i hi) x₀

Premises used: ContMDiff, ContMDiffAt.sum_section
-- 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
u : Set M
s : (x : M) → V x
ψ : M → 𝕜
hψ : ContMDiffOn I 𝓘(𝕜, 𝕜) n ψ u
ht : IsOpen u
ht' : tsupport ψ ⊆ u
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u
apply : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (ψ • s) x⟩) (tsupport ψ)ᶜ
apply₁ : u ∪ (tsupport ψ)ᶜ = Set.univ
⊢ ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, (ψ • s) x⟩

Tactic:
apply contMDiff_of_contMDiffOn_union_of_isOpen (hψ.smul_section hs) ?_ ?_ ht
      (isOpen_compl_iff.mpr <| isClosed_tsupport ψ)

Premises used: Iff.mpr, contMDiff_of_contMDiffOn_union_of_isOpen, isClosed_tsupport, isOpen_compl_iff, ContMDiffOn.smul_section
-- 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
u : Set M
s : (x : M) → V x
ψ : M → 𝕜
hψ : ContMDiffOn I 𝓘(𝕜, 𝕜) n ψ u
ht : IsOpen u
ht' : tsupport ψ ⊆ u
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u
apply : ∀ y ∈ (tsupport ψ)ᶜ, ⟨y, (ψ • s) y⟩ = zeroSection F V y
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (ψ • s) x⟩) (tsupport ψ)ᶜ

Tactic:
apply ((contMDiff_zeroSection _ _).contMDiffOn (s := (tsupport ψ)ᶜ)).congr

Premises used: ContMDiff.contMDiffOn, Bundle.contMDiff_zeroSection, ContMDiffOn.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
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
s : (x : M) → V x
ψ : M → 𝕜
hψ : ContMDiffOn I 𝓘(𝕜, 𝕜) n ψ u
ht : IsOpen u
ht' : tsupport ψ ⊆ u
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u
y : M
hy : y ∈ (tsupport ψ)ᶜ
⊢ ⟨y, (ψ • s) y⟩ = zeroSection F V y

Tactic:
simp [image_eq_zero_of_notMem_tsupport hy, zeroSection]

Premises used: image_eq_zero_of_notMem_tsupport, Bundle.zeroSection
-- 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
u : Set M
s : (x : M) → V x
ψ : M → 𝕜
hψ : ContMDiffOn I 𝓘(𝕜, 𝕜) n ψ u
ht : IsOpen u
ht' : tsupport ψ ⊆ u
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u
⊢ u ∪ (tsupport ψ)ᶜ = Set.univ

Tactic:
Set.compl_subset_iff_union.mp <| Set.compl_subset_compl.mpr ht'

Premises used: Iff.mpr, Set.compl_subset_compl, Set.compl_subset_iff_union, Iff.mp
-- 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
u : Set M
s : (x : M) → V x
ψ : M → 𝕜
hψ : ContMDiffOn I 𝓘(𝕜, 𝕜) n ψ u
ht : IsOpen u
ht' : tsupport ψ ⊆ u
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u
⊢ u ∪ (tsupport ψ)ᶜ = Set.univ

Tactic:
exact Set.compl_subset_iff_union.mp <| Set.compl_subset_compl.mpr ht'

Premises used: Iff.mpr, Set.compl_subset_compl, Set.compl_subset_iff_union, Iff.mp
-- 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
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₀
obtain :
  ∀ (u' : Set M) (hu' : u' ∈ nhds x₀)
    (hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}),
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) u x₀

Tactic:
obtain ⟨u', hu', hfin⟩ := ht x₀
-- 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
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₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
have :
  ∀ (this : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty} : Type u_7)),
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) u x₀

Tactic:
have := hfin.fintype
-- 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
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₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
this : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty} : Type u_7)
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀

Tactic:
have : CMDiffAt[u ∩ u'] n (T% (fun x ↦ (∑ i ∈ s, (t i x)))) x₀ :=
    .sum_section fun i hi ↦ ((ht' i).mono Set.inter_subset_left)
-- 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
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₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty} : Type u_7)
this :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀
apply : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) (u ∩ u') x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) u x₀

Tactic:
apply (contMDiffWithinAt_inter hu').mp

Premises used: contMDiffWithinAt_inter, Iff.mp
-- 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
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₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty} : Type u_7)
this :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀
apply : Eq (α := TotalSpace F V) ⟨x₀, ∑' (i : ι), t i x₀⟩ ⟨x₀, ∑ i ∈ s.toFinset, t i x₀⟩
apply₁ : ∀ (y : M) (hy : y ∈ u ∩ u'), Eq (α := TotalSpace F V) ⟨y, ∑' (i : ι), t i y⟩ ⟨y, ∑ i ∈ s.toFinset, t i y⟩
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) (u ∩ u') x₀

Tactic:
apply this.congr fun y hy ↦ ?_

Premises used: ContMDiffWithinAt.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
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₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty} : Type u_7)
this :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀
rw : (support.{u_7, u_6} (M := V x₀) fun (i : ι) ↦ t i x₀) ⊆ (↑s.toFinset : Set ι)
⊢ Eq (α := TotalSpace F V) ⟨x₀, ∑' (i : ι), t i x₀⟩ ⟨x₀, ∑ i ∈ s.toFinset, t i x₀⟩

Tactic:
rw [TotalSpace.mk_inj, tsum_eq_sum']

Premises used: Bundle.TotalSpace.mk_inj, tsum_eq_sum'
-- 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
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₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty} : Type u_7)
this :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀
⊢ (support.{u_7, u_6} (M := V x₀) fun (i : ι) ↦ t i x₀) ⊆ (↑s.toFinset : Set ι)

Tactic:
support_subset_iff'.mpr fun i hi ↦ ?_

Premises used: Iff.mpr, Function.support_subset_iff'
-- 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
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₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty} : Type u_7)
this :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀
refine : ∀ (i : ι) (hi : i ∉ (↑s.toFinset : Set ι)), t i x₀ = 0
⊢ (support.{u_7, u_6} (M := V x₀) fun (i : ι) ↦ t i x₀) ⊆ (↑s.toFinset : Set ι)

Tactic:
refine support_subset_iff'.mpr fun i hi ↦ ?_

Premises used: Iff.mpr, Function.support_subset_iff'
-- 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
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₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty} : Type u_7)
this :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀
i : ι
hi : i ∉ (↑s.toFinset : Set ι)
by_contra! : ∀ (h : t i x₀ ≠ 0), False
⊢ t i x₀ = 0

Tactic:
by_contra! h
-- 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
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₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty} : Type u_7)
this :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀
i : ι
hi : i ∉ (↑s.toFinset : Set ι)
h : t i x₀ ≠ 0
⊢ i ∈ s.toFinset

Tactic:
Set.mem_toFinset.mpr ?_

Premises used: Iff.mpr, Set.mem_toFinset
-- 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
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₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : Set.Finite.{u_7} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : M | t i x ≠ 0} : Set M)) i ∩ u').Nonempty} : Type u_7)
this :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀
i : ι
hi : i ∉ (↑s.toFinset : Set ι)
h : t i x₀ ≠ 0
refine : i ∈ s
⊢ i ∈ s.toFinset

Tactic:
refine Set.mem_toFinset.mpr ?_

Premises used: Iff.mpr, Set.mem_toFinset