-- Mathlib/Topology/FiberBundle/Trivialization.lean
@[ext]
lemma ext' (e e' : Pretrivialization F proj) (h₁ : e.toPartialEquiv = e'.toPartialEquiv)
    (h₂ : e.baseSet = e'.baseSet) : e = e'

Proof state:
case mk.mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
toPartialEquiv✝¹ : PartialEquiv Z (B × F)
open_target✝¹ : IsOpen toPartialEquiv✝¹.target
baseSet✝¹ : Set B
open_baseSet✝¹ : IsOpen baseSet✝¹
source_eq✝¹ : toPartialEquiv✝¹.source = proj ⁻¹' baseSet✝¹
target_eq✝¹ : toPartialEquiv✝¹.target = baseSet✝¹ ×ˢ univ
proj_toFun✝¹ : ∀ p ∈ toPartialEquiv✝¹.source, (↑toPartialEquiv✝¹ p).1 = proj p
toPartialEquiv✝ : PartialEquiv Z (B × F)
open_target✝ : IsOpen toPartialEquiv✝.target
baseSet✝ : Set B
open_baseSet✝ : IsOpen baseSet✝
source_eq✝ : toPartialEquiv✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toPartialEquiv✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toPartialEquiv✝.source, (↑toPartialEquiv✝ 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✝¹ }.toPartialEquiv =
    { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝,
        open_baseSet := open_baseSet✝, source_eq := source_eq✝, target_eq := target_eq✝,
        proj_toFun := proj_toFun✝ }.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✝¹ }.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✝ }.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✝¹ } =
    { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝,
      open_baseSet := open_baseSet✝, source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }

Tactic:
congr

Result:
no goals

Proof state:
case mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e' : Pretrivialization F proj
toPartialEquiv✝ : PartialEquiv Z (B × F)
open_target✝ : IsOpen toPartialEquiv✝.target
baseSet✝ : Set B
open_baseSet✝ : IsOpen baseSet✝
source_eq✝ : toPartialEquiv✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toPartialEquiv✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toPartialEquiv✝.source, (↑toPartialEquiv✝ 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✝ }.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✝ }.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✝ } =
    e'

Tactic:
cases e'

Result:
case mk.mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
toPartialEquiv✝¹ : PartialEquiv Z (B × F)
open_target✝¹ : IsOpen toPartialEquiv✝¹.target
baseSet✝¹ : Set B
open_baseSet✝¹ : IsOpen baseSet✝¹
source_eq✝¹ : toPartialEquiv✝¹.source = proj ⁻¹' baseSet✝¹
target_eq✝¹ : toPartialEquiv✝¹.target = baseSet✝¹ ×ˢ univ
proj_toFun✝¹ : ∀ p ∈ toPartialEquiv✝¹.source, (↑toPartialEquiv✝¹ p).1 = proj p
toPartialEquiv✝ : PartialEquiv Z (B × F)
open_target✝ : IsOpen toPartialEquiv✝.target
baseSet✝ : Set B
open_baseSet✝ : IsOpen baseSet✝
source_eq✝ : toPartialEquiv✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toPartialEquiv✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toPartialEquiv✝.source, (↑toPartialEquiv✝ 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✝¹ }.toPartialEquiv =
    { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝,
        open_baseSet := open_baseSet✝, source_eq := source_eq✝, target_eq := target_eq✝,
        proj_toFun := proj_toFun✝ }.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✝¹ }.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✝ }.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✝¹ } =
    { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝,
      open_baseSet := open_baseSet✝, source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : e.toPartialEquiv = e'.toPartialEquiv
h₂ : e.baseSet = e'.baseSet
⊢ e = e'

Tactic:
cases e

Result:
case mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e' : Pretrivialization F proj
toPartialEquiv✝ : PartialEquiv Z (B × F)
open_target✝ : IsOpen toPartialEquiv✝.target
baseSet✝ : Set B
open_baseSet✝ : IsOpen baseSet✝
source_eq✝ : toPartialEquiv✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toPartialEquiv✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toPartialEquiv✝.source, (↑toPartialEquiv✝ 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✝ }.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✝ }.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✝ } =
    e'