awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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 : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      x
hu : IsOpen[inst_4] u
hx : x ∈ u
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x
have have : ∀ (this : Fintype ι), ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x
Tactic: have := fintypeOfFiniteDimensional hs hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
⊢ MDiff[u] (T% t)
have inl : ∀ (hs : IsLocalFrameOn I F (V := V) 1 s ∅)
  (h :
    ∀ (i : ι),
      MDiff[∅]
        ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                (hs.coeff (V := V) (u := ∅) i) :
              ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
            (a : (x : M) → V x) → M → 𝕜)
          t)),
  MDiff[∅] (T% t)
Tactic: rcases u.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
Cleared hypotheses: u, hs, h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
inl :
  ∀ (hs : IsLocalFrameOn I F (V := V) 1 s ∅)
    (h :
      ∀ (i : ι),
        MDiff[∅]
          ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                  (hs.coeff (V := V) (u := ∅) i) :
                ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
              (a : (x : M) → V x) → M → 𝕜)
            t)),
    MDiff[∅] (T% t)
⊢ MDiff[u] (T% t)
have inr : ∀ (x : M) (hx : x ∈ u), MDiff[u] (T% t)
Tactic: rcases u.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
x : M
hx : x ∈ u
⊢ MDiff[u] (T% t)
have inr : ∀ (this : Fintype ι), MDiff[u] (T% t)
Tactic: have := fintypeOfFiniteDimensional hs hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
x : M
hx : x ∈ u
this : Fintype ι
⊢ MDiff[u] (T% t)
have this₁ : ∀ (i : ι),
  MDiff[u] fun (x : M) ↦
    ⟨x,
      HSMul.hSMul (α := M → 𝕜)
        ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                  (hs.coeff (V := V) (u := u) i) :
                ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
              (a : (x : M) → V x) → M → 𝕜)
            t :
          M → 𝕜)
        (s i) x⟩
Tactic: have this (i) : MDiff[u] (T% ((LinearMap.piApply (hs.coeff i)) t • s i)) :=
    (h i).smul_section ((hs.contMDiffOn i).mdifferentiableOn one_ne_zero)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
x : M
hx : x ∈ u
this_1 : Fintype ι
this :
  ∀ (i : ι),
    MDiff[u] fun (x : M) ↦
      ⟨x,
        HSMul.hSMul (α := M → 𝕜)
          ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                    (hs.coeff (V := V) (u := u) i) :
                  ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                (a : (x : M) → V x) → M → 𝕜)
              t :
            M → 𝕜)
          (s i) x⟩
⊢ MDiff[u] (T% t)
have almost : MDiff[u] fun (x : M) ↦
  ⟨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: have almost : MDiff[u] (T% (fun x ↦ ∑ i, hs.coeff i x (t x) • s i x)) :=
    .sum_section (fun i _ hx ↦ this i _ hx)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
x : M
hx : x ∈ u
this_1 : Fintype ι
this :
  ∀ (i : ι),
    MDiff[u] fun (x : M) ↦
      ⟨x,
        HSMul.hSMul (α := M → 𝕜)
          ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                    (hs.coeff (V := V) (u := u) i) :
                  ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                (a : (x : M) → V x) → M → 𝕜)
              t :
            M → 𝕜)
          (s i) x⟩
almost :
  MDiff[u] fun (x : M) ↦
    ⟨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)⟩
⊢ MDiff[u] (T% t)
have inr : ∀ y ∈ u,
  ⟨y, t y⟩ =
    ⟨y,
      ∑ i : ι,
        HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i y : (a : V y) → 𝕜) (t y) : 𝕜) (s i y)⟩
Tactic: apply almost.congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiffAt
        ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                (hs.coeff (V := V) (u := u) i) :
              ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
            (a : (x : M) → V x) → M → 𝕜)
          t)
      x
hu : u ∈ 𝓝 x
⊢ MDiffAt (T% t) x
have have : ∀ (this : Fintype ι), MDiffAt (T% t) x
Tactic: have := fintypeOfFiniteDimensional hs (mem_of_mem_nhds hu)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiffAt
        ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                (hs.coeff (V := V) (u := u) i) :
              ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
            (a : (x : M) → V x) → M → 𝕜)
          t)
      x
hu : u ∈ 𝓝 x
this : Fintype ι
⊢ MDiffAt (T% t) x
have almost : (MDiffAt fun (x : M) ↦
    ⟨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)⟩)
  x
Tactic: have almost : MDiffAt (T% (fun x ↦ ∑ i, hs.coeff i x (t x) • s i x)) x :=
    .sum_section (fun i ↦ (h i).smul_section <|
      ((hs.contMDiffOn i).mdifferentiableOn one_ne_zero).mdifferentiableAt hu)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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) → 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 : ι
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, e.localFrame (V := V) b i x⟩) e.baseSet
have 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
Tactic: rw [e.contMDiffOn_section_baseSet_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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) → 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 : ι
⊢ 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
have apply : ∀ y ∈ e.baseSet, ((↑e : TotalSpace F V → M × F) ⟨y, e.localFrame (V := V) b i y⟩).2 = (b : (a : ι) → F) i
Tactic: apply (contMDiffOn_const (c := b i)).congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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) → 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) fun (x_1 : ι) ↦ e.localFrame (V := V) b x_1 x
have h : ∀ (x_1 : ι), e.localFrame (V := V) b x_1 x = (e.basisAt (V := V) b hx : (a : ι) → V x) x_1
Tactic: convert! (e.basisAt b hx).linearIndependent
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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) → 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 fun (x_1 : ι) ↦ e.localFrame (V := V) b x_1 x))
have h : ∀ (x_1 : ι), e.localFrame (V := V) b x_1 x = (e.basisAt (V := V) b hx : (a : ι) → V x) x_1
Tactic: convert! (e.basisAt b hx).span_eq.ge
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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 : ι
⊢ 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 : 𝕜)
have he : IsLocalFrameOn I F (V := V) 1 (e.localFrame (V := V) b) e.baseSet
Tactic: have he := e.isLocalFrameOn_localFrame_baseSet I 1 b
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
have 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)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
⊢ 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 : 𝕜)
have hbasis : 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
⊢ 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
have 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
Tactic: apply this.congr_of_eventuallyEq ?_