awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (hypothesis)
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 : Nonempty X'
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have this₁ : Nonempty Y
Tactic: haveI : Nonempty Y := ⟨y⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (hypothesis)
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 : Nonempty Y
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have this₁ : Nonempty Y'
Tactic: haveI : Nonempty Y' := ⟨eY y⟩
-- 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'
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have 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
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]
-- 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
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have 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
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]
-- 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
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have 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
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]
-- 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
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have 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
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]
-- 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
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have rw : eX'.prod eY' = eX.prod eY ↔ eX = eX' ∧ eY = eY'
Tactic: rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ eY']
-- 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
rw : eX'.prod eY' = eX.prod eY ↔ eX = eX' ∧ eY = eY'
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have rw₁ : eX' = eX ∧ eY' = eY ↔ eX = eX' ∧ eY = eY'
Tactic: rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ eY']
-- 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
rw : eX'.prod eY' = eX.prod eY ↔ eX = eX' ∧ eY = eY'
rw₁ : eX' = eX ∧ eY' = eY ↔ eX = eX' ∧ eY = eY'
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have rw₂ : eX = eX' ∧ eY' = eY ↔ eX = eX' ∧ eY = eY'
Tactic: rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ eY']
-- 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
rw : eX'.prod eY' = eX.prod eY ↔ eX = eX' ∧ eY = eY'
rw₁ : eX' = eX ∧ eY' = eY ↔ eX = eX' ∧ eY = eY'
rw₂ : eX = eX' ∧ eY' = eY ↔ eX = eX' ∧ eY = eY'
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have rw₃ : eX = eX' ∧ eY = eY' ↔ eX = eX' ∧ eY = eY'
Tactic: rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ eY']
-- 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
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e_1 e e' : OpenPartialHomeomorph X Y
inst_6 : (x : X) → Decidable (x ∈ e.source)
inst_7 : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ e.source ∩ frontier e.source = e'.source ∩ frontier e.source
have rw : ∅ = e'.source ∩ frontier e.source
Tactic: rw [e.open_source.inter_frontier_eq, (Hs.symm.frontier_right e'.open_source).inter_eq]
-- 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
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e_1 e e' : OpenPartialHomeomorph X Y
inst_6 : (x : X) → Decidable (x ∈ e.source)
inst_7 : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
rw : ∅ = e'.source ∩ frontier e.source
⊢ e.source ∩ frontier e.source = e'.source ∩ frontier e.source
have rw₁ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
Tactic: rw [e.open_source.inter_frontier_eq, (Hs.symm.frontier_right e'.open_source).inter_eq]
-- 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
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e_1 e e' : OpenPartialHomeomorph X Y
inst_6 : (x : X) → Decidable (x ∈ e.source)
inst_7 : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ frontier e.source)
have rw : EqOn (↑e : X → Y) (↑e' : X → Y) ∅
Tactic: rw [e.open_source.inter_frontier_eq]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
x : ↥s
hxe : (↑x : X) ∈ e.source
⊢ (↑e : X → Y) (↑x : X) ∈ (e.subtypeRestr hs).target
have refine : (↑e : X → Y) (↑x : X) ∈ (↑e.symm : Y → X) ⁻¹' (s.openPartialHomeomorphSubtypeCoe hs).target
Tactic: refine ⟨e.map_source hxe, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
x : ↥s
hxe : (↑x : X) ∈ e.source
⊢ (↑e : X → Y) (↑x : X) ∈ (↑e.symm : Y → X) ⁻¹' (s.openPartialHomeomorphSubtypeCoe hs).target
have rw : (↑x : X) ∈ (↑s : Set X)
Tactic: rw [s.openPartialHomeomorphSubtypeCoe_target, mem_preimage, e.leftInvOn hxe]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
⊢ (e.subtypeRestr hs).target ⊆ e.target
have rw : (↑(e.subtypeRestr hs) : ↥s → Y) '' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' e.source ⊆ (↑e : X → Y) '' e.source
Tactic: rw [← e.image_source_eq_target, ← OpenPartialHomeomorph.image_source_eq_target,
    e.subtypeRestr_source]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
z₀ : ↥s
hz₀ : Membership.mem (γ := Set ↥s) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' e.source) z₀
⊢ (↑(e.subtypeRestr hs) : ↥s → Y) z₀ ∈ (↑e : X → Y) '' e.source
have h : (↑z₀ : X) ∈ e.source ∧ (↑e : X → Y) (↑z₀ : X) = (↑(e.subtypeRestr hs) : ↥s → Y) z₀
Tactic: use z₀.val
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
⊢ (f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈
    (f.symm.trans f').restr (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
have simp : (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans ((s.openPartialHomeomorphSubtypeCoe hs).trans f') ≈
  (f.symm.trans f').restr (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
Tactic: simp only [subtypeRestr_def, trans_symm_eq_symm_trans_symm]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (hypothesis)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
⊢ (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans ((s.openPartialHomeomorphSubtypeCoe hs).trans f') ≈
    (f.symm.trans f').restr (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
have openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
Tactic: have openness₁ : IsOpen (f.target ∩ f.symm ⁻¹' s) := f.isOpen_inter_preimage_symm s.2
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
⊢ (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans ((s.openPartialHomeomorphSubtypeCoe hs).trans f') ≈
    (f.symm.trans f').restr (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
have rw : ((f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs)).trans f' ≈
  ((ofSet (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) openness₁).trans f.symm).trans f'
Tactic: rw [← ofSet_trans _ openness₁, ← trans_assoc, ← trans_assoc]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
⊢ ((f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs)).trans f' ≈
    ((ofSet (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) openness₁).trans f.symm).trans f'
have refine : (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs) ≈
  (ofSet (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) openness₁).trans f.symm
Tactic: refine EqOnSource.trans' ?_ (eqOnSource_refl _)
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
⊢ f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
have h : ∀ (x : Y),
  x ∈ f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) ↔
    x ∈ f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (hypothesis)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
⊢ (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs) ≈
    (ofSet (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) openness₁).trans f.symm
have set_identity : f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
Tactic: have set_identity : f.symm.source ∩ (f.target ∩ f.symm ⁻¹' s) = f.symm.source ∩ f.symm ⁻¹' s := by
    mfld_set_tac
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (hypothesis)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
set_identity :
  f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
⊢ (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs) ≈
    (ofSet (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) openness₁).trans f.symm
have openness₂ : IsOpen[inst] (↑s : Set X)
Tactic: have openness₂ : IsOpen (s : Set X) := s.2
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
set_identity :
  f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
openness₂ : IsOpen[inst] (↑s : Set X)
⊢ (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs) ≈
    (ofSet (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) openness₁).trans f.symm
have rw : f.symm.trans ((s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs)) ≈
  f.symm.trans (ofSet (↑s : Set X) openness₂)
Tactic: rw [ofSet_trans', set_identity, ← trans_of_set' _ openness₂, trans_assoc]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
set_identity :
  f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
openness₂ : IsOpen[inst] (↑s : Set X)
⊢ f.symm.trans ((s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs)) ≈
    f.symm.trans (ofSet (↑s : Set X) openness₂)
have refine : (s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs) ≈ ofSet (↑s : Set X) openness₂
Tactic: refine EqOnSource.trans' (eqOnSource_refl _) ?_
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
set_identity :
  f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
openness₂ : IsOpen[inst] (↑s : Set X)
⊢ (s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs) ≈
    ofSet (↑s : Set X) openness₂
have refine : ofSet (s.openPartialHomeomorphSubtypeCoe hs).target sorry ≈ ofSet (↑s : Set X) openness₂
Tactic: refine Setoid.trans (symm_trans_self (s.openPartialHomeomorphSubtypeCoe hs)) ?_