awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace F
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst_3 : TopologicalSpace HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : FiberBundle F E
x : TotalSpace F E
rw :
  Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB ((↑(trivializationAt F E (x.proj (E := E))) : TotalSpace F E → B × F) x).1)
        (OpenPartialHomeomorph.refl F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
rw₁ rw₂ :
  Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
⊢ Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod
        (chartAt HB
          ((↑(Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) : TotalSpace F E → B × F)
              x).1)
        (OpenPartialHomeomorph.refl F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))

Tactic:
rw [Trivialization.coe_coe, Trivialization.coe_fst' _ (mem_baseSet_trivializationAt F E x.proj)]

Premises used: Bundle.Trivialization.coe_fst', Bundle.TotalSpace.proj, Bundle.Trivialization.coe_coe, FiberBundle.mem_baseSet_trivializationAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace F
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst_3 : TopologicalSpace HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : FiberBundle F E
x : TotalSpace F E
y : ModelProd HB F
hy : Membership.mem (γ := Set (ModelProd HB F)) (PartialEquiv.target (toPartialEquiv (chartAt (ModelProd HB F) x))) y
simp :
  ∀
    (hy :
      y ∈
        SProd.sprod (β := Set F) (toPartialEquiv (chartAt HB (x.proj (E := E)))).target univ ∩
          (fun (p : HB × F) ↦ ((↑(OpenPartialHomeomorph.symm (chartAt HB (x.proj (E := E)))) : HB → B) p.1, p.2)) ⁻¹'
            (toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))))).target),
    ((↑(OpenPartialHomeomorph.symm
                  (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
                    OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))) :
              ModelProd HB F → TotalSpace F E)
            y).proj
        (E := E) =
      (↑(OpenPartialHomeomorph.symm (chartAt HB (x.proj (E := E)))) : HB → B) y.1
⊢ ((↑(OpenPartialHomeomorph.symm (chartAt (ModelProd HB F) x)) : ModelProd HB F → TotalSpace F E) y).proj (E := E) =
    (↑(OpenPartialHomeomorph.symm (chartAt HB (x.proj (E := E)))) : HB → B) y.1

Tactic:
simp only [FiberBundle.chartedSpace_chartAt, mfld_simps] at hy ⊢

Premises used: FiberBundle.chartedSpace_chartAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace F
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst_3 : TopologicalSpace HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : FiberBundle F E
x : TotalSpace F E
y : ModelProd HB F
hy :
  y ∈
    SProd.sprod (β := Set F) (toPartialEquiv (chartAt HB (x.proj (E := E)))).target univ ∩
      (fun (p : HB × F) ↦ ((↑(OpenPartialHomeomorph.symm (chartAt HB (x.proj (E := E)))) : HB → B) p.1, p.2)) ⁻¹'
        (toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))))).target
⊢ ((↑(OpenPartialHomeomorph.symm
                (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
                  OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))) :
            ModelProd HB F → TotalSpace F E)
          y).proj
      (E := E) =
    (↑(OpenPartialHomeomorph.symm (chartAt HB (x.proj (E := E)))) : HB → B) y.1

Tactic:
(trivializationAt F E x.proj).proj_symm_apply hy.2

Premises used: OpenPartialHomeomorph.trans, PartialEquiv.symm, OpenPartialHomeomorph.toFun', Bundle.TotalSpace.proj, FiberBundle.trivializationAt, And.right, Bundle.Trivialization.proj_symm_apply, OpenPartialHomeomorph.trans', PartialEquiv.trans', OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace F
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst_3 : TopologicalSpace HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : FiberBundle F E
x : TotalSpace F E
y : ModelProd HB F
hy :
  y ∈
    SProd.sprod (β := Set F) (toPartialEquiv (chartAt HB (x.proj (E := E)))).target univ ∩
      (fun (p : HB × F) ↦ ((↑(OpenPartialHomeomorph.symm (chartAt HB (x.proj (E := E)))) : HB → B) p.1, p.2)) ⁻¹'
        (toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))))).target
⊢ ((↑(OpenPartialHomeomorph.symm
                (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
                  OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))) :
            ModelProd HB F → TotalSpace F E)
          y).proj
      (E := E) =
    (↑(OpenPartialHomeomorph.symm (chartAt HB (x.proj (E := E)))) : HB → B) y.1

Tactic:
exact (trivializationAt F E x.proj).proj_symm_apply hy.2

Premises used: Bundle.TotalSpace.proj, FiberBundle.trivializationAt, And.right, Bundle.Trivialization.proj_symm_apply
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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
simp_rw :
  toPartialEquiv
        (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
          OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F)) ≫
      ModelWithCorners.toPartialEquiv (IB.prod 𝓘(𝕜, F)) =
    toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
      (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)
⊢ extChartAt (IB.prod 𝓘(𝕜, F)) x =
    toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
      (extChartAt IB (x.proj (E := E))).prod (PartialEquiv.refl F)

Tactic:
simp_rw [extChartAt, FiberBundle.chartedSpace_chartAt, OpenPartialHomeomorph.extend]

Premises used: extChartAt, FiberBundle.chartedSpace_chartAt, OpenPartialHomeomorph.extend
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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
simp :
  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)
⊢ toPartialEquiv
        (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
          OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F)) ≫
      ModelWithCorners.toPartialEquiv (IB.prod 𝓘(𝕜, 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:
simp only [PartialEquiv.trans_assoc, mfld_simps]

Premises used: PartialEquiv.trans_assoc
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [PartialEquiv.prod_trans, PartialEquiv.refl_trans]

Premises used: PartialEquiv.prod_trans, PartialEquiv.refl_trans
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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 :
  ((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
⊢ (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

Tactic:
rw [FiberBundle.extChartAt, PartialEquiv.trans_target, Trivialization.target_eq, inter_prod]

Premises used: Bundle.Trivialization.target_eq, FiberBundle.extChartAt, Set.inter_prod, PartialEquiv.trans_target
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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 (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:
rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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
y : EB × F
hy : y ∈ (extChartAt (IB.prod 𝓘(𝕜, F)) x).target
⊢ writtenInExtChartAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) x
      (↑(trivializationAt F E (x.proj (E := E))) : TotalSpace F E → B × F) y =
    y

Tactic:
writtenInExtChartAt_chartAt_comp _ hy

Premises used: Bundle.Trivialization.toFun', OpenPartialHomeomorph.toFun', writtenInExtChartAt_chartAt_comp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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
y : EB × F
hy : y ∈ (extChartAt (IB.prod 𝓘(𝕜, F)) x).target
⊢ writtenInExtChartAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F))
      ((↑(trivializationAt F E (x.proj (E := E))) : TotalSpace F E → B × F) x)
      (↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))))) :
        B × F → TotalSpace F E)
      y =
    y

Tactic:
writtenInExtChartAt_chartAt_symm_comp _ hy

Premises used: Bundle.Trivialization.toFun', OpenPartialHomeomorph.toFun', writtenInExtChartAt_chartAt_symm_comp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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
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₀
⊢ 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₀

Tactic:
simp +singlePass only [contMDiffWithinAt_iff_target]

Premises used: contMDiffWithinAt_iff_target
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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
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₀)
⊢ 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:
rw [and_and_and_comm, ← FiberBundle.continuousWithinAt_totalSpace, and_congr_right_iff]

Premises used: FiberBundle.continuousWithinAt_totalSpace, and_congr_right_iff, and_and_and_comm
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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₀
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₀
⊢ 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:
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]

Premises used: Function.id_def, PartialEquiv.trans_apply, chartedSpaceSelf_prod, extChartAt_self_apply, FiberBundle.extChartAt, modelWithCornersSelf_prod, Function.comp_def, PartialEquiv.prod_coe, modelWithCornersSelf_coe, PartialEquiv.refl_coe