awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
refine_1 : ((e.restr s).symm.trans e').source = ((e.symm.trans e').restr ((↑e : X → Y) '' s)).source
refine_2 :
  EqOn (↑((e.restr s).symm.trans e') : Y → Y) (↑((e.symm.trans e').restr ((↑e : X → Y) '' s)) : Y → Y)
    ((e.restr s).symm.trans e').source
⊢ (e.restr s).symm.trans e' ≈ (e.symm.trans e').restr ((↑e : X → Y) '' s)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
refine_1 :
  e.target ∩ (↑e.symm : Y → X) ⁻¹' interior s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
    e.target ∩ (↑e.symm : Y → X) ⁻¹' e'.source ∩ interior ((↑e : X → Y) '' s)
⊢ ((e.restr s).symm.trans e').source = ((e.symm.trans e').restr ((↑e : X → Y) '' s)).source

Tactic:
simp only [trans_toPartialEquiv, symm_toPartialEquiv, restr_toPartialEquiv,
      PartialEquiv.trans_source, PartialEquiv.symm_source, PartialEquiv.restr_target, coe_coe_symm,
      PartialEquiv.restr_coe_symm, PartialEquiv.restr_source]

Premises used: PartialEquiv.restr_target, OpenPartialHomeomorph.symm_toPartialEquiv, PartialEquiv.trans_source, OpenPartialHomeomorph.restr_toPartialEquiv, PartialEquiv.restr_coe_symm, OpenPartialHomeomorph.trans_toPartialEquiv, PartialEquiv.symm_source, OpenPartialHomeomorph.coe_coe_symm, PartialEquiv.restr_source
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
refine_1 :
  e.target ∩ (↑e.symm : Y → X) ⁻¹' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
    e.target ∩ (↑e.symm : Y → X) ⁻¹' e'.source ∩ (↑e : X → Y) '' s
⊢ e.target ∩ (↑e.symm : Y → X) ⁻¹' interior s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
    e.target ∩ (↑e.symm : Y → X) ⁻¹' e'.source ∩ interior ((↑e : X → Y) '' s)

