-- 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
inst_2 : TopologicalSpace Z
e' : Trivialization F proj
toOpenPartialHomeomorph : OpenPartialHomeomorph Z (B × F)
baseSet : Set B
open_baseSet : IsOpen[inst] baseSet
source_eq : toOpenPartialHomeomorph.source = proj ⁻¹' baseSet
target_eq : toOpenPartialHomeomorph.target = SProd.sprod (β := Set F) baseSet univ
proj_toFun : ∀ p ∈ toOpenPartialHomeomorph.source, ((↑toOpenPartialHomeomorph : Z → B × F) p).1 = proj p
h₁ :
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun :
        Trivialization F proj }.toOpenPartialHomeomorph =
    e'.toOpenPartialHomeomorph
h₂ :
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Trivialization F proj }.baseSet =
    e'.baseSet
mk :
  ∀ (toOpenPartialHomeomorph_1 : OpenPartialHomeomorph Z (B × F)) (baseSet_1 : Set B)
    (open_baseSet_1 : IsOpen[inst] baseSet_1) (source_eq_1 : toOpenPartialHomeomorph_1.source = proj ⁻¹' baseSet_1)
    (target_eq_1 : toOpenPartialHomeomorph_1.target = SProd.sprod (β := Set F) baseSet_1 univ)
    (proj_toFun_1 : ∀ p ∈ toOpenPartialHomeomorph_1.source, ((↑toOpenPartialHomeomorph_1 : Z → B × F) p).1 = proj p)
    (h₁ :
      { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
            source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun :
            Trivialization F proj }.toOpenPartialHomeomorph =
        { toOpenPartialHomeomorph := toOpenPartialHomeomorph_1, baseSet := baseSet_1, open_baseSet := open_baseSet_1,
            source_eq := source_eq_1, target_eq := target_eq_1, proj_toFun := proj_toFun_1 :
            Trivialization F proj }.toOpenPartialHomeomorph)
    (h₂ :
      { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
            source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Trivialization F proj }.baseSet =
        { toOpenPartialHomeomorph := toOpenPartialHomeomorph_1, baseSet := baseSet_1, open_baseSet := open_baseSet_1,
            source_eq := source_eq_1, target_eq := target_eq_1, proj_toFun := proj_toFun_1 :
            Trivialization F proj }.baseSet),
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Trivialization F proj } =
      { toOpenPartialHomeomorph := toOpenPartialHomeomorph_1, baseSet := baseSet_1, open_baseSet := open_baseSet_1,
        source_eq := source_eq_1, target_eq := target_eq_1, proj_toFun := proj_toFun_1 }
⊢ { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
      source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Trivialization F proj } =
    e'

Tactic:
cases e'