awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
sep : IsSeparatedMap f
g : A → Y
rw :
  ∀ (sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)) (g : A → Y),
    IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal snd)
⊢ IsSeparatedMap (X := Function.Pullback f g) snd

Tactic:
rw [isSeparatedMap_iff_isClosed_diagonal] at sep ⊢

Premises used: isSeparatedMap_iff_isClosed_diagonal
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → Y
rw : IsClosed[instTopologicalSpaceSubtype] (Function.PullbackSelf.map_fst ⁻¹' Function.pullbackDiagonal f)
⊢ IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal snd)

Tactic:
rw [← preimage_map_fst_pullbackDiagonal]

Premises used: preimage_map_fst_pullbackDiagonal
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → Y
⊢ IsClosed[instTopologicalSpaceSubtype] (Function.PullbackSelf.map_fst ⁻¹' Function.pullbackDiagonal f)

Tactic:
sep.preimage (Continuous.mapPullback ?_ ?_)

Premises used: Function.PullbackSelf.map_fst, IsClosed.preimage, Continuous.mapPullback
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → Y
refine_1 refine_2 : Continuous[instTopologicalSpaceSubtype, inst] fst
⊢ IsClosed[instTopologicalSpaceSubtype] (Function.PullbackSelf.map_fst ⁻¹' Function.pullbackDiagonal f)

Tactic:
refine sep.preimage (Continuous.mapPullback ?_ ?_)

Premises used: IsClosed.preimage, Continuous.mapPullback
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → Y
⊢ Continuous[instTopologicalSpaceSubtype, inst] fst

Tactic:
apply_rules [continuous_fst, continuous_subtype_val, Continuous.comp]

Premises used: continuous_subtype_val, Continuous.comp, continuous_fst
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_2
Y : Sort u_3
inst : TopologicalSpace X
A : Sort u_1
f : X → Y
sep : IsSeparatedMap f
g : Y → A
inj : Function.Injective g
⊢ IsSeparatedMap (g ∘ f)

Tactic:
fun x₁ x₂ he ↦ sep x₁ x₂ (inj he)

Premises used: IsSeparatedMap
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
sep : IsSeparatedMap f
g : A → X
cont : Continuous[inst_1, inst] g
inj : Function.Injective g
rw :
  ∀ (sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)) {g : A → X}
    (cont : Continuous[inst_1, inst] g) (inj : Function.Injective g),
    IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal (f ∘ g))
⊢ IsSeparatedMap (f ∘ g)

Tactic:
rw [isSeparatedMap_iff_isClosed_diagonal] at sep ⊢

Premises used: isSeparatedMap_iff_isClosed_diagonal
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → X
cont : Continuous[inst_1, inst] g
inj : Function.Injective g
rw : IsClosed[instTopologicalSpaceSubtype] (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)
⊢ IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal (f ∘ g))

Tactic:
rw [← inj.preimage_pullbackDiagonal]

Premises used: Function.Injective.preimage_pullbackDiagonal
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → X
cont : Continuous[inst_1, inst] g
inj : Function.Injective g
⊢ IsClosed[instTopologicalSpaceSubtype] (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)

Tactic:
sep.preimage (cont.mapPullback cont)

Premises used: IsClosed.preimage, Continuous.mapPullback
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → X
cont : Continuous[inst_1, inst] g
inj : Function.Injective g
⊢ IsClosed[instTopologicalSpaceSubtype] (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)

Tactic:
exact sep.preimage (cont.mapPullback cont)

Premises used: IsClosed.preimage, Continuous.mapPullback
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
inj : Injective f
⊢ _root_.IsLocallyInjective f

Tactic:
fun _ ↦ ⟨_, isOpen_univ, trivial, fun _ _ _ _ ↦ @inj _ _⟩

Premises used: trivial, Set.univ, IsLocallyInjective, isOpen_univ, And.intro, Exists.intro
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
mp : IsLocallyInjective f → ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
mpr : (∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) → IsLocallyInjective f
⊢ IsLocallyInjective f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
constructor
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
mp : ∀ (U : Set X) (ho : IsOpen[inst] U) (hm : x ∈ U) (hi : Set.InjOn f U), ∃ U ∈ 𝓝 x, Set.InjOn f U
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
obtain ⟨U, ho, hm, hi⟩ := h x
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
U : Set X
ho : IsOpen[inst] U
hm : x ∈ U
hi : Set.InjOn f U
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
⟨U, ho.mem_nhds hm, hi⟩

