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
n : ℕ∞ω
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
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_15 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
i : ι
rw :
  ContMDiffOn I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, e.localFrame (V := V) b i x⟩).2)
    e.baseSet
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, e.localFrame (V := V) b i x⟩) e.baseSet

Tactic:
rw [e.contMDiffOn_section_baseSet_iff]

Premises used: Bundle.Trivialization.contMDiffOn_section_baseSet_iff
-- 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 : ℕ∞ω
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
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_15 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
i : ι
apply : ∀ y ∈ e.baseSet, ((↑e : TotalSpace F V → M × F) ⟨y, e.localFrame (V := V) b i y⟩).2 = (b : (a : ι) → F) i
⊢ ContMDiffOn I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, e.localFrame (V := V) b i x⟩).2)
    e.baseSet

Tactic:
apply (contMDiffOn_const (c := b i)).congr

Premises used: ContMDiffOn.congr, contMDiffOn_const
-- 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 : ℕ∞ω
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
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_15 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
i : ι
y : M
hy : y ∈ e.baseSet
⊢ ((↑e : TotalSpace F V → M × F) ⟨y, e.localFrame (V := V) b i y⟩).2 = (b : (a : ι) → F) i

Tactic:
simp [hy, basisAt]

Premises used: Bundle.Trivialization.basisAt
-- 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 : ℕ∞ω
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
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_15 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
x : M
hx : x ∈ e.baseSet
⊢ LinearIndependent.{u_7, u_1, u_6} (ι := ι) 𝕜 (M := V x) (⇑(e.basisAt (V := V) b hx) : (a : ι) → V x)

Tactic:
(e.basisAt b hx).linearIndependent

Premises used: Module.Basis.linearIndependent, Bundle.Trivialization.basisAt
-- 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 : ℕ∞ω
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
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_15 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
x : M
hx : x ∈ e.baseSet
h : ∀ (x_1 : ι), e.localFrame (V := V) b x_1 x = (e.basisAt (V := V) b hx : (a : ι) → V x) x_1
⊢ LinearIndependent.{u_7, u_1, u_6} 𝕜 (M := V x) fun (x_1 : ι) ↦ e.localFrame (V := V) b x_1 x

Tactic:
convert! (e.basisAt b hx).linearIndependent

Premises used: Module.Basis.linearIndependent, Bundle.Trivialization.basisAt
-- 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 : ℕ∞ω
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
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_15 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
x : M
hx : x ∈ e.baseSet
x_1 : ι
⊢ e.localFrame (V := V) b x_1 x = (e.basisAt (V := V) b hx : (a : ι) → V x) x_1

Tactic:
simp [hx, basisAt]

Premises used: Bundle.Trivialization.basisAt
-- 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 : ℕ∞ω
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
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_15 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
x : M
hx : x ∈ e.baseSet
⊢ LE.le.{u_6} (α := Submodule 𝕜 (V x)) ⊤
    (Submodule.span 𝕜 (Set.range.{u_6, u_7 + 1} (ι := ι) (⇑(e.basisAt (V := V) b hx) : (a : ι) → V x)))

Tactic:
(e.basisAt b hx).span_eq.ge

Premises used: Eq.ge, Module.Basis.span_eq, Bundle.Trivialization.basisAt
-- 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 : ℕ∞ω
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
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_15 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
x : M
hx : x ∈ e.baseSet
h : ∀ (x_1 : ι), e.localFrame (V := V) b x_1 x = (e.basisAt (V := V) b hx : (a : ι) → V x) x_1
⊢ LE.le.{u_6} (α := Submodule 𝕜 (V x)) ⊤ (Submodule.span 𝕜 (Set.range fun (x_1 : ι) ↦ e.localFrame (V := V) b x_1 x))

Tactic:
convert! (e.basisAt b hx).span_eq.ge

Premises used: Eq.ge, Module.Basis.span_eq, Bundle.Trivialization.basisAt
-- 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 : ℕ∞ω
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
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle n F V I
ι : Type u_7
x : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_15 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
i : ι
hx : x ∈ e.baseSet
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, e.localFrame (V := V) b i x⟩) x

