awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
right : ∀ (d : E) (d_mem : d ∈ D) (hd : d ∈ Ioo (s x) e), False
⊢ False

Tactic:
rcases D_dense.exists_between H with ⟨d, d_mem, hd⟩

Premises used: Dense.exists_between
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
⊢ Membership.mem (γ := Set X) {y : X | s y < d} x

Tactic:
have : x ∈ {y | s y < d} := hd.1
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this_1 : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
this : Membership.mem (γ := Set X) {y : X | s y < d} x
⊢ ∃ f ∈ A d, f x < d

Tactic:
simpa only [hA d, mem_iUnion₂, exists_prop, U, mem_setOf_eq] using this

Premises used: Set.mem_setOf_eq, exists_prop, Set.mem_iUnion₂
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
right : ∀ (f : X → E) (f_mem : f ∈ A d) (hf : f x < d), False
⊢ False

Tactic:
obtain ⟨f, f_mem, hf⟩ : ∃ f ∈ A d, f x < d := by
    have : x ∈ {y | s y < d} := hd.1
    simpa only [hA d, mem_iUnion₂, exists_prop, U, mem_setOf_eq] using this
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this_1 : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
f : X → E
f_mem : f ∈ A d
hf : f x < d
this : e < e
⊢ False

Tactic:
simpa
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
f : X → E
f_mem : f ∈ A d
hf : f x < d
right : e < e
⊢ False

Tactic:
suffices e < e by simpa
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
f : X → E
f_mem : f ∈ A d
hf : f x < d
⊢ e < e

Tactic:
(he (mem_image_of_mem _ (mem_iUnion₂_of_mem d_mem f_mem))).trans_lt hf |>.trans hd.2

Premises used: Set.mem_iUnion₂_of_mem, And.right, Set.mem_image_of_mem, LT.lt.trans, LE.le.trans_lt
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
f : X → E
f_mem : f ∈ A d
hf : f x < d
⊢ e < e

Tactic:
exact (he (mem_image_of_mem _ (mem_iUnion₂_of_mem d_mem f_mem))).trans_lt hf |>.trans hd.2

Premises used: Set.mem_iUnion₂_of_mem, And.right, Set.mem_image_of_mem, LT.lt.trans, LE.le.trans_lt
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, LowerSemicontinuous f
h𝓕 : IsLUB 𝓕 s
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ IsLUB 𝓕' s

Tactic:
exists_countable_upperSemicontinuous_isGLB (E := Eᵒᵈ) h𝓕_cont h𝓕

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, exists_countable_upperSemicontinuous_isGLB, IsLeast, IsLUB, OrderDual
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
x : X
⊢ Filter.comap (toPullbackDiag f) (𝓝 (toPullbackDiag f x)) = 𝓝 x

