awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
x : TotalSpace F E
rw :
  toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
      (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod
        (PartialEquiv.refl F ≫ PartialEquiv.refl F) =
    toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
      (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)
⊢ toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
      (toPartialEquiv (chartAt HB (x.proj (E := E)))).prod (PartialEquiv.refl F) ≫ IB.prod (PartialEquiv.refl F) =
    toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
      (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)
have rw₁ : toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
    (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F) =
  toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
    (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)
Tactic: rw [PartialEquiv.prod_trans, PartialEquiv.refl_trans]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
x : TotalSpace F E
⊢ (extChartAt (IB.prod 𝓘(𝕜, F)) x).target =
    SProd.sprod (β := Set F)
      ((extChartAt IB (x.proj (E := E))).target ∩
        (↑(extChartAt IB (x.proj (E := E))).symm : EB → B) ⁻¹'
          Trivialization.baseSet (trivializationAt F E (x.proj (E := E))))
      univ
have rw : ((extChartAt IB (x.proj (E := E))).prod (PartialEquiv.refl F)).target ∩
    (↑((extChartAt IB (x.proj (E := E))).prod (PartialEquiv.refl F)).symm : EB × F → B × F) ⁻¹'
      SProd.sprod (β := Set F) (Trivialization.baseSet (trivializationAt F E (x.proj (E := E)))) univ =
  SProd.sprod (β := Set F) (extChartAt IB (x.proj (E := E))).target univ ∩
    SProd.sprod (β := Set F)
      ((↑(extChartAt IB (x.proj (E := E))).symm : EB → B) ⁻¹'
        Trivialization.baseSet (trivializationAt F E (x.proj (E := E))))
      univ
Tactic: rw [FiberBundle.extChartAt, PartialEquiv.trans_target, Trivialization.target_eq, inter_prod]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x₀ ↔
    ContMDiffWithinAt.{u_1, u_10, u_11, u_5, u_7, u_8, u_2} IM IB (M' := B) n (fun (x : M) ↦ (f x).proj (E := E)) s x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n
        (fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) s x₀
have simp : ContinuousWithinAt f s x₀ ∧
    ContMDiffWithinAt IM (E' := EB × F) 𝓘(𝕜, EB × F) n
      ((↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) : TotalSpace F E → EB × F) ∘ f) s x₀ ↔
  (ContinuousWithinAt.{u_5, u_2} (Y := B) (fun (x : M) ↦ (f x).proj (E := E)) s x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, EB) n
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ∘ fun (x : M) ↦ (f x).proj (E := E)) s x₀) ∧
    ContinuousWithinAt.{u_5, u_4} (Y := F)
        (fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) s x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) n
        ((↑(extChartAt 𝓘(𝕜, F) ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x₀)).2) :
            F → F) ∘
          fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2)
        s x₀
Tactic: simp +singlePass only [contMDiffWithinAt_iff_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
⊢ ContinuousWithinAt f s x₀ ∧
      ContMDiffWithinAt IM (E' := EB × F) 𝓘(𝕜, EB × F) n
        ((↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) : TotalSpace F E → EB × F) ∘ f) s x₀ ↔
    (ContinuousWithinAt.{u_5, u_2} (Y := B) (fun (x : M) ↦ (f x).proj (E := E)) s x₀ ∧
        ContMDiffWithinAt IM 𝓘(𝕜, EB) n
          ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ∘ fun (x : M) ↦ (f x).proj (E := E)) s x₀) ∧
      ContinuousWithinAt.{u_5, u_4} (Y := F)
          (fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) s x₀ ∧
        ContMDiffWithinAt IM 𝓘(𝕜, F) n
          ((↑(extChartAt 𝓘(𝕜, F) ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x₀)).2) :
              F → F) ∘
            fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2)
          s x₀
have rw : ContinuousWithinAt f s x₀ →
  (ContMDiffWithinAt IM (E' := EB × F) 𝓘(𝕜, EB × F) n
      ((↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) : TotalSpace F E → EB × F) ∘ f) s x₀ ↔
    ContMDiffWithinAt IM 𝓘(𝕜, EB) n
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ∘ fun (x : M) ↦ (f x).proj (E := E)) s x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) n
        ((↑(extChartAt 𝓘(𝕜, F) ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x₀)).2) :
            F → F) ∘
          fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2)
        s x₀)
