awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y = (↑e.symm : Y → X) y
have rw : (↑e : X → Y) ((Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y) = y
Tactic: rw [e.eq_symm_apply _ hy.1]
-- 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
rw : (↑e : X → Y) ((Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y) = y
⊢ (Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y = (↑e.symm : Y → X) y
have rw₁ : (Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y ∈ e.source
Tactic: rw [e.eq_symm_apply _ hy.1]
-- 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (↑e : X → Y) ((Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y) = y
have change : (↑U : Set X).restrict (π := fun (a : X) ↦ Y) (↑e : X → Y) ((↑(e.subtypeRestr hU).symm : Y → ↥U) y) = y
Tactic: change restrict _ e _ = _
-- 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (↑U : Set X).restrict (π := fun (a : X) ↦ Y) (↑e : X → Y) ((↑(e.subtypeRestr hU).symm : Y → ↥U) y) = y
have rw : (↑(e.subtypeRestr hU) : ↥U → Y) ((↑(e.subtypeRestr hU).symm : Y → ↥U) y) = y
Tactic: rw [← e.subtypeRestr_coe hU, (e.subtypeRestr hU).right_inv hy]
-- 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
rw : (↑(e.subtypeRestr hU) : ↥U → Y) ((↑(e.subtypeRestr hU).symm : Y → ↥U) y) = y
⊢ (↑U : Set X).restrict (π := fun (a : X) ↦ Y) (↑e : X → Y) ((↑(e.subtypeRestr hU).symm : Y → ↥U) y) = y
have rw₁ : y = y
Tactic: rw [← e.subtypeRestr_coe hU, (e.subtypeRestr hU).right_inv hy]
-- 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
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y ∈ e.source
have this : (↑(e.subtypeRestr hU).symm : Y → ↥U) y ∈ (e.subtypeRestr hU).source
Tactic: have := OpenPartialHomeomorph.map_target _ hy
-- 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
this : (↑(e.subtypeRestr hU).symm : Y → ↥U) y ∈ (e.subtypeRestr hU).source
⊢ (Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y ∈ e.source
have rwa : ∀
  (this :
    Membership.mem (γ := Set ↥U) (Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' e.source)
      ((↑(e.subtypeRestr hU).symm : Y → ↥U) y)),
  (Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y ∈ e.source
Tactic: rwa [e.subtypeRestr_source] at this
Cleared hypotheses: this
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (↑(e.subtypeRestr hV).symm : Y → ↥V) y = (i ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y
have dsimp : (↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y) =
  i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y))
Tactic: dsimp [OpenPartialHomeomorph.subtypeRestr_def] at hy ⊢
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
⊢ (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
have rw : ∀ (hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (↑U : Set X)), (↑e.symm : Y → X) y ∈ (↑V : Set X)
Tactic: rw [Opens.openPartialHomeomorphSubtypeCoe_target] at hy ⊢
Cleared hypotheses: hy
-- 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
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
⊢ (↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y) =
    i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y))
have hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
Tactic: have hyV : e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target := by
    rw [Opens.openPartialHomeomorphSubtypeCoe_target] at hy ⊢
    exact hUV hy.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
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ (↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y) =
    i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y))
have refine_1 : (↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y) ∈
  (V.openPartialHomeomorphSubtypeCoe hV).source
Tactic: refine (V.openPartialHomeomorphSubtypeCoe hV).injOn ?_ trivial ?_
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
refine_1 :
  (↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y) ∈
    (V.openPartialHomeomorphSubtypeCoe hV).source
⊢ (↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y) =
    i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y))
have refine_2 : (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
    ((↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y)) =
  (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
    (i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y)))
Tactic: refine (V.openPartialHomeomorphSubtypeCoe hV).injOn ?_ trivial ?_
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
      ((↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y)) =
    (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
      (i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y)))
have refine_2 : (↑e.symm : Y → X) y =
  (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
    (i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y)))
Tactic: rw [(V.openPartialHomeomorphSubtypeCoe hV).right_inv hyV]
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ (↑e.symm : Y → X) y =
    (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
      (i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y)))
have refine_2 : (↑e.symm : Y → X) y =
  (↑(U.openPartialHomeomorphSubtypeCoe hU) : ↥U → X)
    ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y))
