awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
ι : Type u_9
s : Finset ι
t : ι → (x : B) → E x
x₀ : B
hs : ∀ (i : ι), MDiffAt (T% t) x₀
⊢ ∀ (i : ι), MDiffAt[univ] (T% t) x₀

Tactic:
simp_rw [← mdifferentiableWithinAt_univ] at hs ⊢

Premises used: mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
ι : Type u_9
s : Finset ι
t : ι → (x : B) → E x
x₀ : B
hs : ∀ (i : ι), MDiffAt[univ] (T% t) x₀
⊢ (MDiffAt[univ] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀

Tactic:
MDifferentiableWithinAt.sum_section hs

Premises used: MDifferentiableWithinAt.sum_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
ι : Type u_9
s : Finset ι
t : ι → (x : B) → E x
x₀ : B
hs : ∀ (i : ι), MDiffAt[univ] (T% t) x₀
⊢ (MDiffAt[univ] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀

Tactic:
exact MDifferentiableWithinAt.sum_section hs

Premises used: MDifferentiableWithinAt.sum_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
ι : Type u_9
s : Finset ι
t : ι → (x : B) → E x
hs : ∀ (i : ι), MDiff[u] (T% t)
⊢ MDiff[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩

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

Premises used: MDifferentiableOn, MDifferentiableWithinAt.sum_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
ι : Type u_9
s : Finset ι
t : ι → (x : B) → E x
hs : ∀ (i : ι), MDiff (T% t)
⊢ MDiff fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩

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

Premises used: MDifferentiableAt.sum_section, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
s : (x : B) → E x
ψ : B → 𝕜
hψ : MDiff[u] ψ
ht : IsOpen[inst] u
ht' : tsupport ψ ⊆ u
hs : MDiff[u] (T% s)
apply : MDiff[(tsupport ψ)ᶜ] fun (x : B) ↦ ⟨x, (ψ • s) x⟩
apply₁ : u ∪ (tsupport ψ)ᶜ = univ
⊢ MDiff fun (x : B) ↦ ⟨x, (ψ • s) x⟩

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

Premises used: Iff.mpr, mdifferentiable_of_mdifferentiableOn_union_of_isOpen, isClosed_tsupport, MDifferentiableOn.smul_section, isOpen_compl_iff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
s : (x : B) → E x
ψ : B → 𝕜
hψ : MDiff[u] ψ
ht : IsOpen[inst] u
ht' : tsupport ψ ⊆ u
hs : MDiff[u] (T% s)
apply : ∀ y ∈ (tsupport ψ)ᶜ, ⟨y, (ψ • s) y⟩ = zeroSection F E y
⊢ MDiff[(tsupport ψ)ᶜ] fun (x : B) ↦ ⟨x, (ψ • s) x⟩

Tactic:
apply ((mdifferentiable_zeroSection _ _).mdifferentiableOn (s := (tsupport ψ)ᶜ)).congr

Premises used: MDifferentiableOn.congr, Bundle.mdifferentiable_zeroSection, MDifferentiable.mdifferentiableOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
s : (x : B) → E x
ψ : B → 𝕜
hψ : MDiff[u] ψ
ht : IsOpen[inst] u
ht' : tsupport ψ ⊆ u
hs : MDiff[u] (T% s)
y : B
hy : y ∈ (tsupport ψ)ᶜ
⊢ ⟨y, (ψ • s) y⟩ = zeroSection F E 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.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
s : (x : B) → E x
ψ : B → 𝕜
hψ : MDiff[u] ψ
ht : IsOpen[inst] u
ht' : tsupport ψ ⊆ u
hs : MDiff[u] (T% s)
⊢ u ∪ (tsupport ψ)ᶜ = 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.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
s : (x : B) → E x
ψ : B → 𝕜
hψ : MDiff[u] ψ
ht : IsOpen[inst] u
ht' : tsupport ψ ⊆ u
hs : MDiff[u] (T% s)
⊢ u ∪ (tsupport ψ)ᶜ = 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.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
obtain :
  ∀ (u' : Set B) (hu' : u' ∈ 𝓝 x₀)
    (hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}),
    (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀

Tactic:
obtain ⟨u', hu', hfin⟩ := ht x₀
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
u' : Set B
hu' : u' ∈ 𝓝 x₀
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
have :
  ∀ (this : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty} : Type u_9)),
    (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀

Tactic:
have := hfin.fintype
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
u' : Set B
hu' : u' ∈ 𝓝 x₀
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
this : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty} : Type u_9)
⊢ (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) x₀

Tactic:
have : MDiffAt[u ∩ u'] (T% (fun x ↦ ∑ i ∈ s, (t i x))) x₀ :=
     .sum_section fun i ↦ ((ht' i).mono inter_subset_left)
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
u' : Set B
hu' : u' ∈ 𝓝 x₀
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty} : Type u_9)
this : (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) x₀
apply : (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀

Tactic:
apply (mdifferentiableWithinAt_inter hu').mp

Premises used: mdifferentiableWithinAt_inter, Iff.mp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
u' : Set B
hu' : u' ∈ 𝓝 x₀
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty} : Type u_9)
this : (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) x₀
apply : ∀ (y : B) (hy : y ∈ u'), Eq (α := TotalSpace F E) ⟨y, ∑' (i : ι), t i y⟩ ⟨y, ∑ i ∈ s.toFinset, t i y⟩
⊢ (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀

Tactic:
apply this.congr' (fun y hy ↦ ?_) inter_subset_right (mem_of_mem_nhds hu')

Premises used: MDifferentiableWithinAt.congr', mem_of_mem_nhds, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
u' : Set B
hu' : u' ∈ 𝓝 x₀
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty} : Type u_9)
this : (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) x₀
y : B
hy : y ∈ u'
rw : (support.{u_9, u_6} (M := E y) fun (i : ι) ↦ t i y) ⊆ (↑s.toFinset : Set ι)
⊢ Eq (α := TotalSpace F E) ⟨y, ∑' (i : ι), t i y⟩ ⟨y, ∑ i ∈ s.toFinset, t i y⟩

Tactic:
rw [TotalSpace.mk_inj, tsum_eq_sum']

Premises used: Bundle.TotalSpace.mk_inj, tsum_eq_sum'
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
u' : Set B
hu' : u' ∈ 𝓝 x₀
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty} : Type u_9)
this : (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) x₀
y : B
hy : y ∈ u'
⊢ (support.{u_9, u_6} (M := E y) fun (i : ι) ↦ t i y) ⊆ (↑s.toFinset : Set ι)

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

