awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
h : t.Finite
⊢ ∅ᶜ ∈ codiscreteWithin s

Tactic:
simp
-- Module: Mathlib.Topology.DiscreteSubset
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)ᶜ = {τ}ᶜ ∩ tᶜ

Tactic:
aesop
-- Module: Mathlib.Topology.DiscreteSubset
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)ᶜ = {τ}ᶜ ∩ tᶜ

Tactic:
have : (insert τ t)ᶜ = {τ}ᶜ ∩ tᶜ := by aesop
-- Module: Mathlib.Topology.DiscreteSubset
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
this : (insert τ t)ᶜ = {τ}ᶜ ∩ tᶜ
⊢ (insert τ t)ᶜ ∈ codiscreteWithin s

Tactic:
simp_all
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
⊢ S ∈ codiscrete X ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)

Tactic:
simp [codiscrete, mem_codiscreteWithin, compl_eq_univ_diff]

Premises used: mem_codiscreteWithin, Set.compl_eq_univ_diff, Filter.codiscrete
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
⊢ S ∈ codiscrete X ↔ ∀ (x : X), ¬AccPt x (𝓟 Sᶜ)

Tactic:
simp only [mem_codiscrete, disjoint_iff, AccPt, not_neBot]

Premises used: mem_codiscrete, disjoint_iff, AccPt, Filter.not_neBot
-- Module: Mathlib.Topology.DiscreteSubset
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ᶜ
rw₂ rw₃ : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)
⊢ S ∈ codiscrete X ↔ IsOpen[inst] S ∧ IsDiscrete Sᶜ

Tactic:
rw [mem_codiscrete, ← isClosed_compl_iff, isClosed_and_discrete_iff]

Premises used: mem_codiscrete, isClosed_and_discrete_iff, isClosed_compl_iff
-- Module: Mathlib.Topology.DiscreteSubset
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
rw₂ rw₃ : (∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)
⊢ Sᶜ ∈ codiscrete X ↔ IsClosed[inst] S ∧ IsDiscrete S

Tactic:
rw [mem_codiscrete, compl_compl, isClosed_and_discrete_iff]

Premises used: compl_compl, mem_codiscrete, isClosed_and_discrete_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ codiscreteWithin s ≤ codiscrete X ⊓ 𝓟 s

Tactic:
simp [codiscrete, codiscreteWithin_mono]

Premises used: Filter.codiscreteWithin_mono, Filter.codiscrete
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
s t : Set X
⊢ f '' s ∈ codiscreteWithin (f '' t) ↔ s ∈ codiscreteWithin t

Tactic:
simp only [mem_codiscreteWithin_accPt, forall_mem_image, accPt_principal_iff_clusterPt,
    ← hf.mapClusterPt_iff, MapClusterPt, map_principal, image_diff hf.injective, image_singleton]

Premises used: Set.image_singleton, Set.image_diff, mem_codiscreteWithin_accPt, Topology.IsEmbedding.injective, MapClusterPt, Filter.map_principal, Topology.IsEmbedding.toIsInducing, accPt_principal_iff_clusterPt, Topology.IsInducing.mapClusterPt_iff, Set.forall_mem_image
-- Module: Mathlib.Topology.DiscreteSubset
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
rw₂ rw₃ :
  Membership.mem (γ := Filter X) (codiscreteWithin univ) s ↔ Membership.mem (γ := Filter X) (codiscreteWithin univ) s
⊢ f '' s ∈ codiscreteWithin (range f) ↔ s ∈ codiscrete X

Tactic:
rw [← image_univ, hf.image_mem_codiscreteWithin, codiscrete]

Premises used: Set.image_univ, Topology.IsEmbedding.image_mem_codiscreteWithin, Filter.codiscrete
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
U : Set (↑S : Type u_1)
⊢ Membership.mem (γ := Filter (↑S : Type u_1)) (codiscrete (↑S : Type u_1)) U ↔
    Subtype.val (p := fun (x : X) ↦ x ∈ S) '' U ∈ codiscreteWithin S

