awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
e_a : e.invFun ((↑e : X → Z) x₀) = x₀
⊢ f (e.invFun ((↑e : X → Z) x₀)) = f x₀

Tactic:
congr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
⊢ e.invFun ((↑e : X → Z) x₀) = x₀

Tactic:
e.left_inv' hx₀

Premises used: OpenPartialHomeomorph.toFun', PartialEquiv.left_inv', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
⊢ e.invFun ((↑e : X → Z) x₀) = x₀

Tactic:
exact e.left_inv' hx₀

Premises used: PartialEquiv.left_inv', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
z : Z
hz : z ∈ e.target
⊢ extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) ((f ∘ e.invFun) z) = z

Tactic:
simpa only [comp_apply, hf.injective.extend_apply e] using e.right_inv' hz

Premises used: PartialEquiv.right_inv', Topology.IsOpenEmbedding.toIsEmbedding, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply, Topology.IsEmbedding.injective, Function.comp_apply, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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)
neg : ¬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)

Tactic:
by_cases Nonempty X

Premises used: Nonempty
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
x : X'
hx : x ∈ f '' e.source
⊢ ContinuousWithinAt (extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z) (f '' e.source) x

Tactic:
simp_all
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
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)
⊢ ContinuousOn (extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z) (f '' e.source)

Tactic:
set F := (extend f e (fun _ ↦ (Classical.arbitrary Z))) with F_eq

Premises used: OpenPartialHomeomorph.toFun', Function.extend, Classical.arbitrary
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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'
this :
  ∀ (x₀ : X) (hx₀ : x₀ ∈ e.source) (hxx₀ : f x₀ = x),
    F x = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) x
⊢ x ∈ f '' e.source → F x = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) x

Tactic:
⟨x₀, hx₀, hxx₀⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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₀))
rw₄ rw₅ : (↑e : X → Z) x₀ = (↑e : X → Z) x₀
⊢ F x = ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) x

Tactic:
rw [← hxx₀, F_eq, hf.injective.extend_apply e, comp_apply,
        hf.toOpenPartialHomeomorph_left_inv]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply, Topology.IsEmbedding.injective, Function.comp_apply, Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
⊢ EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)

Tactic:
have heq : EqOn F (e ∘ (hf.toOpenPartialHomeomorph).symm) (f '' e.source) := by
      intro x ⟨x₀, hx₀, hxx₀⟩
      rw [← hxx₀, F_eq, hf.injective.extend_apply e, comp_apply,
        hf.toOpenPartialHomeomorph_left_inv]
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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_1 : 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
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
hf₁ : ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' e.source)
h : MapsTo (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' e.source) e.source
⊢ ContinuousOn ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)

Tactic:
apply e.continuousOn_toFun.comp

Premises used: ContinuousOn.comp, OpenPartialHomeomorph.continuousOn_toFun
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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_1 : 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
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
x' : X'
h :
  ∀ (x : X) (hx : x ∈ e.source) (hx'x : f x = x'),
    (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) x' ∈ e.source
⊢ x' ∈ f '' e.source → (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) x' ∈ e.source

Tactic:
⟨x, hx, hx'x⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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_1 : 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
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
x' : X'
x : X
hx : x ∈ e.source
hx'x : f x = x'
h : x ∈ e.source
⊢ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) x' ∈ e.source

Tactic:
rw [← hx'x, hf.toOpenPartialHomeomorph_left_inv]

Premises used: Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
x' : X'
x : X
hx : x ∈ e.source
hx'x : f x = x'
⊢ x ∈ e.source

Tactic:
hx
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
x' : X'
x : X
hx : x ∈ e.source
hx'x : f x = x'
⊢ x ∈ e.source

Tactic:
exact hx
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' univ)

Tactic:
have : ContinuousOn (hf.toOpenPartialHomeomorph).symm (f '' univ) :=
        (hf.toOpenPartialHomeomorph).continuousOn_invFun
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
this : ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' univ)
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' e.source)

Tactic:
this.mono <| image_mono <| subset_univ _

Premises used: Set.subset_univ, Set.image_mono, ContinuousOn.mono
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
this : ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' univ)
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' e.source)

Tactic:
exact this.mono <| image_mono <| subset_univ _

Premises used: Set.subset_univ, Set.image_mono, ContinuousOn.mono
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
⊢ ContinuousOn ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)

Tactic:
have : ContinuousOn (e ∘ (hf.toOpenPartialHomeomorph).symm) (f '' e.source) := by
      apply e.continuousOn_toFun.comp; swap
      · intro x' ⟨x, hx, hx'x⟩
        rw [← hx'x, hf.toOpenPartialHomeomorph_left_inv]; exact hx
      have : ContinuousOn (hf.toOpenPartialHomeomorph).symm (f '' univ) :=
        (hf.toOpenPartialHomeomorph).continuousOn_invFun
      exact this.mono <| image_mono <| subset_univ _
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
this : ContinuousOn ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
⊢ ContinuousOn F (f '' e.source)

Tactic:
ContinuousOn.congr this heq

Premises used: ContinuousOn.congr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
this : ContinuousOn ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
⊢ ContinuousOn F (f '' e.source)

Tactic:
exact ContinuousOn.congr this heq

Premises used: ContinuousOn.congr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
⊢ (↑(e.lift_openEmbedding hf) : X' → Z) = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', dite, Function.extend, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X
simp_rw : extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) (f x) = (↑e : X → Z) x
⊢ (↑(e.lift_openEmbedding hf) : X' → Z) (f x) = (↑e : X → Z) x

Tactic:
simp_rw [e.lift_openEmbedding_toFun]

Premises used: OpenPartialHomeomorph.lift_openEmbedding_toFun
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X
⊢ extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) (f x) = (↑e : X → Z) x

Tactic:
apply hf.injective.extend_apply

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Function.Injective.extend_apply, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
⊢ (e.lift_openEmbedding hf).source = f '' e.source

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
⊢ (e.lift_openEmbedding hf).target = e.target

Tactic:
rfl

Premises used: rfl