-- Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
theorem FiberBundle.extChartAt (x : TotalSpace F E) :
    extChartAt (IB.prod 𝓘(𝕜, F)) x =
      (trivializationAt F E x.proj).toPartialEquiv ≫
        (extChartAt IB x.proj).prod (PartialEquiv.refl F)

Proof state:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ ((trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ
          (chartAt HB x.proj).prod (PartialHomeomorph.refl F)).toPartialEquiv ≫
      (IB.prod 𝓘(𝕜, F)).toPartialEquiv =
    (trivializationAt F E x.proj).toPartialEquiv ≫
      ((chartAt HB x.proj).toPartialEquiv ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)

Tactic:
simp only [PartialEquiv.trans_assoc, mfld_simps]

Result:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ (trivializationAt F E x.proj).toPartialEquiv ≫
      (chartAt HB x.proj).prod (PartialEquiv.refl F) ≫ IB.prod (PartialEquiv.refl F) =
    (trivializationAt F E x.proj).toPartialEquiv ≫
      ((chartAt HB x.proj).toPartialEquiv ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)

Proof state:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ (trivializationAt F E x.proj).toPartialEquiv ≫
      (chartAt HB x.proj).prod (PartialEquiv.refl F) ≫ IB.prod (PartialEquiv.refl F) =
    (trivializationAt F E x.proj).toPartialEquiv ≫
      ((chartAt HB x.proj).toPartialEquiv ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)

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

Result:
no goals

Proof state:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ extChartAt (IB.prod 𝓘(𝕜, F)) x =
    (trivializationAt F E x.proj).toPartialEquiv ≫ (extChartAt IB x.proj).prod (PartialEquiv.refl F)

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

Result:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ ((trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ
          (chartAt HB x.proj).prod (PartialHomeomorph.refl F)).toPartialEquiv ≫
      (IB.prod 𝓘(𝕜, F)).toPartialEquiv =
    (trivializationAt F E x.proj).toPartialEquiv ≫
      ((chartAt HB x.proj).toPartialEquiv ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)