Tactic:
simp [nhds_induced, Filter.comap_comap, nhds_prod_eq, Filter.comap_prod, Function.comp_def,
      Filter.comap_id']

Premises used: Filter.comap_prod, Function.comp_def, Filter.comap_comap, nhds_induced, nhds_prod_eq, Filter.comap_id'
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X₁ : Type u_1
X₂ : Type u_2
Y₁ : Sort u_3
Y₂ : Sort u_4
Z₁ : Type u_5
Z₂ : Type u_6
inst : TopologicalSpace X₁
inst_1 : TopologicalSpace X₂
inst_2 : TopologicalSpace Z₁
inst_3 : TopologicalSpace Z₂
f₁ : X₁ → Y₁
g₁ : Z₁ → Y₁
f₂ : X₂ → Y₂
g₂ : Z₂ → Y₂
mapX : X₁ → X₂
contX : Continuous[inst, inst_1] mapX
mapY : Y₁ → Y₂
mapZ : Z₁ → Z₂
contZ : Continuous[inst_2, inst_3] mapZ
commX : f₂ ∘ mapX = mapY ∘ f₁
commZ : g₂ ∘ mapZ = mapY ∘ g₁
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (Function.mapPullback mapX mapY mapZ commX commZ)

Tactic:
continuous_induced_rng.mpr (.prodMk ?_ ?_)

Premises used: Iff.mpr, Continuous.prodMk, continuous_induced_rng
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X₁ : Type u_1
X₂ : Type u_2
Y₁ : Sort u_3
Y₂ : Sort u_4
Z₁ : Type u_5
Z₂ : Type u_6
inst : TopologicalSpace X₁
inst_1 : TopologicalSpace X₂
inst_2 : TopologicalSpace Z₁
inst_3 : TopologicalSpace Z₂
f₁ : X₁ → Y₁
g₁ : Z₁ → Y₁
f₂ : X₂ → Y₂
g₂ : Z₂ → Y₂
mapX : X₁ → X₂
contX : Continuous[inst, inst_1] mapX
mapY : Y₁ → Y₂
mapZ : Z₁ → Z₂
contZ : Continuous[inst_2, inst_3] mapZ
commX : f₂ ∘ mapX = mapY ∘ f₁
commZ : g₂ ∘ mapZ = mapY ∘ g₁
refine_1 : Continuous[instTopologicalSpaceSubtype, inst_1] fun (x : Function.Pullback f₁ g₁) ↦ mapX x.fst
refine_2 : Continuous[instTopologicalSpaceSubtype, inst_3] fun (x : Function.Pullback f₁ g₁) ↦ mapZ x.snd
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (Function.mapPullback mapX mapY mapZ commX commZ)

Tactic:
refine continuous_induced_rng.mpr (.prodMk ?_ ?_)

Premises used: Iff.mpr, Continuous.prodMk, continuous_induced_rng
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X₁ : Type u_1
X₂ : Type u_2
Y₁ : Sort u_3
Y₂ : Sort u_4
Z₁ : Type u_5
Z₂ : Type u_6
inst : TopologicalSpace X₁
inst_1 : TopologicalSpace X₂
inst_2 : TopologicalSpace Z₁
inst_3 : TopologicalSpace Z₂
f₁ : X₁ → Y₁
g₁ : Z₁ → Y₁
f₂ : X₂ → Y₂
g₂ : Z₂ → Y₂
mapX : X₁ → X₂
contX : Continuous[inst, inst_1] mapX
mapY : Y₁ → Y₂
mapZ : Z₁ → Z₂
contZ : Continuous[inst_2, inst_3] mapZ
commX : f₂ ∘ mapX = mapY ∘ f₁
commZ : g₂ ∘ mapZ = mapY ∘ g₁
⊢ Continuous[instTopologicalSpaceSubtype, inst_1] fun (x : Function.Pullback f₁ g₁) ↦ mapX x.fst

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

Premises used: continuous_subtype_val, Continuous.comp, continuous_snd, continuous_fst
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X₁ : Type u_1
X₂ : Type u_2
Y₁ : Sort u_3
Y₂ : Sort u_4
Z₁ : Type u_5
Z₂ : Type u_6
inst : TopologicalSpace X₁
inst_1 : TopologicalSpace X₂
inst_2 : TopologicalSpace Z₁
inst_3 : TopologicalSpace Z₂
f₁ : X₁ → Y₁
g₁ : Z₁ → Y₁
f₂ : X₂ → Y₂
g₂ : Z₂ → Y₂
mapX : X₁ → X₂
contX : Continuous[inst, inst_1] mapX
mapY : Y₁ → Y₂
mapZ : Z₁ → Z₂
contZ : Continuous[inst_2, inst_3] mapZ
commX : f₂ ∘ mapX = mapY ∘ f₁
commZ : g₂ ∘ mapZ = mapY ∘ g₁
⊢ Continuous[instTopologicalSpaceSubtype, inst_3] fun (x : Function.Pullback f₁ g₁) ↦ mapZ x.snd

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

Premises used: continuous_subtype_val, Continuous.comp, continuous_snd, continuous_fst
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
y : Y
⊢ T2Space X ↔ IsSeparatedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y

Tactic:
⟨fun ⟨t2⟩ _ _ _ hne ↦ t2 hne, fun sep ↦ ⟨fun x₁ x₂ hne ↦ sep x₁ x₂ rfl hne⟩⟩

Premises used: Disjoint, Membership.mem, Exists, _private.0.t2space_iff_isSeparatedMap.match_1, And, Iff.intro, IsOpen, T2Space.mk, rfl
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
inst_1 : T2Space X
f : X → Y
⊢ IsSeparatedMap f

Tactic:
fun _ _ _ ↦ t2_separation

Premises used: IsSeparatedMap, t2_separation
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
inj : Injective f
⊢ IsSeparatedMap f

Tactic:
fun _ _ he hne ↦ (hne (inj he)).elim

Premises used: IsSeparatedMap, False.elim
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
x x' : X
h : f x = f x'
⊢ (x ≠ x' → ∃ (s₁ : Set X) (s₂ : Set X), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ x ∈ s₁ ∧ x' ∈ s₂ ∧ Disjoint s₁ s₂) ↔
    x ≠ x' → Disjoint (𝓝 x) (𝓝 x')