Premises used: And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
U : Set X
ho : IsOpen[inst] U
hm : x ∈ U
hi : Set.InjOn f U
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
exact ⟨U, ho.mem_nhds hm, hi⟩
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
mpr : ∀ (U : Set X) (hn : U ∈ 𝓝 x) (hi : Set.InjOn f U), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn f U
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn f U

Tactic:
obtain ⟨U, hn, hi⟩ := h x
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
U : Set X
hn : U ∈ 𝓝 x
hi : Set.InjOn f U
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn f U

Tactic:
⟨interior U, isOpen_interior, mem_interior_iff_mem_nhds.mpr hn, hi.mono interior_subset⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, interior_subset, isOpen_interior, And.intro, interior, Exists.intro, Set.InjOn.mono
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
U : Set X
hn : U ∈ 𝓝 x
hi : Set.InjOn f U
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn f U

Tactic:
exact ⟨interior U, isOpen_interior, mem_interior_iff_mem_nhds.mpr hn, hi.mono interior_subset⟩
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
simp_rw :
  (∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) ↔
    ∀ (a b : X) (b_1 : f a = f b),
      Subtype.mk (p := fun (a : X × X) ↦ f a.1 = f a.2) (a, b) b_1 ∈ Function.pullbackDiagonal f →
        ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f
⊢ IsLocallyInjective f ↔ IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)

Tactic:
simp_rw [isLocallyInjective_iff_nhds, isOpen_iff_mem_nhds,
    Subtype.forall, Prod.forall, nhds_induced, nhds_prod_eq, Filter.mem_comap]

Premises used: Subtype.forall, Filter.mem_comap, nhds_induced, Prod.forall, nhds_prod_eq, isOpen_iff_mem_nhds, isLocallyInjective_iff_nhds
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ (∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) ↔
    ∀ (a b : X) (b_1 : f a = f b),
      Subtype.mk (p := fun (a : X × X) ↦ f a.1 = f a.2) (a, b) b_1 ∈ Function.pullbackDiagonal f →
        ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f

Tactic:
⟨?_, fun h x ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
refine_1 :
  (∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) →
    ∀ (a b : X) (b_1 : f a = f b),
      Subtype.mk (p := fun (a : X × X) ↦ f a.1 = f a.2) (a, b) b_1 ∈ Function.pullbackDiagonal f →
        ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f