Tactic: change _ = U.openPartialHomeomorphSubtypeCoe hU _
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ (↑e.symm : Y → X) y =
    (↑(U.openPartialHomeomorphSubtypeCoe hU) : ↥U → X)
      ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y))
have refine_2 : (↑e.symm : Y → X) y = (↑e.symm : Y → X) y
Tactic: rw [(U.openPartialHomeomorphSubtypeCoe hU).right_inv hy.2]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) x ∈ e.target
have rw : (↑e : X → Z) x₀ ∈ e.target
Tactic: rw [← hxx₀, hf.injective.extend_apply e]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
⊢ x ∈ f '' e.source → (f ∘ e.invFun) (extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) x) = x
have this : ∀ (x₀ : X) (hx₀ : x₀ ∈ e.source) (hxx₀ : f x₀ = x),
  (f ∘ e.invFun) (extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) x) = x
Tactic: ⟨x₀, hx₀, hxx₀⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ (f ∘ e.invFun) (extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) x) = x
have rw : f (e.invFun ((↑e : X → Z) x₀)) = f x₀
Tactic: rw [← hxx₀, hf.injective.extend_apply e, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ f (e.invFun ((↑e : X → Z) x₀)) = f x₀
have e_a : e.invFun ((↑e : X → Z) x₀) = x₀
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
⊢ ContinuousOn (extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z) (f '' e.source)
have pos : Nonempty X → ContinuousOn (extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z) (f '' e.source)
Tactic: by_cases Nonempty X
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
pos : Nonempty X → ContinuousOn (extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z) (f '' e.source)
⊢ ContinuousOn (extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z) (f '' e.source)
have neg : ¬Nonempty X → ContinuousOn (extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z) (f '' e.source)
Tactic: by_cases Nonempty X
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
⊢ ContinuousOn (extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z) (f '' e.source)
have pos : let F := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z;
∀ (F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z), ContinuousOn F (f '' e.source)
Tactic: set F := (extend f e (fun _ ↦ (Classical.arbitrary Z))) with F_eq
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
F : X' → Z := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
x : X'
⊢ x ∈ f '' e.source → F x = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) x
have this : ∀ (x₀ : X) (hx₀ : x₀ ∈ e.source) (hxx₀ : f x₀ = x),
  F x = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) x
Tactic: ⟨x₀, hx₀, hxx₀⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
F : X' → Z := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ F x = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) x
have rw : F (f x₀) = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f x₀)
Tactic: rw [← hxx₀, F_eq, hf.injective.extend_apply e, comp_apply,
        hf.toOpenPartialHomeomorph_left_inv]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
F : X' → Z := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
rw : F (f x₀) = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f x₀)
rw₁ :
  extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) (f x₀) =
    ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f x₀)
⊢ F x = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) x
have rw₂ : (↑e : X → Z) x₀ = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f x₀)
Tactic: rw [← hxx₀, F_eq, hf.injective.extend_apply e, comp_apply,
        hf.toOpenPartialHomeomorph_left_inv]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
F : X' → Z := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
rw : F (f x₀) = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f x₀)
rw₁ :
  extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) (f x₀) =
    ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f x₀)
rw₂ : (↑e : X → Z) x₀ = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f x₀)
⊢ F x = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) x
have rw₃ : (↑e : X → Z) x₀ = (↑e : X → Z) ((↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f x₀))
Tactic: rw [← hxx₀, F_eq, hf.injective.extend_apply e, comp_apply,
        hf.toOpenPartialHomeomorph_left_inv]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
F : X' → Z := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
rw : F (f x₀) = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f x₀)
rw₁ :
  extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) (f x₀) =
    ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f x₀)
rw₂ : (↑e : X → Z) x₀ = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f x₀)
rw₃ : (↑e : X → Z) x₀ = (↑e : X → Z) ((↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f x₀))
⊢ F x = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) x
have rw₄ : (↑e : X → Z) x₀ = (↑e : X → Z) x₀
Tactic: rw [← hxx₀, F_eq, hf.injective.extend_apply e, comp_apply,
        hf.toOpenPartialHomeomorph_left_inv]