Tactic:
simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens x'),
    ← exists_and_left, and_assoc, and_comm, and_left_comm]

Premises used: exists_and_left, and_left_comm, and_comm, Filter.HasBasis.disjoint_iff, and_assoc, nhds_basis_opens
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
simp_rw :
  (∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → Disjoint (𝓝 x₁) (𝓝 x₂)) ↔
    ∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
⊢ IsSeparatedMap f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂

Tactic:
simp_rw [isSeparatedMap_iff_disjoint_nhds, Filter.disjoint_iff]

Premises used: isSeparatedMap_iff_disjoint_nhds, Filter.disjoint_iff
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
simp_rw :
  (∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂) ↔
    ∀ (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)ᶜ →
        Membership.mem (γ := Filter (Function.Pullback f f))
          (comap (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2)) (𝓝 a ×ˢ 𝓝 b)) (Function.pullbackDiagonal f)ᶜ
⊢ IsSeparatedMap f ↔ IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)

Tactic:
simp_rw [isSeparatedMap_iff_nhds, ← isOpen_compl_iff, isOpen_iff_mem_nhds,
    Subtype.forall, Prod.forall, nhds_induced, nhds_prod_eq]

Premises used: Subtype.forall, nhds_induced, isSeparatedMap_iff_nhds, Prod.forall, nhds_prod_eq, isOpen_iff_mem_nhds, isOpen_compl_iff
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
⊢ (∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂) ↔
    ∀ (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)ᶜ →
        Membership.mem (γ := Filter (Function.Pullback f f))
          (comap (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2)) (𝓝 a ×ˢ 𝓝 b)) (Function.pullbackDiagonal f)ᶜ

Tactic:
forall₄_congr fun x₁ x₂ _ _ ↦ ⟨fun h ↦ ?_, fun ⟨t, ht, t_sub⟩ ↦ ?_⟩

Premises used: Set.Mem, setOf, Disjoint, Membership.mem, Exists, nhds, Function.Pullback.fst, Function.Pullback.snd, _private.0.isSeparatedMap_iff_isClosed_diagonal.match_5, And, Function.pullbackDiagonal, Iff.intro, Not, forall₄_congr
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
refine_1 :
  ∀ (x₁ x₂ : X),
    f x₁ = f x₂ →
      x₁ ≠ x₂ →
        ∀ (h : ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂),
          Membership.mem (γ := Filter (Function.Pullback f f))
            (comap (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2)) (𝓝 x₁ ×ˢ 𝓝 x₂)) (Function.pullbackDiagonal f)ᶜ
refine_2 :
  ∀ (x₁ x₂ : X),
    f x₁ = f x₂ →
      x₁ ≠ x₂ →
        Membership.mem (γ := Filter (Function.Pullback f f))
            (comap (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2)) (𝓝 x₁ ×ˢ 𝓝 x₂)) (Function.pullbackDiagonal f)ᶜ →
          ∀ (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)ᶜ),
            ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
⊢ (∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂) ↔
    ∀ (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)ᶜ →
        Membership.mem (γ := Filter (Function.Pullback f f))
          (comap (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2)) (𝓝 a ×ˢ 𝓝 b)) (Function.pullbackDiagonal f)ᶜ

Tactic:
refine forall₄_congr fun x₁ x₂ _ _ ↦ ⟨fun h ↦ ?_, fun ⟨t, ht, t_sub⟩ ↦ ?_⟩

Premises used: Iff.intro, forall₄_congr
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
x₁ x₂ : X
h_1 : f x₁ = f x₂
h_2 : x₁ ≠ x₂
h : ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
⊢ (diagonal X)ᶜ ∈ 𝓝 x₁ ×ˢ 𝓝 x₂

Tactic:
simp_rw [← Filter.disjoint_iff, ← compl_diagonal_mem_prod] at h