Tactic:
simp [← Topology.IsEmbedding.subtypeVal.image_mem_codiscreteWithin_range]

Premises used: Topology.IsEmbedding.image_mem_codiscreteWithin_range, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
⊢ codiscreteWithin S = ⊥ ↔ IsDiscrete S

Tactic:
simp [isDiscrete_iff_nhdsNE, codiscreteWithin, ← nhdsWithin_inter', Set.diff_eq, inter_comm]

Premises used: Set.diff_eq, Set.inter_comm, isDiscrete_iff_nhdsNE, Filter.codiscreteWithin, nhdsWithin_inter'
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : Membership.mem (γ := Filter X) cofinite s
rw : IsClosed[inst] sᶜ ∧ IsDiscrete sᶜ
⊢ s ∈ codiscrete X

Tactic:
rw [← compl_compl s, compl_mem_codiscrete_iff]

Premises used: compl_compl, compl_mem_codiscrete_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : Membership.mem (γ := Filter X) cofinite s
⊢ IsClosed[inst] sᶜ ∧ IsDiscrete sᶜ

Tactic:
⟨hs.isClosed, hs.isDiscrete⟩

Premises used: Set.Finite.isDiscrete, And.intro, Set.Finite.isClosed
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : Membership.mem (γ := Filter X) cofinite s
⊢ IsClosed[inst] sᶜ ∧ IsDiscrete sᶜ

Tactic:
exact ⟨hs.isClosed, hs.isDiscrete⟩
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
S : Set X
hs : S.Finite
⊢ Membership.mem (γ := Filter X) cofinite Sᶜ

Tactic:
simpa
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
S : Set X
x : X
h : AccPt x (𝓟 S)
hs : S.Finite
⊢ Sᶜ ∈ codiscrete X

Tactic:
have := hs.compl_mem_codiscrete
-- Module: Mathlib.Topology.DiscreteSubset
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
⊢ ∀ (x : X), ¬AccPt x (𝓟 S)

Tactic:
rw [mem_codiscrete_accPt, compl_compl] at this

Premises used: compl_compl, mem_codiscrete_accPt
-- Module: Mathlib.Topology.DiscreteSubset
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 : ∀ (x : X), ¬AccPt x (𝓟 S)
⊢ False

Tactic:
this _ h
-- Module: Mathlib.Topology.DiscreteSubset
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 : ∀ (x : X), ¬AccPt x (𝓟 S)
⊢ False

Tactic:
exact this _ h
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s K : Set X
hK : IsCompact K
hs : s ∈ codiscreteWithin K
⊢ ∀ x ∈ K, ¬AccPt x (𝓟 (K \ s))

Tactic:
rw [mem_codiscreteWithin_accPt] at hs

Premises used: mem_codiscreteWithin_accPt
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s K : Set X
hK : IsCompact K
hs : ∀ x ∈ K, ¬AccPt x (𝓟 (K \ s))
contrapose! : ∀ (hs : (K \ s).Infinite), ∃ x ∈ K, AccPt x (𝓟 (K \ s))
⊢ (K \ s).Finite

Tactic:
contrapose! hs
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s K : Set X
hK : IsCompact K
hs : (K \ s).Infinite
⊢ ∃ x ∈ K, AccPt x (𝓟 (K \ s))

Tactic:
Set.Infinite.exists_accPt_of_subset_isCompact hs hK (sep_subset _ _)

Premises used: Set.Infinite.exists_accPt_of_subset_isCompact, Set.sep_subset
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s K : Set X
hK : IsCompact K
hs : (K \ s).Infinite
⊢ ∃ x ∈ K, AccPt x (𝓟 (K \ s))

Tactic:
exact Set.Infinite.exists_accPt_of_subset_isCompact hs hK (sep_subset _ _)

Premises used: Set.Infinite.exists_accPt_of_subset_isCompact, Set.sep_subset
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
s : Set X
hs : s ∈ codiscreteWithin K
⊢ s ∈ cofinite ⊓ 𝓟 K

Tactic:
simpa [mem_inf_principal, compl_setOf] using hK.finite_diff_of_mem_codiscreteWithin hs

Premises used: Filter.mem_inf_principal, IsCompact.finite_diff_of_mem_codiscreteWithin, Set.compl_setOf
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
inst_1 : T1Space X
hK : IsCompact K
⊢ codiscreteWithin K = cofinite ⊓ 𝓟 K

Tactic:
le_antisymm ?_ hK.cofinite_inf_le_codiscreteWithin

Premises used: IsCompact.cofinite_inf_le_codiscreteWithin, le_antisymm
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
inst_1 : T1Space X
hK : IsCompact K
refine : codiscreteWithin K ≤ cofinite ⊓ 𝓟 K
⊢ codiscreteWithin K = cofinite ⊓ 𝓟 K

Tactic:
refine le_antisymm ?_ hK.cofinite_inf_le_codiscreteWithin

Premises used: IsCompact.cofinite_inf_le_codiscreteWithin, le_antisymm
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
inst_1 : T1Space X
hK : IsCompact K
grw : codiscreteWithin K ≤ codiscrete X ⊓ 𝓟 K
⊢ codiscreteWithin K ≤ cofinite ⊓ 𝓟 K

Tactic:
grw [← codiscrete_le_cofinite]

Premises used: codiscrete_le_cofinite
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
inst_1 : T1Space X
hK : IsCompact K
⊢ codiscreteWithin K ≤ codiscrete X ⊓ 𝓟 K

Tactic:
codiscreteWithin_le_codiscrete_inf_principal K

Premises used: codiscreteWithin_le_codiscrete_inf_principal
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
inst_1 : T1Space X
hK : IsCompact K
⊢ codiscreteWithin K ≤ codiscrete X ⊓ 𝓟 K

Tactic:
exact codiscreteWithin_le_codiscrete_inf_principal K

Premises used: codiscreteWithin_le_codiscrete_inf_principal
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
⊢ cofinite ≤ codiscrete X

Tactic:
simpa using isCompact_univ.cofinite_inf_le_codiscreteWithin

Premises used: IsCompact.cofinite_inf_le_codiscreteWithin, isCompact_univ
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : CompactSpace X
⊢ codiscrete X = cofinite

Tactic:
simpa using isCompact_univ.codiscreteWithin_eq

Premises used: IsCompact.codiscreteWithin_eq, isCompact_univ
-- Module: Mathlib.Topology.DiscreteSubset
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)
suffices : (⋃ (i : ι), s i)ᶜ ∈ codiscrete X
⊢ IsDiscrete.{u_1} (X := X) (⋃ (i : ι), s i)