Premises used: Iff.mpr, Function.support_subset_iff'
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
u' : Set B
hu' : u' ∈ 𝓝 x₀
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty} : Type u_9)
this : (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) x₀
y : B
hy : y ∈ u'
refine : ∀ (i : ι) (hi : i ∉ (↑s.toFinset : Set ι)), t i y = 0
⊢ (support.{u_9, u_6} (M := E y) fun (i : ι) ↦ t i y) ⊆ (↑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.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
u' : Set B
hu' : u' ∈ 𝓝 x₀
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty} : Type u_9)
this : (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) x₀
y : B
hy : y ∈ u'
i : ι
hi : i ∉ (↑s.toFinset : Set ι)
by_contra! : ∀ (h : t i y ≠ 0), False
⊢ t i y = 0

Tactic:
by_contra! h
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
u' : Set B
hu' : u' ∈ 𝓝 x₀
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
s : Set ι := {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty}
this_1 : Fintype (↑{i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ u').Nonempty} : Type u_9)
this : (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) x₀
y : B
hy : y ∈ u'
i : ι
hi : i ∉ (↑s.toFinset : Set ι)
h : t i y ≠ 0
⊢ i ∈ s.toFinset

Tactic:
Set.mem_toFinset.mpr ?_

Premises used: Iff.mpr, Set.mem_toFinset