Premises used: Filter.disjoint_iff, Filter.compl_diagonal_mem_prod
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
x₁ x₂ : X
h_1 : f x₁ = f x₂
h_2 : x₁ ≠ x₂
h : (diagonal X)ᶜ ∈ 𝓝 x₁ ×ˢ 𝓝 x₂
⊢ Membership.mem (γ := Filter (Function.Pullback f f))
    (comap (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2)) (𝓝 x₁ ×ˢ 𝓝 x₂)) (Function.pullbackDiagonal f)ᶜ

Tactic:
⟨_, h, subset_rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, subset_rfl
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
x₁ x₂ : X
h_1 : f x₁ = f x₂
h_2 : x₁ ≠ x₂
h : (diagonal X)ᶜ ∈ 𝓝 x₁ ×ˢ 𝓝 x₂
⊢ Membership.mem (γ := Filter (Function.Pullback f f))
    (comap (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2)) (𝓝 x₁ ×ˢ 𝓝 x₂)) (Function.pullbackDiagonal f)ᶜ

Tactic:
exact ⟨_, h, subset_rfl⟩
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
x₁ x₂ : X
h : f x₁ = f x₂
h_1 : x₁ ≠ x₂
h_2 :
  Membership.mem (γ := Filter (Function.Pullback f f))
    (comap (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2)) (𝓝 x₁ ×ˢ 𝓝 x₂)) (Function.pullbackDiagonal f)ᶜ
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 :
  ∀ (s₁ : Set X) (h₁ : s₁ ∈ 𝓝 x₁) (s₂ : Set X) (h₂ : s₂ ∈ 𝓝 x₂) (s_sub : s₁ ×ˢ s₂ ⊆ t),
    ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
⊢ ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂

Tactic:
obtain ⟨s₁, h₁, s₂, h₂, s_sub⟩ := mem_prod_iff.mp ht

Premises used: Iff.mp, Filter.mem_prod_iff
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
x₁ x₂ : X
h : f x₁ = f x₂
h_1 : x₁ ≠ x₂
h_2 :
  Membership.mem (γ := Filter (Function.Pullback f f))
    (comap (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2)) (𝓝 x₁ ×ˢ 𝓝 x₂)) (Function.pullbackDiagonal f)ᶜ
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)ᶜ
s₁ : Set X
h₁ : s₁ ∈ 𝓝 x₁
s₂ : Set X
h₂ : s₂ ∈ 𝓝 x₂
s_sub : s₁ ×ˢ s₂ ⊆ t
⊢ ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂

Tactic:
⟨s₁, h₁, s₂, h₂, disjoint_left.2 fun x h₁ h₂ ↦ @t_sub ⟨(x, x), rfl⟩ (s_sub ⟨h₁, h₂⟩) rfl⟩

Premises used: Iff.mpr, Set.disjoint_left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
x₁ x₂ : X
h : f x₁ = f x₂
h_1 : x₁ ≠ x₂
h_2 :
  Membership.mem (γ := Filter (Function.Pullback f f))
    (comap (Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2)) (𝓝 x₁ ×ˢ 𝓝 x₂)) (Function.pullbackDiagonal f)ᶜ
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)ᶜ
s₁ : Set X
h₁ : s₁ ∈ 𝓝 x₁
s₂ : Set X
h₂ : s₂ ∈ 𝓝 x₂
s_sub : s₁ ×ˢ s₂ ⊆ t
⊢ ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂

Tactic:
exact ⟨s₁, h₁, s₂, h₂, disjoint_left.2 fun x h₁ h₂ ↦ @t_sub ⟨(x, x), rfl⟩ (s_sub ⟨h₁, h₂⟩) rfl⟩
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
rw : IsClosed[instTopologicalSpaceSubtype] (Set.range (toPullbackDiag f)) ↔ IsClosedEmbedding (toPullbackDiag f)
⊢ IsSeparatedMap f ↔ IsClosedEmbedding (toPullbackDiag f)

Tactic:
rw [isSeparatedMap_iff_isClosed_diagonal, ← range_toPullbackDiag]

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

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

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

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

Tactic:
isSeparatedMap_iff_isClosedEmbedding.trans
    ⟨IsClosedEmbedding.isClosedMap, .of_continuous_injective_isClosedMap
      (IsEmbedding.toPullbackDiag f).continuous (injective_toPullbackDiag f)⟩

Premises used: injective_toPullbackDiag, Topology.IsClosedEmbedding.isClosedMap, isSeparatedMap_iff_isClosedEmbedding, Topology.IsEmbedding.toPullbackDiag, Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap, Iff.intro, Iff.trans, Topology.IsEmbedding.continuous