awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
haveI haveI₁ haveI₂ haveI₃ : ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)), IsClopenable s
haveI₄ haveI₅ :
  ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
    let t := sᶜ;
    ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)), IsClopenable s
haveI₆ :
  ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
    let t := sᶜ;
    ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)),
      let f := Equiv.Set.sumCompl s;
      ∀
        (hle :
          coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
              instTopologicalSpaceSum ≤
            inst),
        IsClopenable s
⊢ IsClopenable s
have refine_1 : ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
  let t := sᶜ;
  ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)),
    let f := Equiv.Set.sumCompl s;
    ∀
      (hle :
        coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
            instTopologicalSpaceSum ≤
          inst),
      PolishSpace α
Tactic: classical
  haveI : PolishSpace s := hs.polishSpace
  let t : Set α := sᶜ
  haveI : PolishSpace t := hs.isOpen_compl.polishSpace
  let f : s ⊕ t ≃ α := Equiv.Set.sumCompl s
  have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› := by
    simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]
    exact ⟨continuous_subtype_val, continuous_subtype_val⟩
  refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
  · rw [← f.induced_symm]
    exact f.symm.polishSpace_induced
  · rw [isOpen_coinduced, isOpen_sum_iff]
    simp [preimage_preimage, f, t]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
haveI haveI₁ haveI₂ haveI₃ : ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)), IsClopenable s
haveI₄ haveI₅ :
  ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
    let t := sᶜ;
    ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)), IsClopenable s
haveI₆ :
  ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
    let t := sᶜ;
    ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)),
      let f := Equiv.Set.sumCompl s;
      ∀
        (hle :
          coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
              instTopologicalSpaceSum ≤
            inst),
        IsClopenable s
refine_1 :
  ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
    let t := sᶜ;
    ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)),
      let f := Equiv.Set.sumCompl s;
      ∀
        (hle :
          coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
              instTopologicalSpaceSum ≤
            inst),
        PolishSpace α
⊢ IsClopenable s
have refine_2 : ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
  let t := sᶜ;
  ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)),
    let f := Equiv.Set.sumCompl s;
    ∀
      (hle :
        coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
            instTopologicalSpaceSum ≤
          inst),
      IsOpen[coinduced (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) instTopologicalSpaceSum] s
Tactic: classical
  haveI : PolishSpace s := hs.polishSpace
  let t : Set α := sᶜ
  haveI : PolishSpace t := hs.isOpen_compl.polishSpace
  let f : s ⊕ t ≃ α := Equiv.Set.sumCompl s
  have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› := by
    simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]
    exact ⟨continuous_subtype_val, continuous_subtype_val⟩
  refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
  · rw [← f.induced_symm]
    exact f.symm.polishSpace_induced
  · rw [isOpen_coinduced, isOpen_sum_iff]
    simp [preimage_preimage, f, t]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsClopenable s
⊢ IsClopenable sᶜ
have rcases : ∀ (t : TopologicalSpace α) (t_le : t ≤ inst) (t_polish : PolishSpace α) (h : IsClosed s) (h' : IsOpen s),
  IsClopenable sᶜ
Tactic: rcases hs with ⟨t, t_le, t_polish, h, h'⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), IsClopenable (s n)
⊢ IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)
have choose : ∀ (m : (n : ℕ) → TopologicalSpace α) (mt : ∀ (n : ℕ), m n ≤ t) (m_polish : ∀ (n : ℕ), PolishSpace α),
  (∀ (n : ℕ), IsClosed[m n] (s n)) →
    ∀ (m_open : ∀ (n : ℕ), IsOpen[m n] (s n)), IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)
Tactic: choose m mt m_polish _ m_open using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
⊢ IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)
have obtain : ∀ (t' : TopologicalSpace α) (t'm : ∀ (n : ℕ), t' ≤ m n) (t'_polish : PolishSpace α),
  IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)
