awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
⊢ ¬Bornology.IsBounded (image2 f s t)
have this : ¬Bornology.IsBounded (image2 f s {b})
Tactic: have : ¬IsBounded (Set.image2 f s {b}) := by
    intro h
    apply hst.1
    rw [Set.image2_singleton_right] at h
    replace h := (hf b).isBounded_preimage h
    exact h.subset (subset_preimage_image _ _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
β : Type v
γ : Type w
inst : MetricSpace γ
inst_1 : PseudoMetricSpace β
f : γ → β
⊢ IsUniformEmbedding f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
have rw : IsUniformInducing f ↔
  (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
Tactic: rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
β : Type v
γ : Type w
inst : MetricSpace γ
inst_1 : PseudoMetricSpace β
f : γ → β
rw :
  IsUniformInducing f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
⊢ IsUniformEmbedding f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
have rw₁ : (UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ) ↔
  (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
Tactic: rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
β : Type v
γ : Type w
inst : MetricSpace γ
inst_1 : PseudoMetricSpace β
f : γ → β
rw :
  IsUniformInducing f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
rw₁ :
  (UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ) ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
⊢ IsUniformEmbedding f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
have rw₂ : ((∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : γ⦄, dist a b < δ → dist (f a) (f b) < ε) ∧
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ) ↔
  (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
Tactic: rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
⊢ SecondCountableTopology α
have refine : ∀ (ε : ℝ) (ε0 : ε > 0), ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
Tactic: refine secondCountable_of_almost_dense_set fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
⊢ ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
have rcases : ∀ (β : Type u_2) (fβ : Encodable β) (F : α → β) (hF : ∀ (x y : α), F x = F y → dist x y ≤ ε),
  ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
Tactic: rcases H ε ε0 with ⟨β, fβ, F, hF⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : (↑(range F) : Type u_2) → α := rangeSplitting F
⊢ ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
have refine : ∀ (x : α), ∃ y ∈ range Finv, dist x y ≤ ε
Tactic: refine ⟨range Finv, ⟨countable_range _, fun x => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : (↑(range F) : Type u_2) → α := rangeSplitting F
x : α
x' : α := Finv (Subtype.mk (p := fun (x : β) ↦ x ∈ range F) (F x) ⋯)
⊢ ∃ y ∈ range Finv, dist x y ≤ ε
have this : F x' = F x
Tactic: have : F x' = F x := apply_rangeSplitting F _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst : PseudoMetricSpace α_1
γ : Type w
inst_1 : MetricSpace γ
α : Type u
inst_2 : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
⊢ dist x y = dist x' y'
have rw : (edist x y).toReal = dist x' y'
Tactic: rw [dist_edist, dist_edist, ← edist_mk x,
    ← edist_mk x', mk_eq_mk.2 hx, mk_eq_mk.2 hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst : PseudoMetricSpace α_1
γ : Type w
inst_1 : MetricSpace γ
α : Type u
inst_2 : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
rw : (edist x y).toReal = dist x' y'
⊢ dist x y = dist x' y'
have rw₁ : (edist x y).toReal = (edist x' y').toReal
Tactic: rw [dist_edist, dist_edist, ← edist_mk x,
    ← edist_mk x', mk_eq_mk.2 hx, mk_eq_mk.2 hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst : PseudoMetricSpace α_1
γ : Type w
inst_1 : MetricSpace γ
α : Type u
inst_2 : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
rw : (edist x y).toReal = dist x' y'
rw₁ : (edist x y).toReal = (edist x' y').toReal
⊢ dist x y = dist x' y'
have rw₂ : (edist (α := SeparationQuotient α) (mk x) (mk y)).toReal = (edist x' y').toReal
Tactic: rw [dist_edist, dist_edist, ← edist_mk x,
    ← edist_mk x', mk_eq_mk.2 hx, mk_eq_mk.2 hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst : PseudoMetricSpace α_1
γ : Type w
inst_1 : MetricSpace γ
α : Type u
inst_2 : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
rw : (edist x y).toReal = dist x' y'
rw₁ : (edist x y).toReal = (edist x' y').toReal
rw₂ : (edist (α := SeparationQuotient α) (mk x) (mk y)).toReal = (edist x' y').toReal
⊢ dist x y = dist x' y'
have rw₃ : (edist (α := SeparationQuotient α) (mk x) (mk y)).toReal = (edist (α := SeparationQuotient α) (mk x') (mk y')).toReal
Tactic: rw [dist_edist, dist_edist, ← edist_mk x,
    ← edist_mk x', mk_eq_mk.2 hx, mk_eq_mk.2 hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst : PseudoMetricSpace α_1
γ : Type w
inst_1 : MetricSpace γ
α : Type u
inst_2 : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
rw : (edist x y).toReal = dist x' y'
rw₁ : (edist x y).toReal = (edist x' y').toReal
rw₂ : (edist (α := SeparationQuotient α) (mk x) (mk y)).toReal = (edist x' y').toReal
rw₃ :
  (edist (α := SeparationQuotient α) (mk x) (mk y)).toReal = (edist (α := SeparationQuotient α) (mk x') (mk y')).toReal
⊢ dist x y = dist x' y'
have rw₄ : (edist (α := SeparationQuotient α) (mk x') (mk y)).toReal = (edist (α := SeparationQuotient α) (mk x') (mk y')).toReal
Tactic: rw [dist_edist, dist_edist, ← edist_mk x,
    ← edist_mk x', mk_eq_mk.2 hx, mk_eq_mk.2 hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst : PseudoMetricSpace α_1
γ : Type w
inst_1 : MetricSpace γ
α : Type u
inst_2 : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
rw : (edist x y).toReal = dist x' y'
rw₁ : (edist x y).toReal = (edist x' y').toReal
rw₂ : (edist (α := SeparationQuotient α) (mk x) (mk y)).toReal = (edist x' y').toReal
rw₃ :
  (edist (α := SeparationQuotient α) (mk x) (mk y)).toReal = (edist (α := SeparationQuotient α) (mk x') (mk y')).toReal
rw₄ :
  (edist (α := SeparationQuotient α) (mk x') (mk y)).toReal = (edist (α := SeparationQuotient α) (mk x') (mk y')).toReal
⊢ dist x y = dist x' y'
have rw₅ : (edist (α := SeparationQuotient α) (mk x') (mk y')).toReal = (edist (α := SeparationQuotient α) (mk x') (mk y')).toReal
Tactic: rw [dist_edist, dist_edist, ← edist_mk x,
    ← edist_mk x', mk_eq_mk.2 hx, mk_eq_mk.2 hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ m.replaceEDist d hd = m
have h : Eq.{u_2 + 1} (α := X → X → ℝ≥0∞) edist edist
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ m.replaceDist d hd = m
have h : Eq.{u_2 + 1} (α := X → X → ℝ) dist dist
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ m.replaceEDist d hd = m
have h : Eq.{u_2 + 1} (α := X → X → ℝ≥0∞) edist edist
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Basic (goal)
Goal:
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ m.replaceDist d hd = m
have h : Eq.{u_2 + 1} (α := X → X → ℝ) dist dist
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ∃ (f : ℕ → Set α),
    Monotone f ∧
      ⋃ (i : ℕ), f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
have inl : ∀ (hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅),
  ∃ (f : ℕ → Set α),
    Monotone f ∧
      Eq.{u + 1} (α := Set α) (⋃ (i : ℕ), f i) ∅ ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
Tactic: obtain rfl | ⟨x, -⟩ := U.eq_empty_or_nonempty
Cleared hypotheses: U, hU
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
inl :
  ∀ (hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅),
    ∃ (f : ℕ → Set α),
      Monotone f ∧
        Eq.{u + 1} (α := Set α) (⋃ (i : ℕ), f i) ∅ ∧
          ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ ∃ (f : ℕ → Set α),
    Monotone f ∧
      ⋃ (i : ℕ), f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
have inr : ∀ (x : α),
  ∃ (f : ℕ → Set α),
    Monotone f ∧
      ⋃ (i : ℕ), f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
Tactic: obtain rfl | ⟨x, -⟩ := U.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
⊢ ∃ (f : ℕ → Set α),
    Monotone f ∧
      ⋃ (i : ℕ), f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
have inr : ∀ (i j : ℕ) (hij : i ≤ j),
  LE.le.{u} (α := Set α) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) j)
Tactic: refine ⟨fun i ↦ U ∩ ball x i, fun i j hij ↦ ?_, ?_, fun i ↦ ⟨?_, hU.inter isOpen_ball⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
inr :
  ∀ (i j : ℕ) (hij : i ≤ j),
    LE.le.{u} (α := Set α) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) j)
⊢ ∃ (f : ℕ → Set α),
    Monotone f ∧
      ⋃ (i : ℕ), f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
have inr₁ : ⋃ (i : ℕ), (fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i = U
Tactic: refine ⟨fun i ↦ U ∩ ball x i, fun i j hij ↦ ?_, ?_, fun i ↦ ⟨?_, hU.inter isOpen_ball⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
inr :
  ∀ (i j : ℕ) (hij : i ≤ j),
    LE.le.{u} (α := Set α) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) j)
inr₁ : ⋃ (i : ℕ), (fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i = U
⊢ ∃ (f : ℕ → Set α),
    Monotone f ∧
      ⋃ (i : ℕ), f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
have inr₂ : ∀ (i : ℕ), Bornology.IsBounded.{u} (α := α) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i)
Tactic: refine ⟨fun i ↦ U ∩ ball x i, fun i j hij ↦ ?_, ?_, fun i ↦ ⟨?_, hU.inter isOpen_ball⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis
    (fun (a : Set α) ↦ x ∈ a ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧ Bornology.IsBounded a) id
have simp_rw : (𝓝 x).HasBasis
  (fun (a : Set α) ↦ (x ∈ a ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a) ∧ Bornology.IsBounded a) id
Tactic: simp_rw [← and_assoc]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis
    (fun (a : Set α) ↦ (x ∈ a ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a) ∧ Bornology.IsBounded a)
    id
have apply : ∀ (s : Set α) (hs : x ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
  ∃ (j : Set α), (x ∈ j ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] j) ∧ Bornology.IsBounded j ∧ j ⊆ s
Tactic: apply (nhds_basis_opens x).restrict fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
⊢ Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto f l (cobounded α)
have rw : Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto f l (comap (β := ℝ) (fun (x : α) ↦ dist x c) atTop)
Tactic: rw [← comap_dist_right_atTop c, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
rw : Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto f l (comap (β := ℝ) (fun (x : α) ↦ dist x c) atTop)
⊢ Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto f l (cobounded α)
have rw₁ : Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto (β := ℝ) ((fun (x : α) ↦ dist x c) ∘ f) l atTop
Tactic: rw [← comap_dist_right_atTop c, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
rw : Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto f l (comap (β := ℝ) (fun (x : α) ↦ dist x c) atTop)
rw₁ : Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto (β := ℝ) ((fun (x : α) ↦ dist x c) ∘ f) l atTop
⊢ Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto f l (cobounded α)
have rw₂ : Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop
Tactic: rw [← comap_dist_right_atTop c, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
c : α
⊢ Bornology.IsCobounded s ↔ ∃ (r : ℝ), (closedBall c r)ᶜ ⊆ s
have rw : (∃ (r : ℝ), sᶜ ⊆ closedBall c r) ↔ ∃ (r : ℝ), (closedBall c r)ᶜ ⊆ s
Tactic: rw [← isBounded_compl_iff, isBounded_iff_subset_closedBall c]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
c : α
⊢ (∃ (r : ℝ), sᶜ ⊆ closedBall c r) ↔ ∃ (r : ℝ), (closedBall c r)ᶜ ⊆ s
have h : ∀ (a : ℝ), sᶜ ⊆ closedBall c a ↔ (closedBall c a)ᶜ ⊆ s
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
c : α
r : ℝ
⊢ sᶜ ⊆ closedBall c r ↔ (closedBall c r)ᶜ ⊆ s
have h : (closedBall c r)ᶜ ⊆ s ↔ (closedBall c r)ᶜ ⊆ s
Tactic: rw [compl_subset_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
c : α
h : ∃ (r : ℝ), (closedBall c r)ᶜ ⊆ s
⊢ s ∈ cocompact α
have rcases : ∀ (r : ℝ) (h : (closedBall c r)ᶜ ⊆ s), s ∈ cocompact α
Tactic: rcases h with ⟨r, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
c : α
r : ℝ
h : (closedBall c r)ᶜ ⊆ s
⊢ s ∈ cocompact α
have rw : ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
Tactic: rw [Filter.mem_cocompact]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (SProd.sprod (α := Filter β) (β := Filter β) Filter.cofinite Filter.cofinite) (𝓤 α)
⊢ Bornology.IsBounded (range f)
have rcases : ∀ (s : Set β) (hsf : s.Finite)
  (hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Membership.mem (γ := Set (α × α)) {p : α × α | dist p.1 p.2 < 1} (Prod.map f f x)),
  Bornology.IsBounded (range f)
Tactic: rcases (hasBasis_cofinite.prod_self.tendsto_iff uniformity_basis_dist).1 hf 1 zero_lt_one with
    ⟨s, hsf, hs1⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (SProd.sprod (α := Filter β) (β := Filter β) Filter.cofinite Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Membership.mem (γ := Set (α × α)) {p : α × α | dist p.1 p.2 < 1} (Prod.map f f x)
⊢ Bornology.IsBounded (range f)
have rw : Bornology.IsBounded (f '' s ∪ f '' sᶜ)
Tactic: rw [← image_union_image_compl_eq_range]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
hf : CauchySeq f
⊢ Cauchy (map f Filter.cofinite)
have rwa : Cauchy (map f atTop)
Tactic: rwa [Nat.cofinite_eq_atTop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
have rw : ∀ x ∈ k, Disjoint (𝓝 x) (comap f (cobounded α) ⊓ 𝓟 s)
Tactic: rw [disjoint_assoc, inf_comm, hk.disjoint_nhdsSet_left]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (hypothesis)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' (t ∩ s))
have this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
Tactic: have : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α)) := by
    rw [disjoint_assoc, inf_comm, hk.disjoint_nhdsSet_left]
    exact fun x hx ↦ disjoint_left_comm.2 <|
      tendsto_comap.disjoint (disjoint_cobounded_nhds _) (hf x hx)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
⊢ ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' (t ∩ s))
have rcases : ∀ (U : Set β) (hUo : IsOpen[inst_1] U) (hkU : k ⊆ U) (t : Set α) (ht : t ∈ cobounded α)
  (hd : Disjoint (U ∩ s) (f ⁻¹' id t)), ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' (t ∩ s))
Tactic: rcases ((((hasBasis_nhdsSet _).inf_principal _)).disjoint_iff ((basis_sets _).comap _)).1 this
    with ⟨U, ⟨hUo, hkU⟩, t, ht, hd⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst_1] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' (t ∩ s))
have refine : f '' (U ∩ s) ⊆ tᶜ
Tactic: refine ⟨U, hkU, hUo, (isBounded_compl_iff.2 ht).subset ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst_1] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ f '' (U ∩ s) ⊆ tᶜ
have rwa : U ∩ s ⊆ f ⁻¹' tᶜ
Tactic: rwa [image_subset_iff, preimage_compl, subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst_1] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
rwa : U ∩ s ⊆ f ⁻¹' tᶜ
⊢ f '' (U ∩ s) ⊆ tᶜ
have rwa₁ : U ∩ s ⊆ (f ⁻¹' t)ᶜ
Tactic: rwa [image_subset_iff, preimage_compl, subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst_1] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
rwa : U ∩ s ⊆ f ⁻¹' tᶜ
rwa₁ : U ∩ s ⊆ (f ⁻¹' t)ᶜ
⊢ f '' (U ∩ s) ⊆ tᶜ
have rwa₂ : Disjoint (U ∩ s) (f ⁻¹' t)
Tactic: rwa [image_subset_iff, preimage_compl, subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (hypothesis)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousAt f x
⊢ ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' t)
have hf₁ : ∀ x ∈ k, ContinuousWithinAt f univ x
Tactic: simp_rw [← continuousWithinAt_univ] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
⊢ IsCompact s
have inl : ∀ (hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hb : Bornology.IsBounded.{u} (α := α) ∅),
  IsCompact.{u} (X := α) ∅
Tactic: rcases eq_empty_or_nonempty s with (rfl | ⟨x, -⟩)
Cleared hypotheses: s, hc, hb