awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ 2 * u n) atTop (𝓝 0)

Tactic:
simpa only [mul_zero] using u_lim.const_mul 2

Premises used: Filter.Tendsto.const_mul, MulZeroClass.mul_zero, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ 2 * u n) atTop (𝓝 0)

Tactic:
have : Tendsto (fun n => 2 * u n) atTop (𝓝 0) := by
        simpa only [mul_zero] using u_lim.const_mul 2
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this_2 : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ 2 * u n) atTop (𝓝 0)
⊢ CauchySeq y

Tactic:
cauchySeq_of_le_tendsto_0' (fun n => 2 * u n) (fun m n hmn => ?_) this

Premises used: HMul.hMul, OfNat.ofNat, cauchySeq_of_le_tendsto_0'
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this_2 : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ 2 * u n) atTop (𝓝 0)
refine : ∀ (m n : ℕ) (hmn : m ≤ n), dist (y m) (y n) ≤ (fun (n : ℕ) ↦ 2 * u n) m
⊢ CauchySeq y

Tactic:
refine cauchySeq_of_le_tendsto_0' (fun n => 2 * u n) (fun m n hmn => ?_) this

Premises used: HMul.hMul, OfNat.ofNat, cauchySeq_of_le_tendsto_0'
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this_2 : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ 2 * u n) atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
rcases :
  ∀ (z : γ) (zsm : z ∈ (↑(s m) : Set γ)) (zsn : z ∈ (↑(s n) : Set γ)), dist (y m) (y n) ≤ (fun (n : ℕ) ↦ 2 * u n) m
⊢ dist (y m) (y n) ≤ (fun (n : ℕ) ↦ 2 * u n) m

Tactic:
rcases I m n with ⟨z, zsm, zsn⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this_2 : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ 2 * u n) atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
z : γ
zsm : z ∈ (↑(s m) : Set γ)
zsn : z ∈ (↑(s n) : Set γ)
⊢ dist (y m) (y n) ≤ dist (y m) z + dist z (y n)

Tactic:
dist_triangle _ _ _

Premises used: dist_triangle
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this_2 : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ 2 * u n) atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
z : γ
zsm : z ∈ (↑(s m) : Set γ)
zsn : z ∈ (↑(s n) : Set γ)
⊢ dist (y m) z + dist z (y n) ≤ u m + u n

Tactic:
(add_le_add ((dist_le_diam_of_mem (hs m).1 (hy m) zsm).trans (hs m).2)
            ((dist_le_diam_of_mem (hs n).1 zsn (hy n)).trans (hs n).2))

Premises used: add_le_add, Metric.dist_le_diam_of_mem, And.right, And.left, LE.le.trans
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this_2 : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ 2 * u n) atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
z : γ
zsm : z ∈ (↑(s m) : Set γ)
zsn : z ∈ (↑(s n) : Set γ)
linarith : 2 * u m < u m + u n → 2 * u m - (u m + u n) + (u n - u m) = 0
⊢ u m + u n ≤ 2 * u m

Tactic:
linarith [u_anti.antitone hmn]

Premises used: StrictAnti.antitone
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this_2 : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ 2 * u n) atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
z : γ
zsm : z ∈ (↑(s m) : Set γ)
zsn : z ∈ (↑(s n) : Set γ)
dist : u m + u n ≤ 2 * u m
⊢ Dist.dist (y m) (y n) ≤ (fun (n : ℕ) ↦ 2 * u n) m

Tactic:
calc
        dist (y m) (y n) ≤ dist (y m) z + dist z (y n) := dist_triangle _ _ _
        _ ≤ u m + u n :=
          (add_le_add ((dist_le_diam_of_mem (hs m).1 (hy m) zsm).trans (hs m).2)
            ((dist_le_diam_of_mem (hs n).1 zsn (hy n)).trans (hs n).2))
        _ ≤ 2 * u m := by linarith [u_anti.antitone hmn]

Premises used: dist_triangle, add_le_add, Metric.dist_le_diam_of_mem, And.right, And.left, Dist.dist, LE.le.trans
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
⊢ CauchySeq y

Tactic:
have cauchy_y : CauchySeq y := by
      have : Tendsto (fun n => 2 * u n) atTop (𝓝 0) := by
        simpa only [mul_zero] using u_lim.const_mul 2
      refine cauchySeq_of_le_tendsto_0' (fun n => 2 * u n) (fun m n hmn => ?_) this
      rcases I m n with ⟨z, zsm, zsn⟩
      calc
        dist (y m) (y n) ≤ dist (y m) z + dist z (y n) := dist_triangle _ _ _
        _ ≤ u m + u n :=
          (add_le_add ((dist_le_diam_of_mem (hs m).1 (hy m) zsm).trans (hs m).2)
            ((dist_le_diam_of_mem (hs n).1 zsn (hy n)).trans (hs n).2))
        _ ≤ 2 * u m := by linarith [u_anti.antitone hmn]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
cauchy_y : CauchySeq y
⊢ Nonempty γ

Tactic:
haveI : Nonempty γ := ⟨y 0⟩