awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u u' : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hu'u : u' ⊆ u
x : M
hx : x ∈ u'
⊢ LE.le.{u_6} (α := Submodule 𝕜 (V x)) ⊤ (Submodule.span 𝕜 (Set.range fun (x_1 : ι) ↦ s x_1 x))

Tactic:
exact hs.generating (hu'u hx)

Premises used: IsLocalFrameOn.generating
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
x : M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hu : IsOpen[inst_4] u
hx : x ∈ u
i : ι
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s i x⟩) x

Tactic:
(hs.contMDiffOn i).contMDiffAt <| hu.mem_nhds hx

Premises used: IsLocalFrameOn.contMDiffOn, ContMDiffOn.contMDiffAt, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
x : M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
i : ι
⊢ (hs.toBasisAt (V := V) (u := u) hx : (a : ι) → V x) i = s i x

Tactic:
simpa only [toBasisAt] using Basis.mk_apply (hs.linearIndependent hx) (hs.generating hx) i

Premises used: IsLocalFrameOn.toBasisAt, Module.Basis.mk_apply, IsLocalFrameOn.linearIndependent, IsLocalFrameOn.generating
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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_1 : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u u' : Set M
x : M
n : ℕ∞ω
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
phi : LinearEquiv.{u_1, u_1, u_6, u_5} (RingHom.id 𝕜) (V x) F :=
  Trivialization.linearEquivAt 𝕜 (E := V) (trivializationAt F V x) x ⋯
⊢ FiniteDimensional.{u_1, u_6} 𝕜 (V x)

Tactic:
Finite.equiv phi.symm

Premises used: LinearEquiv.symm, Module.Finite.equiv
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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_1 : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u u' : Set M
x : M
n : ℕ∞ω
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
phi : LinearEquiv.{u_1, u_1, u_6, u_5} (RingHom.id 𝕜) (V x) F :=
  Trivialization.linearEquivAt 𝕜 (E := V) (trivializationAt F V x) x ⋯
⊢ FiniteDimensional.{u_1, u_6} 𝕜 (V x)

Tactic:
exact Finite.equiv phi.symm

Premises used: LinearEquiv.symm, Module.Finite.equiv
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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_1 : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u u' : Set M
x : M
n : ℕ∞ω
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
⊢ FiniteDimensional.{u_1, u_6} 𝕜 (V x)

Tactic:
have : FiniteDimensional 𝕜 (V x) := by
    let phi := (trivializationAt F V x).linearEquivAt 𝕜 x
      (FiberBundle.mem_baseSet_trivializationAt' x)
    exact Finite.equiv phi.symm
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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_1 : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u u' : Set M
x : M
n : ℕ∞ω
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
this : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
⊢ Fintype ι

Tactic:
exact FiniteDimensional.fintypeBasisIndex (hs.toBasisAt hx)

Premises used: IsLocalFrameOn.toBasisAt, FiniteDimensional.fintypeBasisIndex
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∉ u
i : ι
⊢ hs.coeff (V := V) (u := u) i x = 0

Tactic:
simp [coeff, hx]

Premises used: IsLocalFrameOn.coeff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
t : (x : M) → V x
i : ι
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    (((((hs.toBasisAt (V := V) (u := u) hx).repr : (a : V x) → ι →₀ 𝕜) (t x) : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)

Tactic:
simp [coeff, hx]

Premises used: IsLocalFrameOn.coeff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
inst_13 : Fintype ι
hs : IsLocalFrameOn I F (V := V) n s u
t : (x : M) → V x
hx : x ∈ u
⊢ t x =
    ∑ i : ι, HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜) (s i x)

Tactic:
simpa [coeff, hx] using (Basis.sum_repr (hs.toBasisAt hx) (t x)).symm

Premises used: IsLocalFrameOn.toBasisAt, IsLocalFrameOn.coeff, Eq.symm, Module.Basis.sum_repr
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
inst_13 : Finite ι
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
t t' : (x : M) → V x
h :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
      ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
this : Fintype ι := Fintype.ofFinite ι
⊢ t x =
    ∑ i : ι, HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜) (s i x)

Tactic:
hs.coeff_sum_eq t hx

Premises used: IsLocalFrameOn.coeff_sum_eq
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
inst_13 : Finite ι
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
t t' : (x : M) → V x
h :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
      ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
this : Fintype ι := Fintype.ofFinite ι
⊢ Eq.{u_6 + 1} (α := V x)
    (∑ i : ι, HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜) (s i x))
    (∑ i : ι,
      HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜) (s i x))

Tactic:
simp [h]
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
inst_13 : Finite ι
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
t t' : (x : M) → V x
h :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
      ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
this : Fintype ι := Fintype.ofFinite ι
⊢ ∑ i : ι, HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜) (s i x) =
    t' x

Tactic:
(hs.coeff_sum_eq t' hx).symm

Premises used: Eq.symm, IsLocalFrameOn.coeff_sum_eq
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
inst_13 : Finite ι
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
t t' : (x : M) → V x
h :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
      ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
this : Fintype ι := Fintype.ofFinite ι
t₁ :
  Eq.{u_6 + 1} (α := V x)
    (∑ i : ι, HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜) (s i x))
    (∑ i : ι,
      HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜) (s i x))
⊢ t x = t' x

Tactic:
calc
    t x = ∑ i, hs.coeff i x (t x) • (s i x) := hs.coeff_sum_eq t hx
    _ = ∑ i, hs.coeff i x (t' x) • (s i x) := by simp [h]
    _ = t' x := (hs.coeff_sum_eq t' hx).symm

Premises used: Eq.symm, IsLocalFrameOn.coeff_sum_eq
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
inst_13 : Fintype ι
hs : IsLocalFrameOn I F (V := V) n s u
t : (x : M) → V x
hu'' : u ∈ 𝓝 x
⊢ ∀ᶠ (x' : M) in 𝓝 x,
    t x' =
      ∑ i : ι,
        HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x' : (a : V x') → 𝕜) (t x') : 𝕜) (s i x')

Tactic:
eventually_of_mem hu'' fun _ hx ↦ hs.coeff_sum_eq _ hx

Premises used: Filter.eventually_of_mem, IsLocalFrameOn.coeff_sum_eq
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t t' : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
htt' : t x = t' x
i : ι
pos :
  ∀ (hxe : x ∈ u),
    Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
      ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
neg :
  ∀ (hxe : x ∉ u),
    Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
      ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)

Tactic:
by_cases hxe : x ∈ u
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t t' : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
htt' : t x = t' x
i : ι
hxe : x ∈ u
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)

Tactic:
simp [coeff, hxe, htt']

Premises used: IsLocalFrameOn.coeff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t t' : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
htt' : t x = t' x
i : ι
hxe : x ∉ u
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)

Tactic:
simp [coeff, hxe, htt']

Premises used: IsLocalFrameOn.coeff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F (V := V) n s u
hs' : IsLocalFrameOn I F (V := V) n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
pos :
  ∀ (hxe : x ∈ u),
    Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
      ((hs'.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
neg :
  ∀ (hxe : x ∉ u),
    Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
      ((hs'.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs'.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)

Tactic:
by_cases hxe : x ∈ u
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F (V := V) n s u
hs' : IsLocalFrameOn I F (V := V) n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
hxe : x ∈ u
pos :
  Eq.{u_1 + 1} (α := 𝕜)
    (((((hs.toBasisAt (V := V) (u := u) ⋯).repr : (a : V x) → ι →₀ 𝕜) (t x) : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)
    (((((hs'.toBasisAt (V := V) (u := u) ⋯).repr : (a : V x) → ι →₀ 𝕜) (t x) : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs'.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)

Tactic:
simp [coeff, hxe]

Premises used: IsLocalFrameOn.coeff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F (V := V) n s u
hs' : IsLocalFrameOn I F (V := V) n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
hxe : x ∈ u
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (((((hs.toBasisAt (V := V) (u := u) ⋯).repr : (a : V x) → ι →₀ 𝕜) (t x) : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)
    (((((hs'.toBasisAt (V := V) (u := u) ⋯).repr : (a : V x) → ι →₀ 𝕜) (t x) : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)

Tactic:
simp_all only [toBasisAt]

Premises used: IsLocalFrameOn.toBasisAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F (V := V) n s u
hs' : IsLocalFrameOn I F (V := V) n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
hxe : x ∉ u
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs'.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)

Tactic:
simp [coeff, hxe]

Premises used: IsLocalFrameOn.coeff