Tactic:
suffices (⋃ i, s i)ᶜ ∈ codiscrete X from (compl_mem_codiscrete_iff.mp this).2
-- Module: Mathlib.Topology.DiscreteSubset
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)
⊢ (⋃ (i : ι), s i)ᶜ ∈ codiscrete X

Tactic:
simp [compl_mem_codiscrete_iff, *]

Premises used: compl_mem_codiscrete_iff
-- Module: Mathlib.Topology.DiscreteSubset
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
rw : IsDiscrete.{u_1} (X := X) (⋃ (b : Bool), bif b then s else t)
⊢ IsDiscrete (s ∪ t)

Tactic:
rw [union_eq_iUnion]

Premises used: Set.union_eq_iUnion
-- Module: Mathlib.Topology.DiscreteSubset
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
⊢ ∀ (i : Bool), IsDiscrete (bif i then s else t)

Tactic:
simp [*]
-- Module: Mathlib.Topology.DiscreteSubset
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
⊢ ∀ (i : Bool), IsClosed[inst] (bif i then s else t)

Tactic:
simp [*]
-- Module: Mathlib.Topology.DiscreteSubset
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.{u_1} (X := X) (⋃ (b : Bool), bif b then s else t)

Tactic:
exact .iUnion (by simp [*]) (by simp [*])
-- Module: Mathlib.Topology.DiscreteSubset
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)
⊢ Finite.{u_3 + 1} (↑I : Type u_3)