Tactic:
rw [interior_eq_iff_isOpen.mpr hs', interior_eq_iff_isOpen.mpr hs]

Premises used: Iff.mpr, interior_eq_iff_isOpen
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
refine_1 :
  e.target ∩ (↑e.symm : Y → X) ⁻¹' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
    e.target ∩ (↑e : X → Y) '' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source
⊢ e.target ∩ (↑e.symm : Y → X) ⁻¹' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
    e.target ∩ (↑e.symm : Y → X) ⁻¹' e'.source ∩ (↑e : X → Y) '' s

Tactic:
rw [inter_assoc, inter_assoc, inter_comm _ (e '' s), ← inter_assoc, ← inter_assoc]

Premises used: OpenPartialHomeomorph.toFun', Set.inter_comm, Set.image, Set.inter_assoc
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
refine_1 : e.target ∩ (↑e.symm : Y → X) ⁻¹' s = e.target ∩ (↑e : X → Y) '' s
⊢ e.target ∩ (↑e.symm : Y → X) ⁻¹' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
    e.target ∩ (↑e : X → Y) '' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source

Tactic:
congr 1
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
refine_1 : (↑e : X → Y) '' (e.source ∩ s) = (↑e : X → Y) '' e.source ∩ (↑e : X → Y) '' s
⊢ e.target ∩ (↑e.symm : Y → X) ⁻¹' s = e.target ∩ (↑e : X → Y) '' s

Tactic:
rw [← image_source_inter_eq', ← image_source_eq_target]

Premises used: OpenPartialHomeomorph.image_source_eq_target, OpenPartialHomeomorph.image_source_inter_eq'
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
⊢ (↑e : X → Y) '' (e.source ∩ s) = (↑e : X → Y) '' e.source ∩ (↑e : X → Y) '' s

Tactic:
image_inter_on ?_

Premises used: Set.image_inter_on
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
refine_1 : ∀ x ∈ s, ∀ y ∈ e.source, (↑e : X → Y) x = (↑e : X → Y) y → x = y
⊢ (↑e : X → Y) '' (e.source ∩ s) = (↑e : X → Y) '' e.source ∩ (↑e : X → Y) '' s

Tactic:
refine image_inter_on ?_

Premises used: Set.image_inter_on
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
x : X
hx : x ∈ s
y : X
hy : y ∈ e.source
h : (↑e : X → Y) x = (↑e : X → Y) y
refine_1 : x = (↑e.symm : Y → X) ((↑e : X → Y) y)
refine_1₁ : (↑e.symm : Y → X) ((↑e : X → Y) x) = (↑e.symm : Y → X) ((↑e : X → Y) y)
refine_1₂ refine_1₃ : (↑e.symm : Y → X) ((↑e : X → Y) y) = (↑e.symm : Y → X) ((↑e : X → Y) y)
⊢ x = y

Tactic:
rw [← left_inv e hy, ← left_inv e (hs'' hx), h]

Premises used: OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
refine_2 :
  EqOn ((↑e' : X → Y) ∘ (↑e.symm : Y → X)) ((↑e' : X → Y) ∘ (↑e.symm : Y → X)) ((e.restr s).symm.trans e').source
⊢ EqOn (↑((e.restr s).symm.trans e') : Y → Y) (↑((e.symm.trans e').restr ((↑e : X → Y) '' s)) : Y → Y)
    ((e.restr s).symm.trans e').source

Tactic:
simp_rw [coe_trans, restr_symm_apply, restr_apply, coe_trans]

Premises used: OpenPartialHomeomorph.restr_apply, OpenPartialHomeomorph.restr_symm_apply, OpenPartialHomeomorph.coe_trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
x : Y
hx : x ∈ ((e.restr s).symm.trans e').source
⊢ ((↑e' : X → Y) ∘ (↑e.symm : Y → X)) x = ((↑e' : X → Y) ∘ (↑e.symm : Y → X)) x

Tactic:
simp
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
rw : IsOpen[inst_1] ((↑e' : X → Y) '' (e'.source ∩ s))
⊢ IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)

Tactic:
rw [← image_source_inter_eq']

Premises used: OpenPartialHomeomorph.image_source_inter_eq'
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
⊢ IsOpen[inst_1] ((↑e' : X → Y) '' (e'.source ∩ s))

Tactic:
isOpen_image_source_inter e' hs

Premises used: OpenPartialHomeomorph.isOpen_image_source_inter
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
⊢ IsOpen[inst_1] ((↑e' : X → Y) '' (e'.source ∩ s))

Tactic:
exact isOpen_image_source_inter e' hs

Premises used: OpenPartialHomeomorph.isOpen_image_source_inter
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
⊢ IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)

Tactic:
have ht : IsOpen (e'.target ∩ e'.symm ⁻¹' s) := by
    rw [← image_source_inter_eq']
    exact isOpen_image_source_inter e' hs
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ e'.symm.trans (e.restr s) ≈ (e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)

Tactic:
⟨?_, ?_⟩

Premises used: OpenPartialHomeomorph.EqOnSource, And.intro
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1 : (e'.symm.trans (e.restr s)).source = ((e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)).source
refine_2 :
  EqOn (↑(e'.symm.trans (e.restr s)) : Y → Y)
    (↑((e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)) : Y → Y) (e'.symm.trans (e.restr s)).source
⊢ e'.symm.trans (e.restr s) ≈ (e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1 :
  e'.target ∩ ((↑e'.symm : Y → X) ⁻¹' e.source ∩ (↑e'.symm : Y → X) ⁻¹' interior s) =
    e'.target ∩ (↑e'.symm : Y → X) ⁻¹' e.source ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ (e'.symm.trans (e.restr s)).source = ((e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)).source

Tactic:
simp only [trans_toPartialEquiv, symm_toPartialEquiv, restr_toPartialEquiv,
      PartialEquiv.trans_source, PartialEquiv.symm_source, coe_coe_symm, PartialEquiv.restr_source,
      preimage_inter]

Premises used: Set.preimage_inter, OpenPartialHomeomorph.symm_toPartialEquiv, PartialEquiv.trans_source, OpenPartialHomeomorph.restr_toPartialEquiv, OpenPartialHomeomorph.trans_toPartialEquiv, PartialEquiv.symm_source, OpenPartialHomeomorph.coe_coe_symm, PartialEquiv.restr_source
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1 :
  (↑e'.symm : Y → X) ⁻¹' e.source ∩ (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s) =
    (↑e'.symm : Y → X) ⁻¹' e.source ∩ (e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s))
⊢ e'.target ∩ ((↑e'.symm : Y → X) ⁻¹' e.source ∩ (↑e'.symm : Y → X) ⁻¹' interior s) =
    e'.target ∩ (↑e'.symm : Y → X) ⁻¹' e.source ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)

Tactic:
rw [interior_eq_iff_isOpen.mpr hs,
      ← inter_assoc, inter_comm e'.target, inter_assoc, inter_assoc]

Premises used: Iff.mpr, PartialEquiv.target, Set.inter_comm, interior_eq_iff_isOpen, OpenPartialHomeomorph.toPartialEquiv, Set.inter_assoc
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1 : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ (↑e'.symm : Y → X) ⁻¹' e.source ∩ (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s) =
    (↑e'.symm : Y → X) ⁻¹' e.source ∩ (e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s))

Tactic:
congr 1
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1 : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)

Tactic:
nth_rw 2 [← interior_eq_iff_isOpen.mpr e'.open_target]

Premises used: Iff.mpr, interior_eq_iff_isOpen, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1 : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s))
refine_1₁ : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1₂ : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1₃ refine_1₄ : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s
⊢ e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)

Tactic:
rw [← interior_inter, ← inter_assoc, inter_self, interior_eq_iff_isOpen.mpr ht]

Premises used: Iff.mpr, interior_inter, Set.inter_self, interior_eq_iff_isOpen, Set.inter_assoc
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ EqOn (↑(e'.symm.trans (e.restr s)) : Y → Y)
    (↑((e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)) : Y → Y) (e'.symm.trans (e.restr s)).source

Tactic:
simp [Set.eqOn_refl]

Premises used: Set.eqOn_refl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
e : X ≃ₜ Y
e' : Y ≃ₜ Z
⊢ (e.trans e').toOpenPartialHomeomorph = e.toOpenPartialHomeomorph.trans e'.toOpenPartialHomeomorph

Tactic:
OpenPartialHomeomorph.toPartialEquiv_injective <| Equiv.trans_toPartialEquiv _ _

Premises used: Equiv.trans_toPartialEquiv, OpenPartialHomeomorph.toPartialEquiv_injective
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
e : X ≃ₜ Y
f' : OpenPartialHomeomorph Y Z
⊢ e.transOpenPartialHomeomorph f' = e.toOpenPartialHomeomorph.trans f'

Tactic:
OpenPartialHomeomorph.toPartialEquiv_injective <| Equiv.transPartialEquiv_eq_trans _ _

Premises used: OpenPartialHomeomorph.toPartialEquiv_injective, Equiv.transPartialEquiv_eq_trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
e : X ≃ₜ Y
f : OpenPartialHomeomorph Y Z
f' : OpenPartialHomeomorph Z Z'
⊢ (e.transOpenPartialHomeomorph f).trans f' = e.transOpenPartialHomeomorph (f.trans f')

Tactic:
simp only [transOpenPartialHomeomorph_eq_trans, OpenPartialHomeomorph.trans_assoc]

Premises used: OpenPartialHomeomorph.trans_assoc, Homeomorph.transOpenPartialHomeomorph_eq_trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
e : X ≃ₜ Y
e' : Y ≃ₜ Z
f'' : OpenPartialHomeomorph Z Z'
⊢ (e.trans e').transOpenPartialHomeomorph f'' = e.transOpenPartialHomeomorph (e'.transOpenPartialHomeomorph f'')

Tactic:
simp only [transOpenPartialHomeomorph_eq_trans, OpenPartialHomeomorph.trans_assoc,
    trans_toOpenPartialHomeomorph]

Premises used: OpenPartialHomeomorph.trans_assoc, Homeomorph.transOpenPartialHomeomorph_eq_trans, Homeomorph.trans_toOpenPartialHomeomorph
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
pos : ∀ (hab : a = b), ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
neg : ∀ (hab : a ≠ b), ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)

Tactic:
by_cases! hab : a = b
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a = b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)

Tactic:
simp [hab]
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
neg : Icc a b ⊆ closure[inst] (Ioo a b)
neg₁ : ∀ x ∈ Icc a b, ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)

Tactic:
apply continuousOn_extendFrom

Premises used: continuousOn_extendFrom
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
neg neg₁ : Icc a b ⊆ Icc a b
⊢ Icc a b ⊆ closure[inst] (Ioo a b)

Tactic:
rw [closure_Ioo hab]

Premises used: closure_Ioo
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
neg :
  ∀ (hf : ContinuousOn f (Ioo x b)) (ha : Tendsto f (𝓝[>] x) (𝓝 la)) (hab : x ≠ b) (x_in : x ∈ Icc x b),
    ∃ (y : β), Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
neg₁ :
  ∀ (hf : ContinuousOn f (Ioo a x)) (hb : Tendsto f (𝓝[<] x) (𝓝 lb)) (hab : a ≠ x) (x_in : x ∈ Icc a x),
    ∃ (y : β), Tendsto f (𝓝[Ioo a x] x) (𝓝 y)
neg₂ : ∀ (h : x ∈ Ioo a b), ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
rcases eq_endpoints_or_mem_Ioo_of_mem_Icc x_in with (rfl | rfl | h)

Premises used: Set.eq_endpoints_or_mem_Ioo_of_mem_Icc, rfl
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
b : α
la lb : β
inst_5 : RegularSpace β
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
x : α
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
hab : x ≠ b
x_in : x ∈ Icc x b
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo x b] x) (𝓝 y)

