awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
⊢ TotallyBounded s
have inl : ∀ (hs : s = ∅), TotallyBounded s
Tactic: rcases s.eq_empty_or_nonempty with hs | hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
inl : ∀ (hs : s = ∅), TotallyBounded s
⊢ TotallyBounded s
have inr : ∀ (hs : s.Nonempty), TotallyBounded s
Tactic: rcases s.eq_empty_or_nonempty with hs | hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
hs : s = ∅
⊢ TotallyBounded s
have inl : TotallyBounded.{u} (α := α) ∅
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
hs : s.Nonempty
⊢ TotallyBounded s
have inr : ∀ (x0 : α) (hx0 : x0 ∈ s), TotallyBounded s
Tactic: rcases hs with ⟨x0, hx0⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
⊢ TotallyBounded s
have inr : ∀ (this : Inhabited (↑s : Type u)), TotallyBounded s
Tactic: haveI : Inhabited s := ⟨⟨x0, hx0⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited (↑s : Type u)
⊢ TotallyBounded s
have inr : ∀ (ε : ℝ) (ε0 : ε > 0), ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
Tactic: refine totallyBounded_iff.2 fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited (↑s : Type u)
ε : ℝ
ε0 : ε > 0
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
have inr : ∀ (β : Type u) (fβ : Fintype β) (F : (↑s : Type u) → β)
  (hF : ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε),
  ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
Tactic: rcases H ε ε0 with ⟨β, fβ, F, hF⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited (↑s : Type u)
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : (↑s : Type u) → β
hF : ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
Finv : β → (↑s : Type u) := Function.invFun F
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
have inr : ∀ (x : α) (xs : x ∈ s),
  Membership.mem (γ := Set α) (⋃ y ∈ range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ Finv), ball y ε) x
Tactic: refine ⟨range (Subtype.val ∘ Finv), finite_range _, fun x xs => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited (↑s : Type u)
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : (↑s : Type u) → β
hF : ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
Finv : β → (↑s : Type u) := Function.invFun F
x : α
xs : x ∈ s
x' : (↑s : Type u) := Finv (F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs))
⊢ Membership.mem (γ := Set α) (⋃ y ∈ range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ Finv), ball y ε) x
have this₁ : F x' = F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs)
Tactic: have : F x' = F ⟨x, xs⟩ := Function.invFun_eq ⟨⟨x, xs⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this_1 : Inhabited (↑s : Type u)
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : (↑s : Type u) → β
hF : ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
Finv : β → (↑s : Type u) := Function.invFun F
x : α
xs : x ∈ s
x' : (↑s : Type u) := Finv (F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs))
this : F x' = F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs)
⊢ Membership.mem (γ := Set α) (⋃ y ∈ range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ Finv), ball y ε) x
have inr : ∃ (i : α) (_ : ∃ (y : β), (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ Finv) y = i), x ∈ ball i ε
Tactic: simp only [Set.mem_iUnion, Set.mem_range]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : TotallyBounded s
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
have rw : ∀ (hs : ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ d}) (ε : ℝ) (ε_pos : ε > 0),
  ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
Tactic: rw [totallyBounded_iff_subset] at hs
Cleared hypotheses: hs, ε, ε_pos
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
⊢ TendstoUniformlyOnFilter F f p p' ↔ ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
have refine : ∀ (H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε) (u : Set (α × α)) (hu : u ∈ 𝓤 α),
  ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
Tactic: refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
have rcases : ∀ (ε : ℝ) (εpos : ε > 0) (hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u),
  ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
