awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₀ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₁ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₂ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₃ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₁₄ : y ∉ u → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₀ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₁ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₂ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₃ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₄ : y ∉ u → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₁₅ : ¬(y ∈ T ∧ y ∉ {x}) → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₀ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₁ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₂ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₃ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₄ : y ∉ u → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₅ a₁₆ a₁₇ : ¬(y ∈ T ∧ y ∉ {x}) → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₁₈ : y ∈ S → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₀ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₁ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₂ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₃ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₄ : y ∉ u → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₅ a₁₆ a₁₇ : ¬(y ∈ T ∧ y ∉ {x}) → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₈ : y ∈ S → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₁₉ : y ∉ u → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₀ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₁ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₂ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₃ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₄ : y ∉ u → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₅ a₁₆ a₁₇ : ¬(y ∈ T ∧ y ∉ {x}) → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₈ : y ∈ S → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₉ : y ∉ u → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₂₀ : ¬y ∉ {x} → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₀ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₁ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₂ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₃ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₄ : y ∉ u → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₅ a₁₆ a₁₇ : ¬(y ∈ T ∧ y ∉ {x}) → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₈ : y ∈ S → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₉ : y ∉ u → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₀ : ¬y ∉ {x} → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₂₁ : y ∉ T → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₀ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₁ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₂ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₃ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₄ : y ∉ u → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₅ a₁₆ a₁₇ : ¬(y ∈ T ∧ y ∉ {x}) → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₈ : y ∈ S → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₉ : y ∉ u → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₀ : ¬y ∉ {x} → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₁ : y ∉ T → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₂₂ : ¬y ∉ S → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₀ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₁ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₂ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₃ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₄ : y ∉ u → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₅ a₁₆ a₁₇ : ¬(y ∈ T ∧ y ∉ {x}) → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₈ : y ∈ S → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₉ : y ∉ u → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₀ : ¬y ∉ {x} → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₁ : y ∉ T → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₂ a₂₃ a₂₄ : ¬y ∉ S → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₂₅ : y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → y ∉ T → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₀ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₁ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₂ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₃ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₄ : y ∉ u → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₅ a₁₆ a₁₇ : ¬(y ∈ T ∧ y ∉ {x}) → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₈ : y ∈ S → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₉ : y ∉ u → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₀ : ¬y ∉ {x} → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₁ : y ∉ T → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₂ a₂₃ a₂₄ : ¬y ∉ S → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₅ : y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → y ∉ T → False
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₂₆ : y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → ¬y ∉ {x} → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₀ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₁ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₂ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₃ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₄ : y ∉ u → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₅ a₁₆ a₁₇ : ¬(y ∈ T ∧ y ∉ {x}) → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₈ : y ∈ S → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₉ : y ∉ u → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₀ : ¬y ∉ {x} → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₁ : y ∉ T → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₂ a₂₃ a₂₄ : ¬y ∉ S → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₅ : y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → y ∉ T → False
a₂₆ : y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → ¬y ∉ {x} → False
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₂₇ : y ∈ S → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, S ∪ Tᶜ ∈ 𝓝[≠] x
have simp_rw : (∀ x ∈ T, Disjoint (𝓝[≠] x) (𝓟 (T \ S))) ↔ ∀ x ∈ T, S ∪ Tᶜ ∈ 𝓝[≠] x
Tactic: simp_rw [mem_codiscreteWithin, disjoint_principal_right, Set.compl_diff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
simp_rw : (∀ x ∈ T, Disjoint (𝓝[≠] x) (𝓟 (T \ S))) ↔ ∀ x ∈ T, S ∪ Tᶜ ∈ 𝓝[≠] x
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, S ∪ Tᶜ ∈ 𝓝[≠] x
have simp_rw₁ : (∀ x ∈ T, (T \ S)ᶜ ∈ 𝓝[≠] x) ↔ ∀ x ∈ T, S ∪ Tᶜ ∈ 𝓝[≠] x
Tactic: simp_rw [mem_codiscreteWithin, disjoint_principal_right, Set.compl_diff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
⊢ codiscreteWithin U₁ ≤ codiscreteWithin U
have refine : ∀ x ∈ U, 𝓝[U₁ \ {x}] x ≤ 𝓝[U \ {x}] x
Tactic: refine (biSup_mono hU).trans <| iSup₂_mono fun _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ IsDiscrete (s ∩ U)
have rw : ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, 𝓝[≠] x ⊓ 𝓟 (sᶜ ∪ Uᶜ)ᶜ = ⊥
Tactic: rw [(by simp : ((s ∩ U) : Set X) = ((sᶜ ∪ Uᶜ)ᶜ : Set X)), isDiscrete_iff_nhdsNE]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, 𝓝[≠] x ⊓ 𝓟 (sᶜ ∪ Uᶜ)ᶜ = ⊥
have simp_rw : ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, sᶜ ∪ Uᶜ ∈ 𝓝[≠] x
Tactic: simp_rw [← Filter.mem_iff_inf_principal_compl]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
⊢ s ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
have simp : (∀ x ∈ U, (U \ s)ᶜ ∈ 𝓝[≠] x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
Tactic: simp only [mem_codiscreteWithin, disjoint_principal_right]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
⊢ (∀ x ∈ U, (U \ s)ᶜ ∈ 𝓝[≠] x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
have refine : ∀ (h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) (z : X) (hz : z ∈ U), (U \ s)ᶜ ∈ 𝓝[≠] z
Tactic: refine ⟨fun h z hz ↦ ⟨(U \ s)ᶜ, h z hz, by simp⟩, fun h z hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
hz : z ∈ U
⊢ (U \ s)ᶜ ∈ 𝓝[≠] z
have rw : ∃ t ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ
Tactic: rw [← exists_mem_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ
have obtain : ∀ (t : Set X) (h₁t : t ∈ 𝓝[≠] z) (h₂t : t ∩ (U \ s) = ∅), ∃ t ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ
Tactic: obtain ⟨t, h₁t, h₂t⟩ := h z hz
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
hz : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
w : Set X
left : t ∈ 𝓝[≠] z
⊢ ∃ t ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ
have right : t ⊆ (U \ s)ᶜ
Tactic: use t, h₁t, (disjoint_iff_inter_eq_empty.mpr h₂t).subset_compl_right
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
⊢ IsClosed[inst] (U \ s)
have rw : ∀ x ∈ (U \ s)ᶜ, ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
Tactic: rw [← isOpen_compl_iff, isOpen_iff_eventually]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
have pos : ∀ (h₁x : x ∈ U), ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
Tactic: by_cases h₁x : x ∈ U
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
pos : ∀ (h₁x : x ∈ U), ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
have neg : ∀ (h₁x : x ∉ U), ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
Tactic: by_cases h₁x : x ∈ U
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
have pos : ∀ (hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))) (hU : IsClosed[inst] U) (x : X) (hx : x ∈ (U \ s)ᶜ) (h₁x : x ∈ U),
  ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
Tactic: rw [mem_codiscreteWithin] at hs
Cleared hypotheses: hs, hU, x, hx, h₁x
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
have h : ∀ (a : X), (Membership.mem (γ := Set X) {x}ᶜ a → a ∉ U \ s) → a ∈ (U \ s)ᶜ
Tactic: filter_upwards [eventually_nhdsWithin_iff.1 (disjoint_principal_right.1 (hs x h₁x))]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : Membership.mem (γ := Set X) {x}ᶜ a → a ∉ U \ s
⊢ a ∈ (U \ s)ᶜ
have pos : ∀ (h₂a : a = x), a ∈ (U \ s)ᶜ
Tactic: by_cases h₂a : a = x
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : Membership.mem (γ := Set X) {x}ᶜ a → a ∉ U \ s
pos : ∀ (h₂a : a = x), a ∈ (U \ s)ᶜ
⊢ a ∈ (U \ s)ᶜ
have neg : ∀ (h₂a : ¬a = x), a ∈ (U \ s)ᶜ
Tactic: by_cases h₂a : a = x
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : Membership.mem (γ := Set X) {x}ᶜ a → a ∉ U \ s
h₂a : a = x
⊢ a ∈ (U \ s)ᶜ
have pos : ∀ (hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U ∩ sᶜ))) (hU : IsClosed[inst] U) (hx : ¬(True ∧ x ∉ s)) (h₁x : x ∈ U)
  (ha : x ∉ {x} → ¬False) (h₂a : a = x), ¬False
Tactic: tauto_set
Cleared hypotheses: hs, hU, hx, h₁x, ha, h₂a
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : Membership.mem (γ := Set X) {x}ᶜ a → a ∉ U \ s
h₂a : ¬a = x
⊢ a ∈ (U \ s)ᶜ
have ha₁ : a ∉ U \ s
Tactic: specialize ha h₂a
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
h₂a : ¬a = x
ha : a ∉ U \ s
⊢ a ∈ (U \ s)ᶜ
have neg : ∀ (hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U ∩ sᶜ))) (hU : IsClosed[inst] U) (hx : ¬(True ∧ x ∉ s)) (h₁x : x ∈ U)
  (h₂a : ¬a = x) (ha : ¬(a ∈ U ∧ a ∉ s)), ¬False
