-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
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
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have 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
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]