awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsSeparatedMap f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
have 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₂
Tactic: simp_rw [isSeparatedMap_iff_disjoint_nhds, Filter.disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsSeparatedMap f ↔ IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
have 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)ᶜ
Tactic: simp_rw [isSeparatedMap_iff_nhds, ← isOpen_compl_iff, isOpen_iff_mem_nhds,
    Subtype.forall, Prod.forall, nhds_induced, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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)ᶜ
have 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)ᶜ
Tactic: refine forall₄_congr fun x₁ x₂ _ _ ↦ ⟨fun h ↦ ?_, fun ⟨t, ht, t_sub⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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)ᶜ
⊢ (∀ (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)ᶜ
have 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₂
Tactic: refine forall₄_congr fun x₁ x₂ _ _ ↦ ⟨fun h ↦ ?_, fun ⟨t, ht, t_sub⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (hypothesis)
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₂
⊢ 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)ᶜ
have h₁ : (diagonal X)ᶜ ∈ 𝓝 x₁ ×ˢ 𝓝 x₂
Tactic: simp_rw [← Filter.disjoint_iff, ← compl_diagonal_mem_prod] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
have 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₂
Tactic: obtain ⟨s₁, h₁, s₂, h₂, s_sub⟩ := mem_prod_iff.mp ht
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
Goal:
X : Type u_1
Y : Sort u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsSeparatedMap f ↔ IsClosedEmbedding (toPullbackDiag f)
have rw : IsClosed[instTopologicalSpaceSubtype] (Set.range (toPullbackDiag f)) ↔ IsClosedEmbedding (toPullbackDiag f)
Tactic: rw [isSeparatedMap_iff_isClosed_diagonal, ← range_toPullbackDiag]
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
⊢ IsSeparatedMap (X := Function.Pullback f g) snd
have rw : ∀ (sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)) (g : A → Y),
  IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal snd)