refine_2 :
  ∀
    (h :
      ∀ (a b : X) (b_1 : f a = f b),
        Subtype.mk (p := fun (a : X × X) ↦ f a.1 = f a.2) (a, b) b_1 ∈ Function.pullbackDiagonal f →
          ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f)
    (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
⊢ (∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) ↔
    ∀ (a b : X) (b_1 : f a = f b),
      Subtype.mk (p := fun (a : X × X) ↦ f a.1 = f a.2) (a, b) b_1 ∈ Function.pullbackDiagonal f →
        ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f

Tactic:
refine ⟨?_, fun h x ↦ ?_⟩
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
hx : f x = f x
refine_1 :
  ∀ (U : Set X) (hn : U ∈ 𝓝 x) (hi : Set.InjOn f U),
    ∃ t ∈ 𝓝 x ×ˢ 𝓝 x, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f
⊢ ∃ t ∈ 𝓝 x ×ˢ 𝓝 x, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f

Tactic:
obtain ⟨U, hn, hi⟩ := h x
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
hx : f x = f x
U : Set X
hn : U ∈ 𝓝 x
hi : Set.InjOn f U
⊢ ∃ t ∈ 𝓝 x ×ˢ 𝓝 x, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f

Tactic:
⟨_, Filter.prod_mem_prod hn hn, fun {p} hp ↦ hi hp.1 hp.2 p.2⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Filter.prod_mem_prod, Subtype.property
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
hx : f x = f x
U : Set X
hn : U ∈ 𝓝 x
hi : Set.InjOn f U
⊢ ∃ t ∈ 𝓝 x ×ˢ 𝓝 x, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f

Tactic:
exact ⟨_, Filter.prod_mem_prod hn hn, fun {p} hp ↦ hi hp.1 hp.2 p.2⟩
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h :
  ∀ (a b : X) (b_1 : f a = f b),
    Subtype.mk (p := fun (a : X × X) ↦ f a.1 = f a.2) (a, b) b_1 ∈ Function.pullbackDiagonal f →
      ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f
x : X
refine_2 :
  ∀ (t : Set (X × X)) (ht : t ∈ 𝓝 x ×ˢ 𝓝 x)
    (t_sub : Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f),
    ∃ U ∈ 𝓝 x, Set.InjOn f U
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
obtain ⟨t, ht, t_sub⟩ := h x x rfl rfl

Premises used: rfl
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h :
  ∀ (a b : X) (b_1 : f a = f b),
    Subtype.mk (p := fun (a : X × X) ↦ f a.1 = f a.2) (a, b) b_1 ∈ Function.pullbackDiagonal f →
      ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f
x : X
t : Set (X × X)
ht : t ∈ 𝓝 x ×ˢ 𝓝 x
t_sub : Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f
refine_2 :
  ∀ (t₁ : Set X) (h₁ : t₁ ∈ 𝓝 x) (t₂ : Set X) (h₂ : t₂ ∈ 𝓝 x) (prod_sub : t₁ ×ˢ t₂ ⊆ t), ∃ U ∈ 𝓝 x, Set.InjOn f U
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
obtain ⟨t₁, h₁, t₂, h₂, prod_sub⟩ := Filter.mem_prod_iff.mp ht

Premises used: Iff.mp, Filter.mem_prod_iff
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h :
  ∀ (a b : X) (b_1 : f a = f b),
    Subtype.mk (p := fun (a : X × X) ↦ f a.1 = f a.2) (a, b) b_1 ∈ Function.pullbackDiagonal f →
      ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f
x : X
t : Set (X × X)
ht : t ∈ 𝓝 x ×ˢ 𝓝 x
t_sub : Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f
t₁ : Set X
h₁ : t₁ ∈ 𝓝 x
t₂ : Set X
h₂ : t₂ ∈ 𝓝 x
prod_sub : t₁ ×ˢ t₂ ⊆ t
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
⟨t₁ ∩ t₂, Filter.inter_mem h₁ h₂,
      fun x₁ h₁ x₂ h₂ he ↦ @t_sub ⟨(x₁, x₂), he⟩ (prod_sub ⟨h₁.1, h₂.2⟩)⟩

Premises used: Filter.inter_mem, Inter.inter, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h :
  ∀ (a b : X) (b_1 : f a = f b),
    Subtype.mk (p := fun (a : X × X) ↦ f a.1 = f a.2) (a, b) b_1 ∈ Function.pullbackDiagonal f →
      ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f
x : X
t : Set (X × X)
ht : t ∈ 𝓝 x ×ˢ 𝓝 x
t_sub : Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f
t₁ : Set X
h₁ : t₁ ∈ 𝓝 x
t₂ : Set X
h₂ : t₂ ∈ 𝓝 x
prod_sub : t₁ ×ˢ t₂ ⊆ t
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
exact ⟨t₁ ∩ t₂, Filter.inter_mem h₁ h₂,
      fun x₁ h₁ x₂ h₂ he ↦ @t_sub ⟨(x₁, x₂), he⟩ (prod_sub ⟨h₁.1, h₂.2⟩)⟩
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
rw : IsOpen[instTopologicalSpaceSubtype] (Set.range (toPullbackDiag f)) ↔ IsOpenEmbedding (toPullbackDiag f)
⊢ IsLocallyInjective f ↔ IsOpenEmbedding (toPullbackDiag f)

Tactic:
rw [isLocallyInjective_iff_isOpen_diagonal, ← range_toPullbackDiag]

Premises used: isLocallyInjective_iff_isOpen_diagonal, range_toPullbackDiag
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsOpen[instTopologicalSpaceSubtype] (Set.range (toPullbackDiag f)) ↔ IsOpenEmbedding (toPullbackDiag f)

Tactic:
⟨fun h ↦ ⟨.toPullbackDiag f, h⟩, fun h ↦ h.isOpen_range⟩

Premises used: Topology.IsEmbedding.toPullbackDiag, Topology.IsOpenEmbedding.isOpen_range, Iff.intro, Topology.IsOpenEmbedding.mk
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsOpen[instTopologicalSpaceSubtype] (Set.range (toPullbackDiag f)) ↔ IsOpenEmbedding (toPullbackDiag f)

Tactic:
exact ⟨fun h ↦ ⟨.toPullbackDiag f, h⟩, fun h ↦ h.isOpen_range⟩
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ IsOpenMap (toPullbackDiag f)

Tactic:
IsLocallyInjective_iff_isOpenEmbedding.trans
    ⟨IsOpenEmbedding.isOpenMap, .of_continuous_injective_isOpenMap
      (IsEmbedding.toPullbackDiag f).continuous (injective_toPullbackDiag f)⟩

Premises used: Topology.IsOpenEmbedding.isOpenMap, injective_toPullbackDiag, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, Topology.IsEmbedding.toPullbackDiag, IsLocallyInjective_iff_isOpenEmbedding, Iff.intro, Iff.trans, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
rw : (∀ (x : X), {x} ∈ 𝓝 x) ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
⊢ DiscreteTopology X ↔ IsLocallyInjective.{u_1, u_2} (Y := Y) fun (x : X) ↦ y

Tactic:
rw [discreteTopology_iff_singleton_mem_nhds, isLocallyInjective_iff_nhds]

Premises used: discreteTopology_iff_singleton_mem_nhds, isLocallyInjective_iff_nhds
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
⊢ (∀ (x : X), {x} ∈ 𝓝 x) ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U

Tactic:
forall_congr' fun x ↦ ⟨fun h ↦ ⟨{x}, h, Set.injOn_singleton _ _⟩, fun ⟨U, hU, inj⟩ ↦ ?_⟩

Premises used: _private.0.discreteTopology_iff_locallyInjective.match_1, Membership.mem, nhds, Set.injOn_singleton, And.intro, Iff.intro, Exists.intro, forall_congr', Singleton.singleton
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
refine :
  ∀ (x : X),
    (∃ U ∈ 𝓝 x, Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U) →
      ∀ (U : Set X) (hU : U ∈ 𝓝 x) (inj : Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U), {x} ∈ 𝓝 x
⊢ (∀ (x : X), {x} ∈ 𝓝 x) ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U

Tactic:
refine forall_congr' fun x ↦ ⟨fun h ↦ ⟨{x}, h, Set.injOn_singleton _ _⟩, fun ⟨U, hU, inj⟩ ↦ ?_⟩

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
x : X
h : ∃ U ∈ 𝓝 x, Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
⊢ U ∈ 𝓝 x

Tactic:
hU
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
x : X
h_1 : ∃ U ∈ 𝓝 x, Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
h : {x} = U
⊢ {x} ∈ 𝓝 x

Tactic:
convert! hU
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
x : X
h_1 : ∃ U ∈ 𝓝 x, Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
h : ∀ (x' : X), Membership.mem (γ := Set X) {x} x' ↔ x' ∈ U
⊢ {x} = U

Tactic:
ext x'
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
x : X
h : ∃ U ∈ 𝓝 x, Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
x' : X
⊢ Membership.mem (γ := Set X) {x} x' ↔ x' ∈ U

Tactic:
⟨?_, fun h ↦ inj h (mem_of_mem_nhds hU) rfl⟩

Premises used: mem_of_mem_nhds, Iff.intro, rfl
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
x : X
h_1 : ∃ U ∈ 𝓝 x, Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
x' : X
h : Membership.mem (γ := Set X) {x} x' → x' ∈ U
⊢ Membership.mem (γ := Set X) {x} x' ↔ x' ∈ U

Tactic:
refine ⟨?_, fun h ↦ inj h (mem_of_mem_nhds hU) rfl⟩
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
U : Set X
inj : Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
x' : X
h : ∃ U ∈ 𝓝 x', Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
hU : U ∈ 𝓝 x'
⊢ x' ∈ U

Tactic:
mem_of_mem_nhds hU

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
U : Set X
inj : Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
x' : X
h : ∃ U ∈ 𝓝 x', Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
hU : U ∈ 𝓝 x'
⊢ x' ∈ U

Tactic:
exact mem_of_mem_nhds hU

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
A : Type u_1
f : X → Y
hf : IsLocallyInjective f
g : Y → A
hg : Function.Injective g
⊢ IsLocallyInjective (g ∘ f)

Tactic:
fun x ↦ let ⟨U, hU, hx, inj⟩ := hf x; ⟨U, hU, hx, hg.comp_injOn inj⟩

Premises used: Function.comp, Membership.mem, Exists, IsLocallyInjective, Function.Injective.comp_injOn, _private.0.IsLocallyInjective.comp_left.match_1, And, And.intro, Exists.intro, IsOpen, Set.InjOn
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
hf : IsLocallyInjective f
g : A → X
cont : Continuous[inst_1, inst] g
hg : Function.Injective g
rw :
  ∀ (hf : IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)) {g : A → X}
    (cont : Continuous[inst_1, inst] g) (hg : Function.Injective g),
    IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal (f ∘ g))