Tactic: tauto_set
Cleared hypotheses: hs, hU, hx, h₁x, h₂a, ha
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
have neg : ∃ v ∈ 𝓝 x, ∀ y ∈ v, y ∈ (U \ s)ᶜ
Tactic: rw [eventually_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
⊢ ∃ v ∈ 𝓝 x, ∀ y ∈ v, y ∈ (U \ s)ᶜ
have right : ∀ y ∈ Uᶜ, y ∈ (U \ s)ᶜ
Tactic: use Uᶜ, hU.compl_mem_nhds h₁x
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
y : X
hy : y ∈ Uᶜ
⊢ y ∈ (U \ s)ᶜ
have right : ∀ (hx : ¬(False ∧ x ∉ s)) (h₁x : x ∉ U) (hy : y ∉ U), ¬(False ∧ y ∉ s)
Tactic: tauto_set
Cleared hypotheses: hx, h₁x, hy
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hU : U ∈ 𝓝[≠] x
hs : Finite.{u_3 + 1} (↑s : Type u_3)
⊢ U \ s ∈ 𝓝[≠] x
have rw : ∀ (hU : ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U) (hs : Finite.{u_3 + 1} (↑s : Type u_3)),
  ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s
Tactic: rw [mem_nhdsWithin] at hU ⊢
Cleared hypotheses: hU, hs
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hU : ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U
hs : Finite.{u_3 + 1} (↑s : Type u_3)
⊢ ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s
have obtain : ∀ (t : Set X) (ht : IsOpen[inst] t) (h₁ts : x ∈ t) (h₂ts : t ∩ {x}ᶜ ⊆ U),
  ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s
Tactic: obtain ⟨t, ht, h₁ts, h₂ts⟩ := hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hs : Finite.{u_3 + 1} (↑s : Type u_3)
t : Set X
ht : IsOpen[inst] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s
have h : IsOpen[inst] (t \ (s \ {x})) ∧ x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s
Tactic: use t \ (s \ {x})
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hs : Finite.{u_3 + 1} (↑s : Type u_3)
t : Set X
ht : IsOpen[inst] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ IsOpen[inst] (t \ (s \ {x})) ∧ x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s
have h : IsOpen[inst] (t \ (s \ {x}))
Tactic: constructor