Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case mk.mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
toOpenPartialHomeomorph✝¹ : OpenPartialHomeomorph Z (B × F)
baseSet✝¹ : Set B
open_baseSet✝¹ : IsOpen[inst✝²] baseSet✝¹
source_eq✝¹ : toOpenPartialHomeomorph✝¹.source = proj ⁻¹' baseSet✝¹
target_eq✝¹ : toOpenPartialHomeomorph✝¹.target = baseSet✝¹ ×ˢ univ
proj_toFun✝¹ : ∀ p ∈ toOpenPartialHomeomorph✝¹.source, (↑toOpenPartialHomeomorph✝¹ p).1 = proj p
toOpenPartialHomeomorph✝ : OpenPartialHomeomorph Z (B × F)
baseSet✝ : Set B
open_baseSet✝ : IsOpen[inst✝²] baseSet✝
source_eq✝ : toOpenPartialHomeomorph✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toOpenPartialHomeomorph✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toOpenPartialHomeomorph✝.source, (↑toOpenPartialHomeomorph✝ 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✝¹ }.toOpenPartialHomeomorph =
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.toOpenPartialHomeomorph
h₂ :
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝¹, baseSet := baseSet✝¹, open_baseSet := open_baseSet✝¹,
        source_eq := source_eq✝¹, target_eq := target_eq✝¹, proj_toFun := proj_toFun✝¹ }.baseSet =
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.baseSet
⊢ { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝¹, baseSet := baseSet✝¹, open_baseSet := open_baseSet✝¹,
      source_eq := source_eq✝¹, target_eq := target_eq✝¹, proj_toFun := proj_toFun✝¹ } =
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
      source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }

Tactic:
;

Goal state after:
case mk.mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
toOpenPartialHomeomorph✝¹ : OpenPartialHomeomorph Z (B × F)
baseSet✝¹ : Set B
open_baseSet✝¹ : IsOpen[inst✝²] baseSet✝¹
source_eq✝¹ : toOpenPartialHomeomorph✝¹.source = proj ⁻¹' baseSet✝¹
target_eq✝¹ : toOpenPartialHomeomorph✝¹.target = baseSet✝¹ ×ˢ univ
proj_toFun✝¹ : ∀ p ∈ toOpenPartialHomeomorph✝¹.source, (↑toOpenPartialHomeomorph✝¹ p).1 = proj p
toOpenPartialHomeomorph✝ : OpenPartialHomeomorph Z (B × F)
baseSet✝ : Set B
open_baseSet✝ : IsOpen[inst✝²] baseSet✝
source_eq✝ : toOpenPartialHomeomorph✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toOpenPartialHomeomorph✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toOpenPartialHomeomorph✝.source, (↑toOpenPartialHomeomorph✝ 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✝¹ }.toOpenPartialHomeomorph =
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.toOpenPartialHomeomorph
h₂ :
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝¹, baseSet := baseSet✝¹, open_baseSet := open_baseSet✝¹,
        source_eq := source_eq✝¹, target_eq := target_eq✝¹, proj_toFun := proj_toFun✝¹ }.baseSet =
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.baseSet
⊢ { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝¹, baseSet := baseSet✝¹, open_baseSet := open_baseSet✝¹,
      source_eq := source_eq✝¹, target_eq := target_eq✝¹, proj_toFun := proj_toFun✝¹ } =
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
      source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }