-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this_1 : Nonempty X
this_2 : Nonempty X'
this_3 : Nonempty Y
this : Nonempty Y'
simp_rw :
  (∀ (x : X × Y), (↑(eX.prod eY) : X × Y → X' × Y') x = (↑(eX'.prod eY') : X × Y → X' × Y') x) ∧
      (∀ (x : X' × Y'), (↑(eX.prod eY).symm : X' × Y' → X × Y) x = (↑(eX'.prod eY').symm : X' × Y' → X × Y) x) ∧
        (eX.prod eY).source = (eX'.prod eY').source ↔
    ((∀ (x : X), (↑eX : X → X') x = (↑eX' : X → X') x) ∧
        (∀ (x : X'), (↑eX.symm : X' → X) x = (↑eX'.symm : X' → X) x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), (↑eY : Y → Y') x = (↑eY' : Y → Y') x) ∧
        (∀ (x : Y'), (↑eY.symm : Y' → Y) x = (↑eY'.symm : Y' → Y) x) ∧ eY.source = eY'.source
simp_rw₁ :
  (∀ (x : X × Y), ((↑eX : X → X') x.1, (↑eY : Y → Y') x.2) = ((↑eX' : X → X') x.1, (↑eY' : Y → Y') x.2)) ∧
      (∀ (x : X' × Y'), (↑(eX.prod eY).symm : X' × Y' → X × Y) x = (↑(eX'.prod eY').symm : X' × Y' → X × Y) x) ∧
        (eX.prod eY).source = (eX'.prod eY').source ↔
    ((∀ (x : X), (↑eX : X → X') x = (↑eX' : X → X') x) ∧
        (∀ (x : X'), (↑eX.symm : X' → X) x = (↑eX'.symm : X' → X) x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), (↑eY : Y → Y') x = (↑eY' : Y → Y') x) ∧
        (∀ (x : Y'), (↑eY.symm : Y' → Y) x = (↑eY'.symm : Y' → Y) x) ∧ eY.source = eY'.source
simp_rw₂ :
  (∀ (x : X × Y), ((↑eX : X → X') x.1, (↑eY : Y → Y') x.2) = ((↑eX' : X → X') x.1, (↑eY' : Y → Y') x.2)) ∧
      (∀ (x : X' × Y'),
          ((↑eX.symm : X' → X) x.1, (↑eY.symm : Y' → Y) x.2) = ((↑eX'.symm : X' → X) x.1, (↑eY'.symm : Y' → Y) x.2)) ∧
        (eX.prod eY).source = (eX'.prod eY').source ↔
    ((∀ (x : X), (↑eX : X → X') x = (↑eX' : X → X') x) ∧
        (∀ (x : X'), (↑eX.symm : X' → X) x = (↑eX'.symm : X' → X) x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), (↑eY : Y → Y') x = (↑eY' : Y → Y') x) ∧
        (∀ (x : Y'), (↑eY.symm : Y' → Y) x = (↑eY'.symm : Y' → Y) x) ∧ eY.source = eY'.source
simp_rw₃ :
  (∀ (x : X × Y), ((↑eX : X → X') x.1, (↑eY : Y → Y') x.2) = ((↑eX' : X → X') x.1, (↑eY' : Y → Y') x.2)) ∧
      (∀ (x : X' × Y'),
          ((↑eX.symm : X' → X) x.1, (↑eY.symm : Y' → Y) x.2) = ((↑eX'.symm : X' → X) x.1, (↑eY'.symm : Y' → Y) x.2)) ∧
        eX.source ×ˢ eY.source = eX'.source ×ˢ eY'.source ↔
    ((∀ (x : X), (↑eX : X → X') x = (↑eX' : X → X') x) ∧
        (∀ (x : X'), (↑eX.symm : X' → X) x = (↑eX'.symm : X' → X) x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), (↑eY : Y → Y') x = (↑eY' : Y → Y') x) ∧
        (∀ (x : Y'), (↑eY.symm : Y' → Y) x = (↑eY'.symm : Y' → Y) x) ∧ eY.source = eY'.source
simp_rw₄ :
  (∀ (x : X × Y), (↑eX : X → X') x.1 = (↑eX' : X → X') x.1 ∧ (↑eY : Y → Y') x.2 = (↑eY' : Y → Y') x.2) ∧
      (∀ (x : X' × Y'),
          (↑eX.symm : X' → X) x.1 = (↑eX'.symm : X' → X) x.1 ∧ (↑eY.symm : Y' → Y) x.2 = (↑eY'.symm : Y' → Y) x.2) ∧
        eX.source ×ˢ eY.source = eX'.source ×ˢ eY'.source ↔
    ((∀ (x : X), (↑eX : X → X') x = (↑eX' : X → X') x) ∧
        (∀ (x : X'), (↑eX.symm : X' → X) x = (↑eX'.symm : X' → X) x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), (↑eY : Y → Y') x = (↑eY' : Y → Y') x) ∧
        (∀ (x : Y'), (↑eY.symm : Y' → Y) x = (↑eY'.symm : Y' → Y) x) ∧ eY.source = eY'.source
simp_rw₅ :
  (∀ (x : X × Y), (↑eX : X → X') x.1 = (↑eX' : X → X') x.1 ∧ (↑eY : Y → Y') x.2 = (↑eY' : Y → Y') x.2) ∧
      (∀ (x : X' × Y'),
          (↑eX.symm : X' → X) x.1 = (↑eX'.symm : X' → X) x.1 ∧ (↑eY.symm : Y' → Y) x.2 = (↑eY'.symm : Y' → Y) x.2) ∧
        eX.source = eX'.source ∧ eY.source = eY'.source ↔
    ((∀ (x : X), (↑eX : X → X') x = (↑eX' : X → X') x) ∧
        (∀ (x : X'), (↑eX.symm : X' → X) x = (↑eX'.symm : X' → X) x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), (↑eY : Y → Y') x = (↑eY' : Y → Y') x) ∧
        (∀ (x : Y'), (↑eY.symm : Y' → Y) x = (↑eY'.symm : Y' → Y) x) ∧ eY.source = eY'.source
simp_rw₆ :
  ((∀ (x : X × Y), (↑eX : X → X') x.1 = (↑eX' : X → X') x.1) ∧
        ∀ (x : X × Y), (↑eY : Y → Y') x.2 = (↑eY' : Y → Y') x.2) ∧
      ((∀ (x : X' × Y'), (↑eX.symm : X' → X) x.1 = (↑eX'.symm : X' → X) x.1) ∧
          ∀ (x : X' × Y'), (↑eY.symm : Y' → Y) x.2 = (↑eY'.symm : Y' → Y) x.2) ∧
        eX.source = eX'.source ∧ eY.source = eY'.source ↔
    ((∀ (x : X), (↑eX : X → X') x = (↑eX' : X → X') x) ∧
        (∀ (x : X'), (↑eX.symm : X' → X) x = (↑eX'.symm : X' → X) x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), (↑eY : Y → Y') x = (↑eY' : Y → Y') x) ∧
        (∀ (x : Y'), (↑eY.symm : Y' → Y) x = (↑eY'.symm : Y' → Y) x) ∧ eY.source = eY'.source
simp_rw₇ :
  ((∀ (a : X) (b : Y), (↑eX : X → X') a = (↑eX' : X → X') a) ∧
        ∀ (a : X) (b : Y), (↑eY : Y → Y') b = (↑eY' : Y → Y') b) ∧
      ((∀ (a : X') (b : Y'), (↑eX.symm : X' → X) a = (↑eX'.symm : X' → X) a) ∧
          ∀ (a : X') (b : Y'), (↑eY.symm : Y' → Y) b = (↑eY'.symm : Y' → Y) b) ∧
        eX.source = eX'.source ∧ eY.source = eY'.source ↔
    ((∀ (x : X), (↑eX : X → X') x = (↑eX' : X → X') x) ∧
        (∀ (x : X'), (↑eX.symm : X' → X) x = (↑eX'.symm : X' → X) x) ∧ eX.source = eX'.source) ∧
      (∀ (b : Y), (↑eY : Y → Y') b = (↑eY' : Y → Y') b) ∧
        (∀ (b : Y'), (↑eY.symm : Y' → Y) b = (↑eY'.symm : Y' → Y) b) ∧ eY.source = eY'.source
simp_rw₈ :
  ((∀ (a : X), (↑eX : X → X') a = (↑eX' : X → X') a) ∧ ∀ (b : Y), (↑eY : Y → Y') b = (↑eY' : Y → Y') b) ∧
      ((∀ (a : X'), (↑eX.symm : X' → X) a = (↑eX'.symm : X' → X) a) ∧
          ∀ (b : Y'), (↑eY.symm : Y' → Y) b = (↑eY'.symm : Y' → Y) b) ∧
        eX.source = eX'.source ∧ eY.source = eY'.source ↔
    ((∀ (a : X), (↑eX : X → X') a = (↑eX' : X → X') a) ∧
        (∀ (a : X'), (↑eX.symm : X' → X) a = (↑eX'.symm : X' → X) a) ∧ eX.source = eX'.source) ∧
      (∀ (b : Y), (↑eY : Y → Y') b = (↑eY' : Y → Y') b) ∧
        (∀ (b : Y'), (↑eY.symm : Y' → Y) b = (↑eY'.symm : Y' → Y) b) ∧ eY.source = eY'.source
simp_rw₉ :
  (∀ (a : X), (↑eX : X → X') a = (↑eX' : X → X') a) ∧
      (∀ (b : Y), (↑eY : Y → Y') b = (↑eY' : Y → Y') b) ∧
        (∀ (a : X'), (↑eX.symm : X' → X) a = (↑eX'.symm : X' → X) a) ∧
          (∀ (b : Y'), (↑eY.symm : Y' → Y) b = (↑eY'.symm : Y' → Y) b) ∧
            eX.source = eX'.source ∧ eY.source = eY'.source ↔
    (∀ (a : X), (↑eX : X → X') a = (↑eX' : X → X') a) ∧
      (∀ (a : X'), (↑eX.symm : X' → X) a = (↑eX'.symm : X' → X) a) ∧
        eX.source = eX'.source ∧
          (∀ (b : Y), (↑eY : Y → Y') b = (↑eY' : Y → Y') b) ∧
            (∀ (b : Y'), (↑eY.symm : Y' → Y) b = (↑eY'.symm : Y' → Y) b) ∧ eY.source = eY'.source
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
simp_rw [OpenPartialHomeomorph.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]

Premises used: OpenPartialHomeomorph.ext_iff, OpenPartialHomeomorph.prod_symm_apply, Prod.ext_iff, OpenPartialHomeomorph.prod_apply, and_left_comm, Set.prod_eq_prod_iff_of_nonempty, and_assoc, Prod.forall, forall_const, OpenPartialHomeomorph.prod_source, forall_and