awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : IsOpen[inst] (t \ (s \ {x}))
⊢ IsOpen[inst] (t \ (s \ {x})) ∧ x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s
have h₁ : x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s
Tactic: constructor
-- 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}))
have h : IsClosed[inst] (s \ {x} ∪ tᶜ)
Tactic: rw [← isClosed_compl_iff, compl_diff]
-- 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
⊢ x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s
have h : ∀ (h₂ts : ∀ (x_1 : X), x_1 ∈ t ∧ x_1 ∉ {x} → x_1 ∈ U),
  (True ∧ ¬(x ∈ s ∧ x ∉ {x})) ∧ ∀ (x_1 : X), (x_1 ∈ t ∧ ¬(x_1 ∈ s ∧ x_1 ∉ {x})) ∧ x_1 ∉ {x} → x_1 ∈ U ∧ x_1 ∉ s
Tactic: tauto_set
Cleared hypotheses: h₂ts
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
⊢ s ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
have rw : (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
Tactic: rw [codiscreteWithin_iff_locallyEmptyComplementWithin]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
have mp : (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) → ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
mp : (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) → ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
have mpr : (∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite) → ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
have mp : ∀ (t : Set X) (h₁t : t ∈ 𝓝[≠] z) (h₂t : t ∩ (U \ s) = ∅), ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
Tactic: obtain ⟨t, h₁t, h₂t⟩ := h z h₁z
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
⊢ ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
have right : (insert z t ∩ (U \ s)).Finite
Tactic: use insert z t, insert_mem_nhds_iff.mpr h₁t
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
⊢ (insert z t ∩ (U \ s)).Finite
have pos : ∀ (hz : z ∈ U \ s), (insert z t ∩ (U \ s)).Finite
Tactic: by_cases hz : z ∈ U \ s
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
pos : ∀ (hz : z ∈ U \ s), (insert z t ∩ (U \ s)).Finite
⊢ (insert z t ∩ (U \ s)).Finite
have neg : ∀ (hz : z ∉ U \ s), (insert z t ∩ (U \ s)).Finite
Tactic: by_cases hz : z ∈ U \ s
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∈ U \ s
⊢ (insert z t ∩ (U \ s)).Finite
have pos : Set.Finite (α := X) (insert z ∅)
Tactic: rw [inter_comm, inter_insert_of_mem hz, inter_comm, h₂t]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∉ U \ s
⊢ (insert z t ∩ (U \ s)).Finite
have neg : Set.Finite.{u_1} (α := X) ∅
Tactic: rw [inter_comm, inter_insert_of_notMem hz, inter_comm, h₂t]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
z : X
h₁z : z ∈ U
⊢ ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
have mpr : ∀ (t : Set X) (h₁t : t ∈ 𝓝 z) (h₂t : (t ∩ (U \ s)).Finite), ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
Tactic: obtain ⟨t, h₁t, h₂t⟩ := h z h₁z
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝 z
h₂t : (t ∩ (U \ s)).Finite
⊢ ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
have right : t \ (t ∩ (U \ s)) ∩ (U \ s) = ∅
Tactic: use t \ (t ∩ (U \ s)), nhdsNE_of_nhdsNE_sdiff_finite (mem_nhdsWithin_of_mem_nhds h₁t) h₂t
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
x : X
⊢ {x}ᶜ ∈ codiscreteWithin s
have rw : ∀ z ∈ s, ∃ t ∈ 𝓝[≠] z, t ∩ (s \ {x}ᶜ) = ∅
Tactic: rw [codiscreteWithin_iff_locallyEmptyComplementWithin]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
x z : X
hz : z ∈ s
⊢ ∃ t ∈ 𝓝[≠] z, t ∩ (s \ {x}ᶜ) = ∅
have h : univ \ {x} ∈ 𝓝[≠] z ∧ univ \ {x} ∩ (s \ {x}ᶜ) = ∅
Tactic: use univ \ {x}
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
h : t.Finite
⊢ tᶜ ∈ codiscreteWithin s
have empty : ∅ᶜ ∈ codiscreteWithin s
Tactic: apply h.induction_on (motive := fun t _ ↦ tᶜ ∈ codiscreteWithin s)
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
h : t.Finite
empty : ∅ᶜ ∈ codiscreteWithin s
⊢ tᶜ ∈ codiscreteWithin s
have insert : ∀ {a : X} {s_1 : Set X}, a ∉ s_1 → ∀ (hs : s_1.Finite), s_1ᶜ ∈ codiscreteWithin s → (insert a s_1)ᶜ ∈ codiscreteWithin s
Tactic: apply h.induction_on (motive := fun t _ ↦ tᶜ ∈ codiscreteWithin s)
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (hypothesis)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
s t_1 : Set X
h : t_1.Finite
τ : X
t : Set X
hτ : τ ∉ t
h₁t : t.Finite
h₂t : tᶜ ∈ codiscreteWithin s
⊢ (insert τ t)ᶜ ∈ codiscreteWithin s
have this : (insert τ t)ᶜ = {τ}ᶜ ∩ tᶜ
Tactic: have : (insert τ t)ᶜ = {τ}ᶜ ∩ tᶜ := by aesop
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
⊢ S ∈ codiscrete X ↔ IsOpen[inst] S ∧ IsDiscrete Sᶜ
have rw : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)) ↔ IsOpen[inst] S ∧ IsDiscrete Sᶜ
Tactic: rw [mem_codiscrete, ← isClosed_compl_iff, isClosed_and_discrete_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
rw : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)) ↔ IsOpen[inst] S ∧ IsDiscrete Sᶜ
⊢ S ∈ codiscrete X ↔ IsOpen[inst] S ∧ IsDiscrete Sᶜ
have rw₁ : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)) ↔ IsClosed[inst] Sᶜ ∧ IsDiscrete Sᶜ
Tactic: rw [mem_codiscrete, ← isClosed_compl_iff, isClosed_and_discrete_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
rw : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)) ↔ IsOpen[inst] S ∧ IsDiscrete Sᶜ
rw₁ : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)) ↔ IsClosed[inst] Sᶜ ∧ IsDiscrete Sᶜ
⊢ S ∈ codiscrete X ↔ IsOpen[inst] S ∧ IsDiscrete Sᶜ
have rw₂ : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)
Tactic: rw [mem_codiscrete, ← isClosed_compl_iff, isClosed_and_discrete_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
⊢ Sᶜ ∈ codiscrete X ↔ IsClosed[inst] S ∧ IsDiscrete S
have rw : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜᶜ)) ↔ IsClosed[inst] S ∧ IsDiscrete S
Tactic: rw [mem_codiscrete, compl_compl, isClosed_and_discrete_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
rw : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜᶜ)) ↔ IsClosed[inst] S ∧ IsDiscrete S
⊢ Sᶜ ∈ codiscrete X ↔ IsClosed[inst] S ∧ IsDiscrete S
have rw₁ : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)) ↔ IsClosed[inst] S ∧ IsDiscrete S
Tactic: rw [mem_codiscrete, compl_compl, isClosed_and_discrete_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
rw : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜᶜ)) ↔ IsClosed[inst] S ∧ IsDiscrete S
rw₁ : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)) ↔ IsClosed[inst] S ∧ IsDiscrete S
⊢ Sᶜ ∈ codiscrete X ↔ IsClosed[inst] S ∧ IsDiscrete S
have rw₂ : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)
Tactic: rw [mem_codiscrete, compl_compl, isClosed_and_discrete_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
s : Set X
⊢ f '' s ∈ codiscreteWithin (range f) ↔ s ∈ codiscrete X
have rw : f '' s ∈ codiscreteWithin (f '' univ) ↔ s ∈ codiscrete X
Tactic: rw [← image_univ, hf.image_mem_codiscreteWithin, codiscrete]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
s : Set X
rw : f '' s ∈ codiscreteWithin (f '' univ) ↔ s ∈ codiscrete X
⊢ f '' s ∈ codiscreteWithin (range f) ↔ s ∈ codiscrete X
have rw₁ : Membership.mem (γ := Filter X) (codiscreteWithin univ) s ↔ s ∈ codiscrete X
Tactic: rw [← image_univ, hf.image_mem_codiscreteWithin, codiscrete]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
s : Set X
rw : f '' s ∈ codiscreteWithin (f '' univ) ↔ s ∈ codiscrete X
rw₁ : Membership.mem (γ := Filter X) (codiscreteWithin univ) s ↔ s ∈ codiscrete X
⊢ f '' s ∈ codiscreteWithin (range f) ↔ s ∈ codiscrete X
have rw₂ : Membership.mem (γ := Filter X) (codiscreteWithin univ) s ↔ Membership.mem (γ := Filter X) (codiscreteWithin univ) s
Tactic: rw [← image_univ, hf.image_mem_codiscreteWithin, codiscrete]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : Membership.mem (γ := Filter X) cofinite s
⊢ s ∈ codiscrete X
have rw : IsClosed[inst] sᶜ ∧ IsDiscrete sᶜ
Tactic: rw [← compl_compl s, compl_mem_codiscrete_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
S : Set X
x : X
h : AccPt x (𝓟 S)
hs : S.Finite
⊢ False
have this : Sᶜ ∈ codiscrete X
Tactic: have := hs.compl_mem_codiscrete
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
S : Set X
x : X
h : AccPt x (𝓟 S)
hs : S.Finite
this : Sᶜ ∈ codiscrete X
⊢ False
have this₁ : ∀ (x : X), ¬AccPt x (𝓟 S)
Tactic: rw [mem_codiscrete_accPt, compl_compl] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s K : Set X
hK : IsCompact K
hs : s ∈ codiscreteWithin K
⊢ (K \ s).Finite
have hs₁ : ∀ x ∈ K, ¬AccPt x (𝓟 (K \ s))
Tactic: rw [mem_codiscreteWithin_accPt] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s K : Set X
hK : IsCompact K
hs : ∀ x ∈ K, ¬AccPt x (𝓟 (K \ s))
⊢ (K \ s).Finite
have contrapose! : ∀ (hs : (K \ s).Infinite), ∃ x ∈ K, AccPt x (𝓟 (K \ s))
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
inst_1 : T1Space X
hK : IsCompact K
⊢ codiscreteWithin K = cofinite ⊓ 𝓟 K
have refine : codiscreteWithin K ≤ cofinite ⊓ 𝓟 K
Tactic: refine le_antisymm ?_ hK.cofinite_inf_le_codiscreteWithin
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
inst_1 : T1Space X
hK : IsCompact K
⊢ codiscreteWithin K ≤ cofinite ⊓ 𝓟 K
have grw : codiscreteWithin K ≤ codiscrete X ⊓ 𝓟 K
Tactic: grw [← codiscrete_le_cofinite]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Sort u_3
inst_1 : Finite ι
s : ι → Set X
hs : ∀ (i : ι), IsDiscrete (s i)
hsc : ∀ (i : ι), IsClosed[inst] (s i)
⊢ IsDiscrete.{u_1} (X := X) (⋃ (i : ι), s i)
have suffices : (⋃ (i : ι), s i)ᶜ ∈ codiscrete X
Tactic: suffices (⋃ i, s i)ᶜ ∈ codiscrete X from (compl_mem_codiscrete_iff.mp this).2
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsDiscrete s
ht_1 : IsDiscrete t
hsc : IsClosed[inst] s
ht : IsClosed[inst] t
⊢ IsDiscrete (s ∪ t)
have rw : IsDiscrete.{u_1} (X := X) (⋃ (b : Bool), bif b then s else t)
Tactic: rw [union_eq_iUnion]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
hI : I.Finite
hs : ∀ i ∈ I, IsDiscrete (s i)
hsc : ∀ i ∈ I, IsClosed[inst] (s i)
⊢ IsDiscrete.{u_1} (X := X) (⋃ i ∈ I, s i)
have this : Finite.{u_3 + 1} (↑I : Type u_3)
Tactic: have := hI.to_subtype
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
hI : I.Finite
hs : ∀ i ∈ I, IsDiscrete (s i)
hsc : ∀ i ∈ I, IsClosed[inst] (s i)
this : Finite.{u_3 + 1} (↑I : Type u_3)
⊢ IsDiscrete.{u_1} (X := X) (⋃ i ∈ I, s i)
have simp : ∀ (hs : ∀ (x : { a : ι // a ∈ I }), IsDiscrete (s (↑x : ι)))
  (hsc : ∀ (x : { a : ι // a ∈ I }), IsClosed[inst] (s (↑x : ι))),
  IsDiscrete.{u_1} (X := X) (⋃ (x : (↑I : Type u_3)), s (↑x : ι))
Tactic: simp only [biUnion_eq_iUnion, Subtype.forall'] at *
Cleared hypotheses: hs, hsc
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
hs : DiscreteTopology.{u_1} (↑S : Type u_1)
ht : DiscreteTopology.{u_1} (↑T : Type u_1)
hs' : IsClosed[inst] S
ht' : IsClosed[inst] T
⊢ DiscreteTopology.{u_1} (↑(S ∪ T) : Type u_1)
have rw : ∀ (hs : IsDiscrete S) (ht : IsDiscrete T) (hs' : IsClosed[inst] S) (ht' : IsClosed[inst] T), IsDiscrete (S ∪ T)
Tactic: rw [← isDiscrete_iff_discreteTopology] at *
Cleared hypotheses: hs, ht, hs', ht'
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
I : Finset ι
s : ι → Set X
hs : ∀ i ∈ I, DiscreteTopology.{u_1} (↑(s i) : Type u_1)
hs' : ∀ i ∈ I, IsClosed[inst] (s i)
⊢ DiscreteTopology.{u_1} (↑(⋃ i ∈ I, s i) : Type u_1)
have simp : ∀ (hs : ∀ i ∈ I, IsDiscrete (s i)), IsDiscrete.{u_1} (X := X) (⋃ i ∈ I, s i)
Tactic: simp only [← isDiscrete_iff_discreteTopology] at *
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
inst_1 : Finite ι
s : ι → Set X
hs : ∀ (i : ι), DiscreteTopology.{u_1} (↑(s i) : Type u_1)
hs' : ∀ (i : ι), IsClosed[inst] (s i)
⊢ DiscreteTopology.{u_1} (↑(⋃ (i : ι), s i) : Type u_1)
have simp : ∀ (hs : ∀ (i : ι), IsDiscrete (s i)), IsDiscrete.{u_1} (X := X) (⋃ (i : ι), s i)
Tactic: simp only [← isDiscrete_iff_discreteTopology] at *
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, edist (f i) (f (i + 1))
have base : edist (f m) (f m) ≤ ∑ i ∈ ∅, edist (f i) (f (i + 1))
Tactic: rw [Finset.Ico_self, Finset.sum_empty, edist_self]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
base : edist (f m) (f m) ≤ ∑ i ∈ ∅, edist (f i) (f (i + 1))
⊢ edist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, edist (f i) (f (i + 1))
have base₁ : edist (f m) (f m) ≤ 0
Tactic: rw [Finset.Ico_self, Finset.sum_empty, edist_self]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
base : edist (f m) (f m) ≤ ∑ i ∈ ∅, edist (f i) (f (i + 1))
base₁ : edist (f m) (f m) ≤ 0
⊢ edist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, edist (f i) (f (i + 1))
have base₂ : LE.le (α := ℝ≥0∞) 0 0
Tactic: rw [Finset.Ico_self, Finset.sum_empty, edist_self]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : ℕ → α
m n_1 n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) + edist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), edist (f i) (f (i + 1))
have rw : n ∉ Finset.Ico m n
Tactic: rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : ℕ → α
m n_1 n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ edist (f m) (f (n + 1)) ≤ ∑ i ∈ Finset.Ico m (n + 1), edist (f i) (f (i + 1))
have edist : ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) + edist (f n) (f (n + 1)) =
  ∑ i ∈ Finset.Ico m (n + 1), edist (f i) (f (i + 1))
Tactic: calc
      edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_triangle _ _ _
      _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
      _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
        rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; simp
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
h : m ≤ n
⊢ edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
have base : edist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, edist (f i) (f (i + 1))
Tactic: induction n, h using Nat.le_induction with
  | base => rw [Finset.Ico_self, Finset.sum_empty, edist_self]
  | succ n hle ihn =>
    calc
      edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_triangle _ _ _
      _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
      _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
        rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; simp
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
h : m ≤ n
base : edist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, edist (f i) (f (i + 1))
⊢ edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
have succ : ∀ (n : ℕ) (hle : m ≤ n) (ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))),
  edist (f m) (f (n + 1)) ≤ ∑ i ∈ Finset.Ico m (n + 1), edist (f i) (f (i + 1))
Tactic: induction n, h using Nat.le_induction with
  | base => rw [Finset.Ico_self, Finset.sum_empty, edist_self]
  | succ n hle ihn =>
    calc
      edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_triangle _ _ _
      _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
      _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
        rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; simp
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞),
      0 < i' →
        ∃ (i : ℝ≥0∞), 0 < i ∧ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < i} ⊆ {p : α × α | edist p.1 p.2 < i'}) ↔
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
have simp : (∀ (i' : ℝ≥0∞),
    0 < i' →
      ∃ (i : ℝ≥0∞),
        0 < i ∧
          ∀ (a b : α),
            (a, b) ∈ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < i} →
              Membership.mem (γ := Set (α × α)) {p : α × α | edist p.1 p.2 < i'} (a, b)) ↔
  ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
Tactic: simp only [subset_def, Prod.forall]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
have rw : Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
Tactic: rw [← neBot_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
have refine : ∀ (H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε) (u : Set (α × α))
  (hu : u ∈ 𝓤 α) (x : β) (hx : x ∈ s), ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Tactic: refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
have rcases : ∀ (ε : ℝ≥0∞) (εpos : ε > 0) (hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u),
  ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Tactic: rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
have rcases : ∀ (t : Set β) (ht : t ∈ 𝓝[s] x) (Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε),
  ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Tactic: rcases H ε εpos x hx with ⟨t, ht, Ht⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
have refine : ∀ (H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε) (u : Set (α × α)) (hu : u ∈ 𝓤 α),
  ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
Tactic: refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
have rcases : ∀ (ε : ℝ≥0∞) (εpos : ε > 0) (hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u), ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
Tactic: rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