Tactic: rw [isSeparatedMap_iff_isClosed_diagonal] at sep ⊢
Cleared hypotheses: sep, g
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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.pullbackDiagonal snd)
have rw : IsClosed[instTopologicalSpaceSubtype] (Function.PullbackSelf.map_fst ⁻¹' Function.pullbackDiagonal f)
Tactic: rw [← preimage_map_fst_pullbackDiagonal]
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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)
have refine_1 : Continuous[instTopologicalSpaceSubtype, inst] fst
Tactic: refine sep.preimage (Continuous.mapPullback ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
⊢ IsSeparatedMap (f ∘ g)
have 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))
Tactic: rw [isSeparatedMap_iff_isClosed_diagonal] at sep ⊢
Cleared hypotheses: sep, g, cont, inj
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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.pullbackDiagonal (f ∘ g))
have rw : IsClosed[instTopologicalSpaceSubtype] (Function.mapPullback g id g sorry sorry ⁻¹' Function.pullbackDiagonal f)
Tactic: rw [← inj.preimage_pullbackDiagonal]
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
have mp : IsLocallyInjective f → ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
⊢ IsLocallyInjective f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
have mpr : (∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) → IsLocallyInjective f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U
have mp : ∀ (U : Set X) (ho : IsOpen[inst] U) (hm : x ∈ U) (hi : Set.InjOn f U), ∃ U ∈ 𝓝 x, Set.InjOn f U
Tactic: obtain ⟨U, ho, hm, hi⟩ := h x
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn f U
have mpr : ∀ (U : Set X) (hn : U ∈ 𝓝 x) (hi : Set.InjOn f U), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn f U
Tactic: obtain ⟨U, hn, hi⟩ := h x
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
have 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
Tactic: simp_rw [isLocallyInjective_iff_nhds, isOpen_iff_mem_nhds,
    Subtype.forall, Prod.forall, nhds_induced, nhds_prod_eq, Filter.mem_comap]
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
have 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
Tactic: refine ⟨?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
⊢ (∀ (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
have 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
Tactic: refine ⟨?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
⊢ ∃ t ∈ 𝓝 x ×ˢ 𝓝 x, Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' t ⊆ Function.pullbackDiagonal f
have 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
Tactic: obtain ⟨U, hn, hi⟩ := h x
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U
have 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
Tactic: obtain ⟨t, ht, t_sub⟩ := h x x rfl rfl
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U
have 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
Tactic: obtain ⟨t₁, h₁, t₂, h₂, prod_sub⟩ := Filter.mem_prod_iff.mp ht
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ IsOpenEmbedding (toPullbackDiag f)
have rw : IsOpen[instTopologicalSpaceSubtype] (Set.range (toPullbackDiag f)) ↔ IsOpenEmbedding (toPullbackDiag f)
Tactic: rw [isLocallyInjective_iff_isOpen_diagonal, ← range_toPullbackDiag]
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
⊢ DiscreteTopology X ↔ IsLocallyInjective.{u_1, u_2} (Y := Y) fun (x : X) ↦ y
have rw : (∀ (x : X), {x} ∈ 𝓝 x) ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn.{u_1, u_2} (β := Y) (fun (x : X) ↦ y) U
Tactic: rw [discreteTopology_iff_singleton_mem_nhds, isLocallyInjective_iff_nhds]
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
have 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
Tactic: refine forall_congr' fun x ↦ ⟨fun h ↦ ⟨{x}, h, Set.injOn_singleton _ _⟩, fun ⟨U, hU, inj⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
have h : {x} = U
Tactic: convert! hU
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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} = U
have h : ∀ (x' : X), Membership.mem (γ := Set X) {x} x' ↔ x' ∈ U
Tactic: ext x'
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
have h : Membership.mem (γ := Set X) {x} x' → x' ∈ U
Tactic: refine ⟨?_, fun h ↦ inj h (mem_of_mem_nhds hU) rfl⟩
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
⊢ IsLocallyInjective (f ∘ g)
have 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))
Tactic: rw [isLocallyInjective_iff_isOpen_diagonal] at hf ⊢
Cleared hypotheses: hf, g, cont, hg
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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.pullbackDiagonal (f ∘ g))
have rw : IsOpen[instTopologicalSpaceSubtype] (Function.mapPullback g id g sorry sorry ⁻¹' Function.pullbackDiagonal f)
Tactic: rw [← hg.preimage_pullbackDiagonal]
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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
⊢ Set.EqOn g₁ g₂ s
have 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₂
Tactic: rw [← Set.restrict_eq_restrict_iff] at he ⊢
Cleared hypotheses: he, a, has, ha
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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 : 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₂
have rw : ∀ (h₁ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₁))
  (h₂ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₂))
  (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₂
Tactic: rw [continuousOn_iff_continuous_restrict] at h₁ h₂
Cleared hypotheses: h₁, h₂, he, a, has, ha
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
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₁ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₁)
h₂ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₂)
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₂
have rw : ∀ (hs : PreconnectedSpace.{u_3} (↑s : Type u_3))
  (h₁ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₁))
  (h₂ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₂))
  (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₂
Tactic: rw [isPreconnected_iff_preconnectedSpace] at hs
Cleared hypotheses: hs, h₁, h₂, he, a, has, ha
-- Lean 4 proof step from Mathlib.Topology.Separation.AlexandrovDiscrete (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
⊢ nhdsKer s = s
have h : ∀ (x : X), x ∈ nhdsKer s ↔ x ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : ∀ s ∈ b, x ∈ s ↔ y ∈ s
⊢ (𝓝 y).HasBasis (fun (t : Set X) ↦ t ∈ b ∧ x ∈ t) fun (t : Set X) ↦ t
have h₁ : ∀ (x_1 : Set X), x_1 ∈ b ∧ x ∈ x_1 ↔ x_1 ∈ b ∧ y ∈ x_1
Tactic: convert! hb.nhds_hasBasis using 2
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsClosed[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst] t → t = s
⊢ s.Subsingleton
have refine : ∀ (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y), False
Tactic: refine fun x hx y hy => of_not_not fun hxy => ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsClosed[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
⊢ False
have rcases : ∀ (U : Set X) (hUo : IsOpen[inst] U) (hU : Xor (x ∈ U) (y ∈ U)), False
Tactic: rcases exists_isOpen_xor_mem hxy with ⟨U, hUo, hU⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsClosed[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst] U
hU : Xor (x ∈ U) (y ∈ U)
⊢ False
have inr : ∀
  (this :
    ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsClosed s)
      (hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y)
      (U : Set X) (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False)
  (h : ¬(x ∈ U ∧ y ∉ U)), False
Tactic: wlog h : x ∈ U ∧ y ∉ U
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsClosed[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst] U
hU : Xor (x ∈ U) (y ∈ U)
inr :
  ∀
    (this :
      ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsClosed s)
        (hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y)
        (U : Set X) (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False)
    (h : ¬(x ∈ U ∧ y ∉ U)), False
⊢ False
have wlog : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsClosed s)
  (hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y) (U : Set X)
  (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False
Tactic: wlog h : x ∈ U ∧ y ∉ U
Cleared hypotheses: inst_1, s, hs, hmin, x, hx, y, hy, hxy, U, hUo, hU
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : T0Space X
s : Set X
hs : IsClosed[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst_1] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst_1] U
hU : Xor (x ∈ U) (y ∈ U)
h : x ∈ U ∧ y ∉ U
⊢ False
have hxU : x ∈ U
Tactic: obtain ⟨hxU, hyU⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : T0Space X
s : Set X
hs : IsClosed[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst_1] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst_1] U
hU : Xor (x ∈ U) (y ∈ U)
h : x ∈ U ∧ y ∉ U
hxU : x ∈ U
⊢ False
have hyU : y ∉ U
Tactic: obtain ⟨hxU, hyU⟩ := h
Cleared hypotheses: h