Tactic: rw [and_and_and_comm, ← FiberBundle.continuousWithinAt_totalSpace, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ ContMDiffWithinAt IM (E' := EB × F) 𝓘(𝕜, EB × F) n
      ((↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) : TotalSpace F E → EB × F) ∘ f) s x₀ ↔
    ContMDiffWithinAt IM 𝓘(𝕜, EB) n
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ∘ fun (x : M) ↦ (f x).proj (E := E)) s x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) n
        ((↑(extChartAt 𝓘(𝕜, F) ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x₀)).2) :
            F → F) ∘
          fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2)
        s x₀
have simp_rw : ContMDiffWithinAt IM (ModelWithCorners.prod 𝓘(𝕜, EB) 𝓘(𝕜, F)) (M' := EB × F) n
    (fun (x : M) ↦
      ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).1,
        ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
              TotalSpace F E → B × F)
            (f x)).2))
    s x₀ ↔
  ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
      (fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) s x₀ ∧
    ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n
      (fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) s x₀
Tactic: simp_rw +instances [modelWithCornersSelf_prod, FiberBundle.extChartAt, Function.comp_def,
    PartialEquiv.trans_apply, PartialEquiv.prod_coe, PartialEquiv.refl_coe,
    extChartAt_self_apply, modelWithCornersSelf_coe, Function.id_def, ← chartedSpaceSelf_prod]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ ContMDiffWithinAt IM (ModelWithCorners.prod 𝓘(𝕜, EB) 𝓘(𝕜, F)) (M' := EB × F) n
      (fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      s x₀ ↔
    ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
        (fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) s x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n
        (fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) s x₀
have refine : ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
    (Function.comp (β := EB × F) Prod.fst fun (x : M) ↦
      ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).1,
        ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
              TotalSpace F E → B × F)
            (f x)).2))
    s x₀ ↔
  ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
    (fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) s x₀
Tactic: refine (contMDiffWithinAt_prod_iff _).trans (and_congr ?_ Iff.rfl)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
      (Function.comp (β := EB × F) Prod.fst fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      s x₀ ↔
    ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
      (fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) s x₀
have h1 : (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
Tactic: have h1 : (fun x => (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀ :=
    ((FiberBundle.continuous_proj F E).continuousWithinAt.comp hf (mapsTo_image f s))
      ((Trivialization.open_baseSet _).mem_nhds (mem_baseSet_trivializationAt F E _))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
⊢ ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
      (Function.comp (β := EB × F) Prod.fst fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      s x₀ ↔
    ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
      (fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) s x₀
have refine_1 : ∀ (x : M)
  (hx :
    Membership.mem (γ := Set M)
      ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))) x),
  Eq.{u_7 + 1} (α := EB)
    (Function.comp (β := EB × F) Prod.fst
      (fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      x)
    ((fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) x)
Tactic: refine EventuallyEq.contMDiffWithinAt_iff (eventually_of_mem h1 fun x hx => ?_) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
refine_1 :
  ∀ (x : M)
    (hx :
      Membership.mem (γ := Set M)
        ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))))
        x),
    Eq.{u_7 + 1} (α := EB)
      (Function.comp (β := EB × F) Prod.fst
        (fun (x : M) ↦
          ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
              ((↑(toPartialEquiv
                        (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                    TotalSpace F E → B × F)
                  (f x)).1,
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).2))
        x)
      ((fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) x)
⊢ ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
      (Function.comp (β := EB × F) Prod.fst fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      s x₀ ↔
    ContMDiffWithinAt IM 𝓘(𝕜, EB) (M' := EB) n
      (fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) s x₀
have refine_2 : Function.comp (β := EB × F) Prod.fst
    (fun (x : M) ↦
      ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).1,
        ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
              TotalSpace F E → B × F)
            (f x)).2))
    x₀ =
  (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x₀).proj (E := E))
Tactic: refine EventuallyEq.contMDiffWithinAt_iff (eventually_of_mem h1 fun x hx => ?_) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
x : M
hx :
  Membership.mem (γ := Set M)
    ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))) x
⊢ Eq.{u_7 + 1} (α := EB)
    (Function.comp (β := EB × F) Prod.fst
      (fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      x)
    ((fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) x)
have refine_1 : (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
    ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).1 =
  (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))
Tactic: simp_rw [Function.comp, OpenPartialHomeomorph.coe_coe, Trivialization.coe_coe]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
x : M
hx :
  Membership.mem (γ := Set M)
    ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))) x
⊢ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
      ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).1 =
    (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))
have refine_1 : (f x).proj (E := E) ∈ Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))
Tactic: rw [Trivialization.coe_fst']