Tactic: rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
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, dist (f y) (F n y) < ε
have refine : ∀ (H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (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 _ (dist_mem_uniformity hε), fun H u hu x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (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 : ∀ (ε : ℝ) (εpos : ε > 0) (hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u),
  ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Tactic: rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist 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, dist (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.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
have refine : ∀ (H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (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 _ (dist_mem_uniformity hε), fun H u hu => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
have rcases : ∀ (ε : ℝ) (εpos : ε > 0) (hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u), ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
Tactic: rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε
have rw : (∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), Membership.mem (γ := Set β) univ x → dist (f x) (F n x) < ε) ↔
  ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε
Tactic: rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ Inseparable x y ↔ nndist x y = 0
have rw : edist x y = 0 ↔ nndist x y = 0
Tactic: rw [EMetric.inseparable_iff, edist_nndist, ENNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : edist x y = 0 ↔ nndist x y = 0
⊢ Inseparable x y ↔ nndist x y = 0
have rw₁ : (↑(nndist x y) : ℝ≥0∞) = 0 ↔ nndist x y = 0
Tactic: rw [EMetric.inseparable_iff, edist_nndist, ENNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : edist x y = 0 ↔ nndist x y = 0
rw₁ : (↑(nndist x y) : ℝ≥0∞) = 0 ↔ nndist x y = 0
⊢ Inseparable x y ↔ nndist x y = 0
have rw₂ : nndist x y = 0 ↔ nndist x y = 0
Tactic: rw [EMetric.inseparable_iff, edist_nndist, ENNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ Inseparable x y ↔ dist x y = 0
have rw : nndist x y = 0 ↔ dist x y = 0
Tactic: rw [Metric.inseparable_iff_nndist, dist_nndist, NNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : nndist x y = 0 ↔ dist x y = 0
⊢ Inseparable x y ↔ dist x y = 0
have rw₁ : nndist x y = 0 ↔ (↑(nndist x y) : ℝ) = 0
Tactic: rw [Metric.inseparable_iff_nndist, dist_nndist, NNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : nndist x y = 0 ↔ dist x y = 0
rw₁ : nndist x y = 0 ↔ (↑(nndist x y) : ℝ) = 0
⊢ Inseparable x y ↔ dist x y = 0
have rw₂ : nndist x y = 0 ↔ nndist x y = 0
Tactic: rw [Metric.inseparable_iff_nndist, dist_nndist, NNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
u : β → α
⊢ CauchySeq u ↔ Tendsto (β := ℝ) (fun (n : β × β) ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (x : β × β) ↦ dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
  Tendsto (β := ℝ) (fun (n : β × β) ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)
Tactic: rw [cauchySeq_iff_tendsto, Metric.uniformity_eq_comap_nhds_zero, tendsto_comap_iff,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
u : β → α
⊢ Tendsto (β := ℝ) (fun (x : β × β) ↦ dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (n : β × β) ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)
have simp_rw : Tendsto (β := ℝ) (fun (x : β × β) ↦ dist (u x.1) (Prod.map u u x).2) atTop (𝓝 0) ↔
  Tendsto (β := ℝ) (fun (n : β × β) ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)
Tactic: simp_rw [Prod.map_fst, Prod.map_snd]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (hypothesis)
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this : UniformSpace α := pseudoMetrizableSpaceUniformity α
⊢ IsSeparable (f ⁻¹' s)
have this₁ : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
Tactic: have := pseudoMetrizableSpaceUniformity_countably_generated
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (hypothesis)
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this_1 : UniformSpace α := pseudoMetrizableSpaceUniformity α
this : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
⊢ IsSeparable (f ⁻¹' s)
have this₁ : SeparableSpace.{u_2} (↑s : Type u_2)
Tactic: have : SeparableSpace s := hs.separableSpace
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (hypothesis)
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this_1 : UniformSpace α := pseudoMetrizableSpaceUniformity α
this_2 : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
this : SeparableSpace.{u_2} (↑s : Type u_2)
⊢ IsSeparable (f ⁻¹' s)
have this₁ : SecondCountableTopology.{u_2} (↑s : Type u_2)
Tactic: have : SecondCountableTopology s := UniformSpace.secondCountable_of_separable _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (hypothesis)
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this_1 : UniformSpace α := pseudoMetrizableSpaceUniformity α
this_2 : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
this_3 : SeparableSpace.{u_2} (↑s : Type u_2)
this : SecondCountableTopology.{u_2} (↑s : Type u_2)
⊢ IsSeparable (f ⁻¹' s)
have this₁ : IsInducing (MapsTo.restrict f (f ⁻¹' s) s sorry)
Tactic: have : IsInducing ((mapsTo_preimage f s).restrict _ _ _) :=
    (hf.comp IsInducing.subtypeVal).codRestrict _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (hypothesis)
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this_1 : UniformSpace α := pseudoMetrizableSpaceUniformity α
this_2 : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
this_3 : SeparableSpace.{u_2} (↑s : Type u_2)
this_4 : SecondCountableTopology.{u_2} (↑s : Type u_2)
this : IsInducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)
⊢ IsSeparable (f ⁻¹' s)
have this₁ : SecondCountableTopology.{v} (↑(f ⁻¹' s) : Type v)
Tactic: have := this.secondCountableTopology
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
⊢ SecondCountableTopology α
have refine : ∀ (ε : ℝ≥0∞) (ε0 : ε > 0), ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
Tactic: refine EMetric.secondCountable_of_almost_dense_set fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
have rcases : ∀ (ε' : ℝ≥0) (ε'0 : 0 < (↑ε' : ℝ≥0∞)) (ε'ε : (↑ε' : ℝ≥0∞) < ε),
  ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
Tactic: rcases ENNReal.lt_iff_exists_nnreal_btwn.1 ε0 with ⟨ε', ε'0, ε'ε⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < (↑ε' : ℝ≥0∞)
ε'ε : (↑ε' : ℝ≥0∞) < ε
⊢ ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
have choose : ∀ (s : Set α) (hsc : s.Countable) (y : (x : α) → α) (hys : ∀ (x : α), y x ∈ s)
  (hyx : ∀ (x : α), dist x (y x) ≤ (↑ε' : ℝ)),
  ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
Tactic: choose s hsc y hys hyx using H ε' (mod_cast ε'0)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < (↑ε' : ℝ≥0∞)
ε'ε : (↑ε' : ℝ≥0∞) < ε
s : Set α
hsc : s.Countable
y : (x : α) → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ (↑ε' : ℝ)
⊢ ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
have refine : ∀ (x : α), edist x (y x) ≤ (↑ε' : ℝ≥0∞)
Tactic: refine ⟨s, hsc, iUnion₂_eq_univ_iff.2 fun x => ⟨y x, hys _, le_trans ?_ ε'ε.le⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
X : Type u_2
inst : PseudoMetricSpace X
s : Set X
ε : ℝ
hs : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
hε : 0 < ε
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x ε
have obtain : ∀ (t : Finset (↑s : Type u_2))
  (hst : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ⊆ ⋃ i ∈ t, ball (↑i : X) ε),
  ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x ε
Tactic: obtain ⟨t, hst⟩ := hs.elim_finite_subcover (fun x : s ↦ ball x ε) (fun _ ↦ isOpen_ball) fun x hx ↦
    let ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ hε; mem_iUnion.2 ⟨⟨y, hy⟩, hxy⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
X : Type u_2
inst : PseudoMetricSpace X
s : Set X
ε : ℝ
hs : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
hε : 0 < ε
t : Finset (↑s : Type u_2)
hst : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ⊆ ⋃ i ∈ t, ball (↑i : X) ε
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x ε
have refine : s ⊆
  ⋃
    x ∈
      (↑(Finset.map { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), inj' := sorry : { x : X // x ∈ s } ↪ X } t) : Set X),
    ball x ε
Tactic: refine ⟨t.map ⟨Subtype.val, Subtype.val_injective⟩, by simp, Finset.finite_toSet _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable (f '' s)
have rw : IsSeparable.{v} (α := β) ((fun (x : (↑s : Type u_2)) ↦ f (↑x : α)) '' univ)
Tactic: rw [image_eq_range, ← image_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ
⊢ val (p := fun (a : α) ↦ p a) '' ball a r = ball (↑a : α) r ∩ {a : α | p a}
have rw : image (α := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) (val (p := fun (a : α) ↦ p a) ⁻¹' ball (↑a : α) r) =
  ball (↑a : α) r ∩ {a : α | p a}
Tactic: rw [← preimage_ball, image_preimage_eq_inter_range, range_val_subtype]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ
rw :
  image (α := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) (val (p := fun (a : α) ↦ p a) ⁻¹' ball (↑a : α) r) =
    ball (↑a : α) r ∩ {a : α | p a}
⊢ val (p := fun (a : α) ↦ p a) '' ball a r = ball (↑a : α) r ∩ {a : α | p a}
have rw₁ : ball (↑a : α) r ∩ range (ι := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) = ball (↑a : α) r ∩ {a : α | p a}
Tactic: rw [← preimage_ball, image_preimage_eq_inter_range, range_val_subtype]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ
rw :
  image (α := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) (val (p := fun (a : α) ↦ p a) ⁻¹' ball (↑a : α) r) =
    ball (↑a : α) r ∩ {a : α | p a}
rw₁ : ball (↑a : α) r ∩ range (ι := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) = ball (↑a : α) r ∩ {a : α | p a}
⊢ val (p := fun (a : α) ↦ p a) '' ball a r = ball (↑a : α) r ∩ {a : α | p a}
have rw₂ : ball (↑a : α) r ∩ {x : α | p x} = ball (↑a : α) r ∩ {a : α | p a}
Tactic: rw [← preimage_ball, image_preimage_eq_inter_range, range_val_subtype]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ
⊢ val (p := fun (a : α) ↦ p a) '' closedBall a r = closedBall (↑a : α) r ∩ {a : α | p a}
have rw : image (α := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) (val (p := fun (a : α) ↦ p a) ⁻¹' closedBall (↑a : α) r) =
  closedBall (↑a : α) r ∩ {a : α | p a}
Tactic: rw [← preimage_closedBall, image_preimage_eq_inter_range, range_val_subtype]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ
rw :
  image (α := { a : α // p a }) (val (p := fun (a : α) ↦ p a))
      (val (p := fun (a : α) ↦ p a) ⁻¹' closedBall (↑a : α) r) =
    closedBall (↑a : α) r ∩ {a : α | p a}
⊢ val (p := fun (a : α) ↦ p a) '' closedBall a r = closedBall (↑a : α) r ∩ {a : α | p a}
have rw₁ : closedBall (↑a : α) r ∩ range (ι := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) =
  closedBall (↑a : α) r ∩ {a : α | p a}
Tactic: rw [← preimage_closedBall, image_preimage_eq_inter_range, range_val_subtype]