awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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
s : Finset ι
t : ι → (x : B) → E x
hs : ∀ (i : ι), MDiffAt[u] (T% t) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀
have empty : (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ ∅, t i x⟩) x₀
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simpa using (contMDiffWithinAt_zeroSection 𝕜 E).mdifferentiableWithinAt one_ne_zero
  | insert i s hi h =>
    simpa [Finset.sum_insert hi] using mdifferentiableWithinAt_add_section (hs i) h
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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
s : Finset ι
t : ι → (x : B) → E x
hs : ∀ (i : ι), MDiffAt[u] (T% t) x₀
empty : (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ ∅, t i x⟩) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s) (h : (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀),
  (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ insert i s, t i x⟩) x₀
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simpa using (contMDiffWithinAt_zeroSection 𝕜 E).mdifferentiableWithinAt one_ne_zero
  | insert i s hi h =>
    simpa [Finset.sum_insert hi] using mdifferentiableWithinAt_add_section (hs i) h
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
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₀
⊢ (MDiffAt fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀
have hs₁ : ∀ (i : ι), MDiffAt[univ] (T% t) x₀
Tactic: simp_rw [← mdifferentiableWithinAt_univ] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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)
⊢ MDiff fun (x : B) ↦ ⟨x, (ψ • s) x⟩
have apply : MDiff[(tsupport ψ)ᶜ] 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 ψ)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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⟩
⊢ MDiff fun (x : B) ↦ ⟨x, (ψ • s) x⟩
have apply₁ : u ∪ (tsupport ψ)ᶜ = univ
Tactic: apply mdifferentiable_of_mdifferentiableOn_union_of_isOpen (hψ.smul_section hs) ?_ ?_ ht
      (isOpen_compl_iff.mpr <| isClosed_tsupport ψ)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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)
⊢ MDiff[(tsupport ψ)ᶜ] fun (x : B) ↦ ⟨x, (ψ • s) x⟩
have apply : ∀ y ∈ (tsupport ψ)ᶜ, ⟨y, (ψ • s) y⟩ = zeroSection F E y
Tactic: apply ((mdifferentiable_zeroSection _ _).mdifferentiableOn (s := (tsupport ψ)ᶜ)).congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀
have 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₀
Tactic: obtain ⟨u', hu', hfin⟩ := ht x₀
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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}
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀
have 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₀
Tactic: have := hfin.fintype
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
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] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀
have this₁ : (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)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀
have apply : (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀
Tactic: apply (mdifferentiableWithinAt_inter hu').mp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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₀
⊢ (MDiffAt[u ∩ u'] fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀
have apply : ∀ (y : B) (hy : y ∈ u'), Eq (α := TotalSpace F E) ⟨y, ∑' (i : ι), t i y⟩ ⟨y, ∑ i ∈ s.toFinset, t i y⟩
Tactic: apply this.congr' (fun y hy ↦ ?_) inter_subset_right (mem_of_mem_nhds hu')
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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'
⊢ Eq (α := TotalSpace F E) ⟨y, ∑' (i : ι), t i y⟩ ⟨y, ∑ i ∈ s.toFinset, t i y⟩
have rw : (support.{u_9, u_6} (M := E y) fun (i : ι) ↦ t i y) ⊆ (↑s.toFinset : Set ι)
Tactic: rw [TotalSpace.mk_inj, tsum_eq_sum']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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 ι)
have refine : ∀ (i : ι) (hi : i ∉ (↑s.toFinset : Set ι)), t i y = 0
Tactic: refine support_subset_iff'.mpr fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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 ι)
⊢ t i y = 0
have by_contra! : ∀ (h : t i y ≠ 0), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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
have refine : i ∈ s
Tactic: refine Set.mem_toFinset.mpr ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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
have simp : ({x : B | ¬t i x = 0} ∩ u').Nonempty
Tactic: simp only [s, ne_eq, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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
⊢ ({x : B | ¬t i x = 0} ∩ u').Nonempty
have h₁ : y ∈ {x : B | ¬t i x = 0} ∩ u'
Tactic: use y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
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
⊢ False
have this₁ : 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
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₀
⊢ (MDiffAt fun (x : B) ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀
have ht'₁ : ∀ (i : ι), MDiffAt[univ] (T% t) x₀
Tactic: simp_rw [← mdifferentiableWithinAt_univ] at ht' ⊢
Cleared hypotheses: ht'