-- Mathlib/Topology/PartialHomeomorph.lean
theorem prod_eq_prod_of_nonempty {eX eX' : PartialHomeomorph X X'} {eY eY' : PartialHomeomorph Y Y'}
    (h : (eX.prod eY).source.Nonempty) : eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Proof state:
case intro.mk
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝ : Nonempty X
this : Nonempty X'
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
haveI : Nonempty Y := ⟨y⟩

Result:
case intro.mk
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝¹ : Nonempty X
this✝ : Nonempty X'
this : Nonempty Y
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Proof state:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
obtain ⟨⟨x, y⟩, -⟩ := id h

Result:
case intro.mk
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Proof state:
case intro.mk
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝¹ : Nonempty X
this✝ : Nonempty X'
this : Nonempty Y
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
haveI : Nonempty Y' := ⟨eY y⟩

Result:
case intro.mk
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝² : Nonempty X
this✝¹ : Nonempty X'
this✝ : Nonempty Y
this : Nonempty Y'
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Proof state:
case intro.mk
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
haveI : Nonempty X := ⟨x⟩

Result:
case intro.mk
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this : Nonempty X
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Proof state:
case intro.mk
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝² : Nonempty X
this✝¹ : Nonempty X'
this✝ : Nonempty Y
this : Nonempty Y'
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
simp_rw [PartialHomeomorph.ext_iff, prod_apply, prod_symm_apply, prod_source, Prod.ext_iff,
  Set.prod_eq_prod_iff_of_nonempty h, forall_and, Prod.forall, forall_const,
  and_assoc, and_left_comm]

Result:
no goals

Proof state:
case intro.mk
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this : Nonempty X
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
haveI : Nonempty X' := ⟨eX x⟩

Result:
case intro.mk
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : PartialHomeomorph X X'
eY eY' : PartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝ : Nonempty X
this : Nonempty X'
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'