-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
e' : Pretrivialization F proj
toPartialEquiv : PartialEquiv Z (B × F)
open_target : IsOpen[instTopologicalSpaceProd] toPartialEquiv.target
baseSet : Set B
open_baseSet : IsOpen[inst] baseSet
source_eq : toPartialEquiv.source = proj ⁻¹' baseSet
target_eq : toPartialEquiv.target = SProd.sprod (β := Set F) baseSet univ
proj_toFun : ∀ p ∈ toPartialEquiv.source, ((↑toPartialEquiv : Z → B × F) p).1 = proj p
h₁ :
  { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun :
        Pretrivialization F proj }.toPartialEquiv =
    e'.toPartialEquiv
h₂ :
  { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Pretrivialization F proj }.baseSet =
    e'.baseSet
mk :
  ∀ (toPartialEquiv_1 : PartialEquiv Z (B × F))
    (open_target_1 : IsOpen[instTopologicalSpaceProd] toPartialEquiv_1.target) (baseSet_1 : Set B)
    (open_baseSet_1 : IsOpen[inst] baseSet_1) (source_eq_1 : toPartialEquiv_1.source = proj ⁻¹' baseSet_1)
    (target_eq_1 : toPartialEquiv_1.target = SProd.sprod (β := Set F) baseSet_1 univ)
    (proj_toFun_1 : ∀ p ∈ toPartialEquiv_1.source, ((↑toPartialEquiv_1 : Z → B × F) p).1 = proj p)
    (h₁ :
      { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
            source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun :
            Pretrivialization F proj }.toPartialEquiv =
        { toPartialEquiv := toPartialEquiv_1, open_target := open_target_1, baseSet := baseSet_1,
            open_baseSet := open_baseSet_1, source_eq := source_eq_1, target_eq := target_eq_1,
            proj_toFun := proj_toFun_1 : Pretrivialization F proj }.toPartialEquiv)
    (h₂ :
      { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
            source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun :
            Pretrivialization F proj }.baseSet =
        { toPartialEquiv := toPartialEquiv_1, open_target := open_target_1, baseSet := baseSet_1,
            open_baseSet := open_baseSet_1, source_eq := source_eq_1, target_eq := target_eq_1,
            proj_toFun := proj_toFun_1 : Pretrivialization F proj }.baseSet),
    { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Pretrivialization F proj } =
      { toPartialEquiv := toPartialEquiv_1, open_target := open_target_1, baseSet := baseSet_1,
        open_baseSet := open_baseSet_1, source_eq := source_eq_1, target_eq := target_eq_1, proj_toFun := proj_toFun_1 }
⊢ { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
      source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Pretrivialization F proj } =
    e'

Tactic:
cases e'