Tactic: obtain ⟨t', t'm, -, t'_polish⟩ :
      ∃ t' : TopologicalSpace α, (∀ n : ℕ, t' ≤ m n) ∧ t' ≤ t ∧ @PolishSpace α t' :=
    exists_polishSpace_forall_le m mt m_polish
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
⊢ IsOpen[t'] (⋃ (n : ℕ), s n)
have h : ∀ (i : ℕ), IsOpen[t'] (s i)
Tactic: apply isOpen_iUnion
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
n : ℕ
⊢ IsOpen[t'] (s n)
have h : IsOpen[m n] (s n)
Tactic: apply t'm n
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
⊢ IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)
have A : IsOpen[t'] (⋃ (n : ℕ), s n)
Tactic: have A : IsOpen[t'] (⋃ n, s n) := by
    apply isOpen_iUnion
    intro n
    apply t'm n
    exact m_open n
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
t : TopologicalSpace α
inst : PolishSpace α
s : ℕ → Set α
m : (n : ℕ) → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
A : IsOpen[t'] (⋃ (n : ℕ), s n)
⊢ IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)
have obtain : ∀ (t'' : TopologicalSpace α) (t''_le : t'' ≤ t') (t''_polish : PolishSpace α)
  (h1 : IsClosed.{u_1} (X := α) (⋃ (n : ℕ), s n)) (h2 : IsOpen.{u_1} (X := α) (⋃ (n : ℕ), s n)),
  IsClopenable.{u_1} (α := α) (⋃ (n : ℕ), s n)
Tactic: obtain ⟨t'', t''_le, t''_polish, h1, h2⟩ : ∃ t'' : TopologicalSpace α,
      t'' ≤ t' ∧ @PolishSpace α t'' ∧ IsClosed[t''] (⋃ n, s n) ∧ IsOpen[t''] (⋃ n, s n) :=
    @IsOpen.isClopenable α t' t'_polish _ A
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
have inl : ∀ (hs : IsClosed.{u_1} (X := α) ∅) (h : ∅ ⊆ ball x r), ∃ r' ∈ Ioo 0 r, ∅ ⊆ ball x r'
Tactic: rcases eq_empty_or_nonempty s with (rfl | hne)
Cleared hypotheses: s, hs, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
inl : ∀ (hs : IsClosed.{u_1} (X := α) ∅) (h : ∅ ⊆ ball x r), ∃ r' ∈ Ioo 0 r, ∅ ⊆ ball x r'
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
have inr : ∀ (hne : s.Nonempty), ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
Tactic: rcases eq_empty_or_nonempty s with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
have this : IsCompact s
Tactic: have : IsCompact s :=
    (isCompact_closedBall x r).of_isClosed_subset hs (h.trans ball_subset_closedBall)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
have inr : ∀ (y : α) (hys : y ∈ s) (hy : s ⊆ closedBall x (dist y x)), ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
Tactic: obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closedBall x (dist y x) :=
    this.exists_isMaxOn (β := α) (α := ℝ) hne (by fun_prop)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
have hyr : dist y x < r
Tactic: have hyr : dist y x < r := h hys
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
hyr : dist y x < r
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
have inr : ∀ (r' : ℝ) (hyr' : dist y x < r') (hrr' : r' < r), ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
Tactic: rcases exists_between hyr with ⟨r', hyr', hrr'⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
⊢ ∃ r' < r, s ⊆ ball x r'
have inl : ∀ (hr : r ≤ 0), ∃ r' < r, s ⊆ ball x r'
Tactic: rcases le_or_gt r 0 with hr | hr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
inl : ∀ (hr : r ≤ 0), ∃ r' < r, s ⊆ ball x r'
⊢ ∃ r' < r, s ⊆ ball x r'
have inr : ∀ (hr : 0 < r), ∃ r' < r, s ⊆ ball x r'
Tactic: rcases le_or_gt r 0 with hr | hr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : r ≤ 0
⊢ ∃ r' < r, s ⊆ ball x r'
have h₁ : s = ∅
Tactic: rw [ball_eq_empty.2 hr, subset_empty_iff] at h
Cleared hypotheses: h, hr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s = ∅
hr : r ≤ 0
⊢ ∃ r' < r, s ⊆ ball x r'
have inl : ∀ (hs : IsClosed.{u_1} (X := α) ∅), ∃ r' < r, ∅ ⊆ ball x r'
Tactic: subst s
Cleared hypotheses: s, hs, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
inst_2 : TopologicalSpace β
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : OrderTopology β
f : α → β
a z : α
r : ℝ
hf : ContinuousOn f (closedBall a r)
hz : z ∈ closedBall a r
hf1 : ∀ z' ∈ sphere a r, f z < f z'
⊢ ∃ z ∈ ball a r, IsLocalMin f z
have hf1₁ : ∀ z' ∈ closedBall a r \ ball a r, f z < f z'
Tactic: simp_rw [← closedBall_diff_ball] at hf1
Cleared hypotheses: hf1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
⊢ ProperSpace α ↔ ∀ (x : α), IsProperMap (dist x)
have refine : ∀ (H : ∀ (x : α), IsProperMap (dist x)) (x : α) (r : ℝ), IsCompact (closedBall x r)
Tactic: refine ⟨fun _ ↦ isProperMap_dist, fun H ↦ ⟨fun x r ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
H : ∀ (x : α), IsProperMap (dist x)
x : α
r : ℝ
⊢ IsCompact (closedBall x r)
have h : closedBall x r = dist x ⁻¹' closedBall 0 r
Tactic: convert! (H x).isCompact_preimage (isCompact_closedBall 0 r)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
H : ∀ (x : α), IsProperMap (dist x)
x : α
r : ℝ
⊢ closedBall x r = dist x ⁻¹' closedBall 0 r
have h : ∀ (x_1 : α), x_1 ∈ closedBall x r ↔ x_1 ∈ dist x ⁻¹' closedBall 0 r
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace.Real (hypothesis)
Goal:
x : ℝ≥0
r : ℝ
⊢ IsCompact (Metric.closedBall x r)
have emb : IsClosedEmbedding toReal
Tactic: have emb : IsClosedEmbedding ((↑) : ℝ≥0 → ℝ) := Isometry.isClosedEmbedding fun _ ↦ congrFun rfl
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
⊢ SecondCountableTopology α
have suffices : SigmaCompactSpace α
Tactic: suffices SigmaCompactSpace α from EMetric.secondCountable_of_sigmaCompact α
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
⊢ SigmaCompactSpace α
have inl : ∀ (x : α), SigmaCompactSpace α
Tactic: rcases em (Nonempty α) with (⟨⟨x⟩⟩ | hn)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
inl : ∀ (x : α), SigmaCompactSpace α
⊢ SigmaCompactSpace α
have inr : ∀ (hn : ¬Nonempty α), SigmaCompactSpace α
Tactic: rcases em (Nonempty α) with (⟨⟨x⟩⟩ | hn)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
f : Filter α
hf : Cauchy f
⊢ ∃ (x : α), f ≤ nhds x
have obtain : ∀ (t : Set α) (t_fset : t ∈ f) (ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1), ∃ (x : α), f ≤ nhds x
Tactic: obtain ⟨t, t_fset, ht⟩ : ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < 1 :=
      (Metric.cauchy_iff.1 hf).2 1 zero_lt_one
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
⊢ ∃ (x : α), f ≤ nhds x
have rcases : ∀ (x : α) (xt : x ∈ t), ∃ (x : α), f ≤ nhds x
Tactic: rcases hf.1.nonempty_of_mem t_fset with ⟨x, xt⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace (hypothesis)
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
x : α
xt : x ∈ t
⊢ ∃ (x : α), f ≤ nhds x
have this : closedBall x 1 ∈ f
Tactic: have : closedBall x 1 ∈ f := mem_of_superset t_fset fun y yt => (ht y yt x xt).le
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
x : α
xt : x ∈ t
this : closedBall x 1 ∈ f
⊢ ∃ (x : α), f ≤ nhds x
have rcases : ∀ (y : α) (hy : f ≤ nhds y), ∃ (x : α), f ≤ nhds x
Tactic: rcases (isCompact_iff_totallyBounded_isComplete.1 (isCompact_closedBall x 1)).2 f hf
        (le_principal_iff.2 this) with
      ⟨y, -, hy⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace (goal)
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α_1
α : Type u_3
β : Type u_4
inst_1 : PseudoMetricSpace α
inst_2 : PseudoMetricSpace β
inst_3 : ProperSpace α
inst_4 : ProperSpace β
x : α
y : β
r : ℝ
⊢ IsCompact (closedBall (x, y) r)
have rw : IsCompact (closedBall x r ×ˢ closedBall y r)
Tactic: rw [← closedBall_prod_same x y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace (goal)
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace.{u_3} (X b)
⊢ ProperSpace ((b : β) → X b)
have refine : ∀ (x : (b : β) → X b) (r : ℝ) (hr : 0 ≤ r), IsCompact (closedBall x r)
Tactic: refine .of_isCompact_closedBall_of_le 0 fun x r hr => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ProperSpace (goal)
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace.{u_3} (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ IsCompact (closedBall x r)
have rw : IsCompact (X := (b : β) → X b) (Set.pi (α := X) univ fun (b : β) ↦ closedBall (x b) r)
Tactic: rw [closedBall_pi _ hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
⊢ dist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, dist (f i) (f (i + 1))
have base : dist (f m) (f m) ≤ ∑ i ∈ ∅, dist (f i) (f (i + 1))
Tactic: rw [Finset.Ico_self, Finset.sum_empty, dist_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
base : dist (f m) (f m) ≤ ∑ i ∈ ∅, dist (f i) (f (i + 1))
⊢ dist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, dist (f i) (f (i + 1))
have base₁ : dist (f m) (f m) ≤ 0
Tactic: rw [Finset.Ico_self, Finset.sum_empty, dist_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
base : dist (f m) (f m) ≤ ∑ i ∈ ∅, dist (f i) (f (i + 1))
base₁ : dist (f m) (f m) ≤ 0
⊢ dist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, dist (f i) (f (i + 1))
have base₂ : LE.le (α := ℝ) 0 0
Tactic: rw [Finset.Ico_self, Finset.sum_empty, dist_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n_1 n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) + dist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), dist (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.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n_1 n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ dist (f m) (f (n + 1)) ≤ ∑ i ∈ Finset.Ico m (n + 1), dist (f i) (f (i + 1))
have dist : ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) + dist (f n) (f (n + 1)) =
  ∑ i ∈ Finset.Ico m (n + 1), dist (f i) (f (i + 1))
Tactic: calc
      dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_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.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
h : m ≤ n
⊢ dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
have base : dist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, dist (f i) (f (i + 1))
Tactic: induction n, h using Nat.le_induction with
  | base => rw [Finset.Ico_self, Finset.sum_empty, dist_self]
  | succ n hle ihn =>
    calc
      dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_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.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
h : m ≤ n
base : dist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, dist (f i) (f (i + 1))
⊢ dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
have succ : ∀ (n : ℕ) (hle : m ≤ n) (ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))),
  dist (f m) (f (n + 1)) ≤ ∑ i ∈ Finset.Ico m (n + 1), dist (f i) (f (i + 1))
Tactic: induction n, h using Nat.le_induction with
  | base => rw [Finset.Ico_self, Finset.sum_empty, dist_self]
  | succ n hle ihn =>
    calc
      dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_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.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
⊢ IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
have rw : IsUniformInducing f ∧ Function.Injective f ↔
  Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
Tactic: rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
rw :
  IsUniformInducing f ∧ Function.Injective f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
⊢ IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
have rw₁ : Function.Injective f ∧ IsUniformInducing f ↔
  Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
Tactic: rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
rw :
  IsUniformInducing f ∧ Function.Injective f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
rw₁ :
  Function.Injective f ∧ IsUniformInducing f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
⊢ IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
have rw₂ : (Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ) ↔
  Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
Tactic: rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff]