-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ { 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'
have 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 }
Tactic: cases e'
Cleared hypotheses: e', h₁, h₂