⊢ IsLocallyInjective (f ∘ g)

Tactic:
rw [isLocallyInjective_iff_isOpen_diagonal] at hf ⊢

Premises used: isLocallyInjective_iff_isOpen_diagonal
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
hf : IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → X
cont : Continuous[inst_1, inst] g
hg : Function.Injective g
rw : IsOpen[instTopologicalSpaceSubtype] (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)
⊢ IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal (f ∘ g))

Tactic:
rw [← hg.preimage_pullbackDiagonal]

Premises used: Function.Injective.preimage_pullbackDiagonal
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
hf : IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → X
cont : Continuous[inst_1, inst] g
hg : Function.Injective g
⊢ IsOpen[instTopologicalSpaceSubtype] (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)

Tactic:
apply hf.preimage (cont.mapPullback cont)

Premises used: IsOpen.preimage, Continuous.mapPullback
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
g₁ g₂ : A → X
h₁ : Continuous[inst_1, inst] g₁
h₂ : Continuous[inst_1, inst] g₂
sep : IsSeparatedMap f
he : f ∘ g₁ = f ∘ g₂
g : A → Function.Pullback f f := fun (a : A) ↦ Subtype.mk (p := fun (p : X × X) ↦ f p.1 = f p.2) (g₁ a, g₂ a) ⋯
⊢ Continuous[inst_1, instTopologicalSpaceSubtype] g