Tactic:
have := hI.to_subtype
-- Module: Mathlib.Topology.DiscreteSubset
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)
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 : ι))
⊢ IsDiscrete.{u_1} (X := X) (⋃ i ∈ I, s i)

Tactic:
simp only [biUnion_eq_iUnion, Subtype.forall'] at *

Premises used: Set.biUnion_eq_iUnion, Subtype.forall'
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
hI : I.Finite
this : Finite.{u_3 + 1} (↑I : Type u_3)
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:
.iUnion hs hsc

Premises used: IsDiscrete.iUnion
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
hI : I.Finite
this : Finite.{u_3 + 1} (↑I : Type u_3)
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:
exact .iUnion hs hsc
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
I : Finset ι
s : ι → Set X
hs : ∀ i ∈ I, IsDiscrete (s i)
hsc : ∀ i ∈ I, IsClosed[inst] (s i)
⊢ IsDiscrete.{u_1} (X := X) (⋃ i ∈ I, s i)

Tactic:
.biUnion I.finite_toSet hs hsc

Premises used: Finset.finite_toSet, IsDiscrete.biUnion
-- Module: Mathlib.Topology.DiscreteSubset
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
rw : ∀ (hs : IsDiscrete S) (ht : IsDiscrete T) (hs' : IsClosed[inst] S) (ht' : IsClosed[inst] T), IsDiscrete (S ∪ T)
⊢ DiscreteTopology.{u_1} (↑(S ∪ T) : Type u_1)

Tactic:
rw [← isDiscrete_iff_discreteTopology] at *

Premises used: isDiscrete_iff_discreteTopology
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
hs : IsDiscrete S
ht : IsDiscrete T
hs' : IsClosed[inst] S
ht' : IsClosed[inst] T
⊢ IsDiscrete (S ∪ T)

Tactic:
hs.union ht hs' ht'

Premises used: IsDiscrete.union
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
hs : IsDiscrete S
ht : IsDiscrete T
hs' : IsClosed[inst] S
ht' : IsClosed[inst] T
⊢ IsDiscrete (S ∪ T)

Tactic:
exact hs.union ht hs' ht'

Premises used: IsDiscrete.union
-- Module: Mathlib.Topology.DiscreteSubset
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)
simp : ∀ (hs : ∀ i ∈ I, IsDiscrete (s i)), IsDiscrete.{u_1} (X := X) (⋃ i ∈ I, s i)
⊢ DiscreteTopology.{u_1} (↑(⋃ i ∈ I, s i) : Type u_1)

Tactic:
simp only [← isDiscrete_iff_discreteTopology] at *

Premises used: isDiscrete_iff_discreteTopology
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
I : Finset ι
s : ι → Set X
hs' : ∀ i ∈ I, IsClosed[inst] (s i)
hs : ∀ i ∈ I, IsDiscrete (s i)
⊢ IsDiscrete.{u_1} (X := X) (⋃ i ∈ I, s i)

Tactic:
.biUnion_finset hs hs'

Premises used: IsDiscrete.biUnion_finset
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
I : Finset ι
s : ι → Set X
hs' : ∀ i ∈ I, IsClosed[inst] (s i)
hs : ∀ i ∈ I, IsDiscrete (s i)
⊢ IsDiscrete.{u_1} (X := X) (⋃ i ∈ I, s i)

Tactic:
exact .biUnion_finset hs hs'
-- Module: Mathlib.Topology.DiscreteSubset
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)
simp : ∀ (hs : ∀ (i : ι), IsDiscrete (s i)), IsDiscrete.{u_1} (X := X) (⋃ (i : ι), s i)
⊢ DiscreteTopology.{u_1} (↑(⋃ (i : ι), s i) : Type u_1)

Tactic:
simp only [← isDiscrete_iff_discreteTopology] at *

Premises used: isDiscrete_iff_discreteTopology
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
inst_1 : Finite ι
s : ι → Set X
hs' : ∀ (i : ι), IsClosed[inst] (s i)
hs : ∀ (i : ι), IsDiscrete (s i)
⊢ IsDiscrete.{u_1} (X := X) (⋃ (i : ι), s i)

