awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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
s : Finset ι
hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
have empty : ∀
  (hs :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, 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: induction s using Finset.induction_on with
  | empty =>
    simpa only [Finset.sum_empty] using contMDiffWithinAt_zeroSection ..
  | insert i s hi h =>
    simp only [Finset.sum_insert hi]
    apply (hs _ (s.mem_insert_self i)).add_section
    exact h fun i a ↦ hs _ (s.mem_insert_of_mem a)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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
s : Finset ι
hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀
empty :
  ∀
    (hs :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, 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₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (h :
    ∀ (hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀),
      ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀)
  (hs :
    ∀ i_1 ∈ insert i s,
      ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i_1 x⟩) u x₀),
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ insert i s, t i x⟩) u x₀
Tactic: induction s using Finset.induction_on with
  | empty =>
    simpa only [Finset.sum_empty] using contMDiffWithinAt_zeroSection ..
  | insert i s hi h =>
    simp only [Finset.sum_insert hi]
    apply (hs _ (s.mem_insert_self i)).add_section
    exact h fun i a ↦ hs _ (s.mem_insert_of_mem a)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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
s : Finset ι
hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
have empty : ∀
  (hs :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, 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: classical
  induction s using Finset.induction_on with
  | empty =>
    simpa only [Finset.sum_empty] using contMDiffWithinAt_zeroSection ..
  | insert i s hi h =>
    simp only [Finset.sum_insert hi]
    apply (hs _ (s.mem_insert_self i)).add_section
    exact h fun i a ↦ hs _ (s.mem_insert_of_mem a)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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
s : Finset ι
hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀
empty :
  ∀
    (hs :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, 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₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (h :
    ∀ (hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀),
      ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀)
  (hs :
    ∀ i_1 ∈ insert i s,
      ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i_1 x⟩) u x₀),
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ insert i s, t i x⟩) u x₀
Tactic: classical
  induction s using Finset.induction_on with
  | empty =>
    simpa only [Finset.sum_empty] using contMDiffWithinAt_zeroSection ..
  | insert i s hi h =>
    simp only [Finset.sum_insert hi]
    apply (hs _ (s.mem_insert_self i)).add_section
    exact h fun i a ↦ hs _ (s.mem_insert_of_mem a)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (hypothesis)
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
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
s : Finset ι
hs : ∀ i ∈ s, ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) x₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀
have hs₁ : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) Set.univ x₀
Tactic: simp_rw [← contMDiffWithinAt_univ] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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
⊢ ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, (ψ • s) x⟩
have apply : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (ψ • s) x⟩) (tsupport ψ)ᶜ
Tactic: apply contMDiff_of_contMDiffOn_union_of_isOpen (hψ.smul_section hs) ?_ ?_ ht
      (isOpen_compl_iff.mpr <| isClosed_tsupport ψ)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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 ψ)ᶜ
⊢ ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, (ψ • s) x⟩
have apply₁ : u ∪ (tsupport ψ)ᶜ = Set.univ
Tactic: apply contMDiff_of_contMDiffOn_union_of_isOpen (hψ.smul_section hs) ?_ ?_ ht
      (isOpen_compl_iff.mpr <| isClosed_tsupport ψ)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (ψ • s) x⟩) (tsupport ψ)ᶜ
have apply : ∀ y ∈ (tsupport ψ)ᶜ, ⟨y, (ψ • s) y⟩ = zeroSection F V y
Tactic: apply ((contMDiff_zeroSection _ _).contMDiffOn (s := (tsupport ψ)ᶜ)).congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) u x₀
have 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₀
Tactic: obtain ⟨u', hu', hfin⟩ := ht x₀
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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}
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) u x₀
have 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₀
Tactic: have := hfin.fintype
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (hypothesis)
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 : ι), t i x⟩) u x₀
have this₁ : 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)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) u x₀
have apply : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) (u ∩ u') x₀
Tactic: apply (contMDiffWithinAt_inter hu').mp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) (u ∩ u') x₀
have apply : Eq (α := TotalSpace F V) ⟨x₀, ∑' (i : ι), t i x₀⟩ ⟨x₀, ∑ i ∈ s.toFinset, t i x₀⟩
Tactic: apply this.congr fun y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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₀⟩
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑' (i : ι), t i x⟩) (u ∩ u') x₀
have apply₁ : ∀ (y : M) (hy : y ∈ u ∩ u'), Eq (α := TotalSpace F V) ⟨y, ∑' (i : ι), t i y⟩ ⟨y, ∑ i ∈ s.toFinset, t i y⟩
Tactic: apply this.congr fun y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (goal)
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₀
⊢ Eq (α := TotalSpace F V) ⟨x₀, ∑' (i : ι), t i x₀⟩ ⟨x₀, ∑ i ∈ s.toFinset, t i x₀⟩
have rw : (support.{u_7, u_6} (M := V x₀) fun (i : ι) ↦ t i x₀) ⊆ (↑s.toFinset : Set ι)
Tactic: rw [TotalSpace.mk_inj, tsum_eq_sum']