Tactic:
fun_prop
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Type u_2
A : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace A
f : X → Y
g₁ g₂ : A → X
h₁ : Continuous[inst_1, inst] g₁
h₂ : Continuous[inst_1, inst] g₂
inj : IsLocallyInjective f
he : f ∘ g₁ = f ∘ g₂
g : A → Function.Pullback f f := fun (a : A) ↦ Subtype.mk (p := fun (p : X × X) ↦ f p.1 = f p.2) (g₁ a, g₂ a) ⋯
⊢ Continuous[inst_1, instTopologicalSpaceSubtype] g

Tactic:
fun_prop
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
E : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace A
p : E → X
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
inst_2 : PreconnectedSpace A
h₁ : Continuous[inst_1, inst] g₁
h₂ : Continuous[inst_1, inst] g₂
he : p ∘ g₁ = p ∘ g₂
a : A
ha : g₁ a = g₂ a
a' : A
⊢ g₁ a' = g₂ a'

Tactic:
apply (IsClopen.eq_univ ⟨sep.isClosed_eqLocus h₁ h₂ he, inj.isOpen_eqLocus h₁ h₂ he⟩ ⟨a, ha⟩).symm
    ▸ Set.mem_univ a'
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
E : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : IsPreconnected s
h₁ : ContinuousOn g₁ s
h₂ : ContinuousOn g₂ s
he : Set.EqOn (p ∘ g₁) (p ∘ g₂) s
a : A
has : a ∈ s
ha : g₁ a = g₂ a
rw :
  ∀ (he : s.restrict (π := fun (a : A) ↦ X) (p ∘ g₁) = s.restrict (π := fun (a : A) ↦ X) (p ∘ g₂)) {a : A} (has : a ∈ s)
    (ha : g₁ a = g₂ a), s.restrict (π := fun (a : A) ↦ E) g₁ = s.restrict (π := fun (a : A) ↦ E) g₂
⊢ Set.EqOn g₁ g₂ s

Tactic:
rw [← Set.restrict_eq_restrict_iff] at he ⊢

Premises used: Set.restrict_eq_restrict_iff