Tactic:
(e.isLocalFrameOn_localFrame_baseSet I n b).contMDiffAt e.open_baseSet hx _

Premises used: Bundle.Trivialization.open_baseSet, IsLocalFrameOn.contMDiffAt, Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet
-- 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
inst_13 : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_14 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
inst_15 : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∉ e.baseSet
i : ι
⊢ Eq (α := LinearMap.{u_1, u_1, u_6, u_1} (RingHom.id 𝕜) (V x) 𝕜) (localFrame_coeff I (V := V) e b i x) 0

Tactic:
simpa [localFrame_coeff] using
    (e.isLocalFrameOn_localFrame_baseSet I 1 b).coeff_apply_of_notMem hx i

Premises used: IsLocalFrameOn.coeff_apply_of_notMem, Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet, Bundle.Trivialization.localFrame_coeff, OfNat.ofNat
-- 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
inst_13 : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_14 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
inst_15 : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ e.baseSet
s : (x : M) → V x
i : ι
⊢ IsLocalFrameOn I F (V := V) 1 (e.localFrame (V := V) b) e.baseSet

Tactic:
have he := e.isLocalFrameOn_localFrame_baseSet I 1 b
-- 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
inst_13 : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_14 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
inst_15 : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ e.baseSet
s : (x : M) → V x
i : ι
he : IsLocalFrameOn I F (V := V) 1 (e.localFrame (V := V) b) e.baseSet
a :
  ∀ (j : ι),
    Eq.{u_6 + 1} (α := V x) ((e.basisAt (V := V) b hx : (a : ι) → V x) j : V x)
      ((he.toBasisAt (V := V) (u := e.baseSet) hx : (a : ι) → V x) j : V x)
⊢ e.basisAt (V := V) b hx = he.toBasisAt (V := V) (u := e.baseSet) hx

Tactic:
ext j
-- 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
inst_13 : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_14 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
inst_15 : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ e.baseSet
s : (x : M) → V x
i : ι
he : IsLocalFrameOn I F (V := V) 1 (e.localFrame (V := V) b) e.baseSet
j : ι
⊢ Eq.{u_6 + 1} (α := V x) ((e.basisAt (V := V) b hx : (a : ι) → V x) j : V x)
    ((he.toBasisAt (V := V) (u := e.baseSet) hx : (a : ι) → V x) j : V x)

Tactic:
simp [IsLocalFrameOn.toBasisAt, localFrame, basisAt, hx]

Premises used: IsLocalFrameOn.toBasisAt, Bundle.Trivialization.localFrame, Bundle.Trivialization.basisAt
-- 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
inst_13 : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_14 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
inst_15 : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ e.baseSet
s : (x : M) → V x
i : ι
he : IsLocalFrameOn I F (V := V) 1 (e.localFrame (V := V) b) e.baseSet
⊢ e.basisAt (V := V) b hx = he.toBasisAt (V := V) (u := e.baseSet) hx

Tactic:
have hbasis : e.basisAt b hx = he.toBasisAt hx := by
    ext j
    simp [IsLocalFrameOn.toBasisAt, localFrame, basisAt, hx]