Tactic:
⟨la, ha.mono_left <| nhdsWithin_mono _ Ioo_subset_Ioi_self⟩

Premises used: Exists.intro, Filter.Tendsto.mono_left, Set.Ioo_subset_Ioi_self, nhdsWithin_mono
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
b : α
la lb : β
inst_5 : RegularSpace β
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
x : α
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
hab : x ≠ b
x_in : x ∈ Icc x b
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo x b] x) (𝓝 y)

Tactic:
exact ⟨la, ha.mono_left <| nhdsWithin_mono _ Ioo_subset_Ioi_self⟩
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a : α
la lb : β
inst_5 : RegularSpace β
ha : Tendsto f (𝓝[>] a) (𝓝 la)
x : α
hf : ContinuousOn f (Ioo a x)
hb : Tendsto f (𝓝[<] x) (𝓝 lb)
hab : a ≠ x
x_in : x ∈ Icc a x
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a x] x) (𝓝 y)

Tactic:
⟨lb, hb.mono_left <| nhdsWithin_mono _ Ioo_subset_Iio_self⟩

Premises used: Set.Ioo_subset_Iio_self, Exists.intro, Filter.Tendsto.mono_left, nhdsWithin_mono
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a : α
la lb : β
inst_5 : RegularSpace β
ha : Tendsto f (𝓝[>] a) (𝓝 la)
x : α
hf : ContinuousOn f (Ioo a x)
hb : Tendsto f (𝓝[<] x) (𝓝 lb)
hab : a ≠ x
x_in : x ∈ Icc a x
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a x] x) (𝓝 y)

Tactic:
exact ⟨lb, hb.mono_left <| nhdsWithin_mono _ Ioo_subset_Iio_self⟩
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
h : x ∈ Ioo a b
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
⟨f x, hf x h⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
h : x ∈ Ioo a b
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
exact ⟨f x, hf x h⟩
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
pos : ∀ (hab : a = b), ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
neg : ∀ (hab : a ≠ b), ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
by_cases! hab : a = b