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
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
refine : i ∈ s
⊢ i ∈ s.toFinset

Tactic:
refine Set.mem_toFinset.mpr ?_

Premises used: Iff.mpr, Set.mem_toFinset
-- 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
simp : ({x : B | ¬t i x = 0} ∩ u').Nonempty
⊢ i ∈ s

Tactic:
simp only [s, ne_eq, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, ne_eq
-- 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
h₁ : y ∈ {x : B | ¬t i x = 0} ∩ u'
⊢ ({x : B | ¬t i x = 0} ∩ u').Nonempty

Tactic:
use y
-- 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
⊢ y ∈ {x : B | ¬t i x = 0} ∩ u'

Tactic:
simp [h, hy]
-- 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:
have : i ∈ s.toFinset := by
    refine Set.mem_toFinset.mpr ?_
    simp only [s, ne_eq, Set.mem_setOf_eq]
    use y
    simp [h, hy]
-- 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_2 : (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
this : i ∈ s.toFinset
⊢ False

Tactic:
hi this
-- 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_2 : (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
this : i ∈ s.toFinset
⊢ False

Tactic:
exact hi this
-- 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
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 (T% t) x₀
⊢ ∀ (i : ι), MDiffAt[univ] (T% t) x₀

Tactic:
simp_rw [← mdifferentiableWithinAt_univ] at ht' ⊢

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
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[univ] (T% t) x₀
⊢ (MDiffAt[univ] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀

Tactic:
.sum_section_of_locallyFinite ht ht'

Premises used: MDifferentiableWithinAt.sum_section_of_locallyFinite
-- 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
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[univ] (T% t) x₀
⊢ (MDiffAt[univ] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀

Tactic:
exact .sum_section_of_locallyFinite ht ht'
-- 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
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiff[u] (T% t)
⊢ MDiff[u] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩

Tactic:
fun x hx ↦ .sum_section_of_locallyFinite ht (ht' · x hx)

Premises used: MDifferentiableWithinAt.sum_section_of_locallyFinite, 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
ι : 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 : ι), MDiff (T% t)
⊢ MDiff fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩

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

Premises used: MDifferentiableAt.sum_section_of_locallyFinite, 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
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 ⊆ univ

Tactic:
grind
-- 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₀
apply :
  ∀ (y : B) (hy : Membership.mem (γ := Set B) univ y),
    Eq (α := TotalSpace F E) ⟨y, ∑ᶠ (i : ι), t i y⟩ ⟨y, ∑' (i : ι), t i y⟩
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀

Tactic:
apply (MDifferentiableWithinAt.sum_section_of_locallyFinite ht ht').congr' (t := Set.univ)
      (fun y hy ↦ ?_) (by grind) trivial

Premises used: MDifferentiableWithinAt.congr', trivial, MDifferentiableWithinAt.sum_section_of_locallyFinite
-- 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₀
y : B
hy : Membership.mem (γ := Set B) univ y
choose :
  ∀ (U : Set B) (hu : U ∈ 𝓝 y)
    (hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}),
    Eq (α := TotalSpace F E) ⟨y, ∑ᶠ (i : ι), t i y⟩ ⟨y, ∑' (i : ι), t i y⟩
⊢ Eq (α := TotalSpace F E) ⟨y, ∑ᶠ (i : ι), t i y⟩ ⟨y, ∑' (i : ι), t i y⟩

Tactic:
choose U hu hfin using ht y
-- 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₀
y : B
hy : Membership.mem (γ := Set B) univ y
U : Set B
hu : U ∈ 𝓝 y
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
x : ι
hx : Membership.mem (γ := Set ι) {x : ι | t x y ≠ 0} x
⊢ t x y ≠ 0

Tactic:
rw [Set.mem_setOf] at hx ⊢

Premises used: Set.mem_setOf
-- 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₀
y : B
hy : Membership.mem (γ := Set B) univ y
U : Set B
hu : U ∈ 𝓝 y
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
x : ι
hx : t x y ≠ 0
h : y ∈ (fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) x ∩ U
⊢ ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) x ∩ U).Nonempty

Tactic:
use y
-- 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₀
y : B
hy : Membership.mem (γ := Set B) univ y
U : Set B
hu : U ∈ 𝓝 y
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
x : ι
hx : t x y ≠ 0
⊢ y ∈ (fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) x ∩ U

Tactic:
simpa using ⟨hx, mem_of_mem_nhds hu⟩
-- 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₀
y : B
hy : Membership.mem (γ := Set B) univ y
U : Set B
hu : U ∈ 𝓝 y
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
⊢ Subset.{u_9} (α := Set ι) {x : ι | t x y ≠ 0} {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) 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⟩
-- 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₀
y : B
hy : Membership.mem (γ := Set B) univ y
U : Set B
hu : U ∈ 𝓝 y
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
this :
  Subset.{u_9} (α := Set ι) {x : ι | t x y ≠ 0} {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
rw rw₁ : Eq (α := TotalSpace F E) ⟨y, ∑ᶠ (i : ι), t i y⟩ ⟨y, ∑ᶠ (b : ι), t b y⟩
⊢ Eq (α := TotalSpace F E) ⟨y, ∑ᶠ (i : ι), t i y⟩ ⟨y, ∑' (i : ι), t i y⟩

Tactic:
rw [tsum_eq_finsum (hfin.subset this)]

Premises used: tsum_eq_finsum, Set.Finite.subset