-- 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
inst_13 : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_14 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
inst_15 : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ e.baseSet
s : (x : M) → V x
i : ι
he : IsLocalFrameOn I F (V := V) 1 (e.localFrame (V := V) b) e.baseSet
hbasis : e.basisAt (V := V) b hx = he.toBasisAt (V := V) (u := e.baseSet) hx
⊢ Eq.{u_1 + 1} (α := 𝕜) ((localFrame_coeff I (V := V) e b i x : (a : V x) → 𝕜) (s x) : 𝕜)
    ((((Basis.repr (e.basisAt (V := V) b hx) : (a : V x) → ι →₀ 𝕜) (s x) : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)

Tactic:
simp [localFrame_coeff, IsLocalFrameOn.coeff, hx, hbasis]

Premises used: IsLocalFrameOn.coeff, Bundle.Trivialization.localFrame_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
inst_13 : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_14 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
inst_15 : ContMDiffVectorBundle 1 F V I
x' : M
s : (x : M) → V x
inst_16 : Fintype ι
hx : x' ∈ e.baseSet
⊢ s x' =
    ∑ i : ι,
      HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((localFrame_coeff I (V := V) e b i x' : (a : V x') → 𝕜) (s x') : 𝕜)
        (e.localFrame (V := V) b i x')

Tactic:
(isLocalFrameOn_localFrame_baseSet I 1 e b).coeff_sum_eq s hx

Premises used: Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet, OfNat.ofNat, 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
inst_13 : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_14 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
inst_15 : ContMDiffVectorBundle 1 F V I
x : M
s : (x : M) → V x
inst_16 : Fintype ι
hxe : x ∈ e.baseSet
⊢ ∀ᶠ (x' : M) in 𝓝 x,
    s x' =
      ∑ i : ι,
        HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((localFrame_coeff I (V := V) e b i x' : (a : V x') → 𝕜) (s x') : 𝕜)
          (e.localFrame (V := V) b i x')

Tactic:
eventually_nhds_iff.mpr ⟨e.baseSet, fun _ ↦ e.eq_sum_localFrame_coeff_smul, e.open_baseSet, hxe⟩

Premises used: Iff.mpr, Bundle.Trivialization.eq_sum_localFrame_coeff_smul, Bundle.Trivialization.open_baseSet, eventually_nhds_iff, And.intro, Exists.intro, Bundle.Trivialization.baseSet
-- 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
inst_13 : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_14 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
inst_15 : ContMDiffVectorBundle 1 F V I
x : M
s s' : (x : M) → V x
i : ι
hss' : s x = s' x
⊢ Eq.{u_1 + 1} (α := 𝕜) ((localFrame_coeff I (V := V) e b i x : (a : V x) → 𝕜) (s x) : 𝕜)
    ((localFrame_coeff I (V := V) e b i x : (a : V x) → 𝕜) (s' x) : 𝕜)

Tactic:
simpa using (isLocalFrameOn_localFrame_baseSet I 1 e b).coeff_congr hss' i

Premises used: IsLocalFrameOn.coeff_congr, Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet, OfNat.ofNat
-- 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
inst_13 : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_14 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
inst_15 : ContMDiffVectorBundle 1 F V I
x : M
s : (x : M) → V x
hxe : x ∈ e.baseSet
i : ι
⊢ Eq.{u_1 + 1} (α := 𝕜) ((localFrame_coeff I (V := V) e b i x : (a : V x) → 𝕜) (s x) : 𝕜)
    ((((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2 : ι →₀ 𝕜) :
          (a : ι) → 𝕜)
        i :
      𝕜)

Tactic:
simp [e.localFrame_coeff_apply_of_mem_baseSet b hxe, basisAt]

Premises used: Bundle.Trivialization.basisAt, Bundle.Trivialization.localFrame_coeff_apply_of_mem_baseSet
-- 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
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle 1 F V I
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_15 : MemTrivializationAtlas (E := V) e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
k : ℕ∞ω
x : M
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
inst_18 : ContMDiffVectorBundle k F V I
hxe : x ∈ e.baseSet
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x : M) ↦ ⟨x, s x⟩) x
i : ι
aux : (x : M) → 𝕜 :=
  fun (x : M) ↦
    (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2 : ι →₀ 𝕜) :
        (a : ι) → 𝕜)
      i
this : ContMDiffAt I 𝓘(𝕜, 𝕜) k aux x
apply :
  (((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
            (Trivialization.localFrame_coeff I (V := V) e b i) :
          ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
        (a : (x : M) → V x) → M → 𝕜)
      s =ᶠ[𝓝 x]
    aux
⊢ ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) k
    ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
            (Trivialization.localFrame_coeff I (V := V) e b i) :
          ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
        (a : (x : M) → V x) → M → 𝕜)
      s)
    x

Tactic:
apply this.congr_of_eventuallyEq ?_

Premises used: ContMDiffAt.congr_of_eventuallyEq