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
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
⊢ (((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
have apply : Set.EqOn
  ((((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)
  aux e.baseSet
Tactic: apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe])
-- 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
⊢ 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 suffices : ContMDiffAt I 𝓘(𝕜, 𝕜) k aux x
Tactic: suffices CMDiffAt k aux x by
    apply this.congr_of_eventuallyEq ?_
    apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe])
    intro y hy
    simp [aux, e.localFrame_coeff_eq_coeff hy]
-- 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
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
⊢ ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) k
    (fun (x : M) ↦ (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2 : ι →₀ 𝕜) : (a : ι) → 𝕜) i)
    x
have h₁ : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2) x
Tactic: have h₁ : CMDiffAt k (fun x ↦ (e ((T% s) x)).2) x := by
    simpa using (e.contMDiffAt_section_iff hxe).1 hs
-- 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
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
h₁ : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2) x
breprl : F →ₗ[𝕜] 𝕜 :=
  { toFun := fun (v : F) ↦ (((b.repr : (a : F) → ι →₀ 𝕜) v : ι →₀ 𝕜) : (a : ι) → 𝕜) i, map_add' := ⋯, map_smul' := ⋯ }
⊢ ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) k
    (fun (x : M) ↦ (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2 : ι →₀ 𝕜) : (a : ι) → 𝕜) i)
    x
have this : ContMDiffAt 𝓘(𝕜, F) 𝓘(𝕜, 𝕜) (M' := 𝕜) k
  (⇑(((LinearMap.toContinuousLinearMap.{u_1, u_5, u_1} (𝕜 := 𝕜) (E := F) (F' := 𝕜) : (F →ₗ[𝕜] 𝕜) ≃ₗ[𝕜] F →L[𝕜] 𝕜) :
            (a : F →ₗ[𝕜] 𝕜) → F →L[𝕜] 𝕜)
          breprl :
        F →L[𝕜] 𝕜) :
    (a : F) → 𝕜)
  ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2
Tactic: have : ContMDiffAt 𝓘(𝕜, F) 𝓘(𝕜) k breprl.toContinuousLinearMap (e ((T% s) x)).2 :=
    contMDiffAt_iff_contDiffAt.mpr <| by fun_prop
-- 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 : ι
step step₁ step₂ :
  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
⊢ 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 step₃ : let 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;
ContMDiffAt I 𝓘(𝕜, 𝕜) k aux x
Tactic: classical
  -- step 1: on e.baseSet, we know compute the coefficient very well
  let aux := fun x ↦ b.repr (e ((T% s) x)).2 i
  -- Since `e.baseSet` is open, this is sufficient.
  suffices CMDiffAt k aux x by
    apply this.congr_of_eventuallyEq ?_
    apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe])
    intro y hy
    simp [aux, e.localFrame_coeff_eq_coeff hy]
  simp only [aux]
  -- step 2: `s` read in trivialization `e` is `C^k`
  have h₁ : CMDiffAt k (fun x ↦ (e ((T% s) x)).2) x := by
    simpa using (e.contMDiffAt_section_iff hxe).1 hs
  -- step 3: `b.repr` is a linear map, so the composition is smooth
  let breprl : F →ₗ[𝕜] 𝕜 :=
    { toFun v := b.repr v i
      map_add' m m' := by simp
      map_smul' m x := by simp }
  have : ContMDiffAt 𝓘(𝕜, F) 𝓘(𝕜) k breprl.toContinuousLinearMap (e ((T% s) x)).2 :=
    contMDiffAt_iff_contDiffAt.mpr <| by fun_prop
  exact this.comp x 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
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
t : Set M
k : ℕ∞ω
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
inst_18 : ContMDiffVectorBundle k F V I
ht : IsOpen[inst_4] t
ht' : t ⊆ e.baseSet
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x : M) ↦ ⟨x, s x⟩) t ↔
    ∀ (i : ι),
      ContMDiffOn 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)
        t
have refine : ∀
  (h :
    ∀ (i : ι),
      ContMDiffOn 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)
        t)
  (x : M) (hx : x ∈ t), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x : M) ↦ ⟨x, s x⟩) t x
Tactic: refine ⟨fun h i ↦ contMDiffOn_localFrame_coeff b ht ht' h _, fun h 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
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 : ℕ∞ω
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
inst_18 : ContMDiffVectorBundle k F V I
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x : M) ↦ ⟨x, s x⟩) e.baseSet ↔
    ∀ (i : ι),
      ContMDiffOn 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)
        e.baseSet
have rw : (∀ (i : ι),
    ContMDiffOn 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)
      e.baseSet) ↔
  ∀ (i : ι),
    ContMDiffOn 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)
      e.baseSet
Tactic: rw [contMDiffOn_iff_localFrame_coeff b e.open_baseSet (subset_refl _)]
-- 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
x : M
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) 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 : MDiffAt aux x
⊢ MDiffAt
      ((((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
-- 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
x : M
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) 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 : MDiffAt aux x
⊢ (((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
have apply : Set.EqOn
  ((((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)
  aux e.baseSet
Tactic: apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe])
-- 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
x : M
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) 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
⊢ MDiffAt
      ((((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 suffices : MDiffAt aux x
Tactic: suffices MDiffAt aux x by
    apply this.congr_of_eventuallyEq
    apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe])
    intro y hy
    simp [aux, e.localFrame_coeff_eq_coeff hy]
-- 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
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
x : M
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) 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
⊢ (MDiffAt fun (x : M) ↦
      (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2 : ι →₀ 𝕜) : (a : ι) → 𝕜) i)
    x
have h₁ : (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2) x
Tactic: have h₁ : MDiffAt (fun x ↦ (e ((T% s) x)).2) x := by
    simpa using (e.mdifferentiableAt_section_iff I s hxe).1 hs
-- 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
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
x : M
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) 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
h₁ : (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2) x
breprl : F →ₗ[𝕜] 𝕜 :=
  { toFun := fun (v : F) ↦ (((b.repr : (a : F) → ι →₀ 𝕜) v : ι →₀ 𝕜) : (a : ι) → 𝕜) i, map_add' := ⋯, map_smul' := ⋯ }
⊢ (MDiffAt fun (x : M) ↦
      (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2 : ι →₀ 𝕜) : (a : ι) → 𝕜) i)
    x
have this : MDiffAt
    (⇑(((LinearMap.toContinuousLinearMap.{u_1, u_5, u_1} (𝕜 := 𝕜) (E := F) (F' := 𝕜) : (F →ₗ[𝕜] 𝕜) ≃ₗ[𝕜] F →L[𝕜] 𝕜) :
              (a : F →ₗ[𝕜] 𝕜) → F →L[𝕜] 𝕜)
            breprl :
          F →L[𝕜] 𝕜) :
      (a : F) → 𝕜)
  ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2
Tactic: have : MDifferentiableAt 𝓘(𝕜, F) 𝓘(𝕜) breprl.toContinuousLinearMap (e ((T% s) x)).2 :=
    mdifferentiableAt_iff_differentiableAt.mpr <| by fun_prop