-- 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
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
⊢ { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
      source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Trivialization F proj } =
    e'
have 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 }
Tactic: cases e'
Cleared hypotheses: e', h₁, h₂