Tactic:
.iUnion hs hs'

Premises used: IsDiscrete.iUnion
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
inst_1 : Finite ι
s : ι → Set X
hs' : ∀ (i : ι), IsClosed[inst] (s i)
hs : ∀ (i : ι), IsDiscrete (s i)
⊢ IsDiscrete.{u_1} (X := X) (⋃ (i : ι), s i)

Tactic:
exact .iUnion hs hs'
-- Module: Mathlib.Topology.EMetricSpace.Basic
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
base₂ base₃ : LE.le (α := ℝ≥0∞) 0 0
⊢ edist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, edist (f i) (f (i + 1))

Tactic:
rw [Finset.Ico_self, Finset.sum_empty, edist_self]

Premises used: Finset.Ico_self, PseudoEMetricSpace.edist_self, Finset.sum_empty
-- Module: Mathlib.Topology.EMetricSpace.Basic
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)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1))

Tactic:
edist_triangle _ _ _

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.Basic
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) + edist (f n) (f (n + 1)) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) + edist (f n) (f (n + 1))

Tactic:
add_le_add ihn le_rfl

Premises used: le_rfl, add_le_add
-- Module: Mathlib.Topology.EMetricSpace.Basic
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))
rw : n ∉ Finset.Ico m n
⊢ ∑ 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:
rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]

Premises used: add_comm, Finset.insert_Ico_right_eq_Ico_add_one, Finset.sum_insert
-- Module: Mathlib.Topology.EMetricSpace.Basic
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))
⊢ n ∉ Finset.Ico m n

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : ℕ → α
m n_1 n : ℕ
hle : m ≤ n
ihn : EDist.edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, EDist.edist (f i) (f (i + 1))
edist :
  ∑ i ∈ Finset.Ico m n, EDist.edist (f i) (f (i + 1)) + EDist.edist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), EDist.edist (f i) (f (i + 1))
⊢ EDist.edist (f m) (f (n + 1)) ≤ ∑ i ∈ Finset.Ico m (n + 1), EDist.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

Premises used: le_rfl, add_le_add, Finset.Ico, HAdd.hAdd, EDist.edist, OfNat.ofNat, Finset.sum, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.Basic
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))
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))
⊢ edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, 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

Premises used: Finset.Ico_self, Finset.Ico, PseudoEMetricSpace.edist_self, HAdd.hAdd, Finset.sum_empty, EDist.edist, OfNat.ofNat, Finset.sum, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : ℕ → α
n : ℕ
⊢ edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, edist (f i) (f (i + 1))

Tactic:
Nat.Ico_zero_eq_range n ▸ edist_le_Ico_sum_edist f (Nat.zero_le n)

Premises used: Nat.zero_le, Eq.rec, Nat.Ico_zero_eq_range, edist_le_Ico_sum_edist
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
hmn : m ≤ n
d : ℕ → ℝ≥0∞
hd : ∀ {k : ℕ}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k
⊢ edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i

Tactic:
le_trans (edist_le_Ico_sum_edist f hmn) <|
    Finset.sum_le_sum fun _k hk => hd (Finset.mem_Ico.1 hk).1 (Finset.mem_Ico.1 hk).2

Premises used: And.right, And.left, Iff.mp, Finset.sum_le_sum, edist_le_Ico_sum_edist, Finset.mem_Ico, le_trans
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : ℕ → α
n : ℕ
d : ℕ → ℝ≥0∞
hd : ∀ {k : ℕ}, k < n → edist (f k) (f (k + 1)) ≤ d k
⊢ edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i

Tactic:
Nat.Ico_zero_eq_range n ▸ edist_le_Ico_sum_of_edist_le zero_le fun _ => hd

Premises used: zero_le, edist_le_Ico_sum_of_edist_le, Eq.rec, Nat.Ico_zero_eq_range
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
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 < δ
⊢ (∀ (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 < δ

Tactic:
simp only [subset_def, Prod.forall]

Premises used: Set.subset_def, Prod.forall
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
⊢ (∀ (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:
rfl