awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (u N) < ε
N n : ℕ
hn : n ≥ N
hN : dist (u n) (u N) < 1
refine_2 : ∀ (this : ¬u n = u N), False
⊢ u n = u N

Tactic:
by_contra
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (u N) < ε
N n : ℕ
hn : n ≥ N
hN : dist (u n) (u N) < 1
this : ¬u n = u N
⊢ LT.lt (α := ℝ) (if u n = u N then 0 else 1) 1

Tactic:
change (if u n = u N then 0 else 1) < 1 at hN

Premises used: OfNat.ofNat, ite
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (u N) < ε
N n : ℕ
hn : n ≥ N
this : ¬u n = u N
hN : LT.lt (α := ℝ) (if u n = u N then 0 else 1) 1
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
let let₁ let₂ : IsCompletelyMetrizableSpace X
refine_1 :
  let m :=
    { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯,
      edist_dist := ⋯, uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ : MetricSpace X };
  UniformSpace.toTopologicalSpace = inst
refine_2 refine_2₁ :
  let m :=
    { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯,
      edist_dist := ⋯, uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ : MetricSpace X };
  CompleteSpace X
⊢ IsCompletelyMetrizableSpace X

Tactic:
classical
  let m : MetricSpace X :=
    { dist x y := if x = y then 0 else 1
      dist_self x := by simp
      dist_comm x y := by
        obtain h | h := eq_or_ne x y
        · simp [h]
        · simp [h, h.symm]
      dist_triangle x y z := by
        by_cases x = y <;> by_cases x = z <;> by_cases y = z <;> simp_all
      eq_of_dist_eq_zero := by simp }
  refine ⟨m, ?_, ?_⟩
  · rw [DiscreteTopology.eq_bot (α := X)]
    refine eq_bot_of_singletons_open fun x ↦ ?_
    convert! @Metric.isOpen_ball _ _ x 1
    refine subset_antisymm (singleton_subset_iff.2 (Metric.mem_ball_self (by simp)))
      fun y hy ↦ ?_
    simp only [Metric.mem_ball, mem_singleton_iff] at *
    by_contra
    change (if y = x then 0 else 1) < 1 at hy
    simp_all
  · refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_
    rw [Metric.cauchySeq_iff'] at hu
    obtain ⟨N, hN⟩ := hu 1 (by simp)
    refine ⟨u N, @tendsto_atTop_of_eventually_const X UniformSpace.toTopologicalSpace (u N) _ _ _ N
      fun n hn ↦ ?_⟩
    specialize hN n hn
    by_contra
    change (if u n = u N then 0 else 1) < 1 at hN
    simp_all

Premises used: Iff.mpr, Set.singleton_subset_iff, Metric.mem_ball_self, subset_antisymm, Metric.mem_ball, Set.mem_singleton_iff, Metric.complete_of_cauchySeq_tendsto, DiscreteTopology.eq_bot, eq_bot_of_singletons_open, Metric.cauchySeq_iff'
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyMetrizableSpace X
s : Set X
hs : IsClosed[inst] s
⊢ IsCompletelyMetrizableSpace.{u_1} (↑s : Type u_1)

Tactic:
hs.isClosedEmbedding_subtypeVal.IsCompletelyMetrizableSpace

Premises used: IsClosed.isClosedEmbedding_subtypeVal, Topology.IsClosedEmbedding.IsCompletelyMetrizableSpace
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : IsCompletelyMetrizableSpace X
⊢ IsCompletelyMetrizableSpace.{u_1} (↑Set.univ : Type u_1)

Tactic:
isClosed_univ.isCompletelyMetrizableSpace

Premises used: isClosed_univ, IsClosed.isCompletelyMetrizableSpace
-- Module: Mathlib.Topology.Metrizable.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : SigmaCompactSpace X
inst_3 : TopologicalSpace Y
inst_4 : PseudoMetrizableSpace Y
⊢ PseudoMetrizableSpace C(X, Y)

Tactic:
let := pseudoMetrizableSpaceUniformity Y
  have := pseudoMetrizableSpaceUniformity_countably_generated Y
  inferInstance

Premises used: inferInstance, TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated, TopologicalSpace.pseudoMetrizableSpaceUniformity
-- Module: Mathlib.Topology.Metrizable.Real
Goal:
⊢ MetrizableSpace ℝ≥0∞

Tactic:
orderIsoUnitIntervalBirational.toHomeomorph.isEmbedding.metrizableSpace

Premises used: Topology.IsEmbedding.metrizableSpace, ENNReal.orderIsoUnitIntervalBirational, Homeomorph.isEmbedding, OrderIso.toHomeomorph
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x : X
⊢ (zipWith d [x] ([] ++ [x])).sum = 0

Tactic:
simp [dist_self]
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
⊢ Eq (α := ℝ≥0) (⨅ (l : List X), (zipWith d (x :: l) (l ++ [y])).sum)
    (⨅ (l : List X), (zipWith d (y :: l) (l ++ [x])).sum)

Tactic:
reverse_surjective.iInf_congr _ fun l ↦ ?_

Premises used: List.reverse_surjective, Function.Surjective.iInf_congr
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
refine : ∀ (l : List X), (zipWith d (y :: l.reverse) (l.reverse ++ [x])).sum = (zipWith d (x :: l) (l ++ [y])).sum
⊢ Eq (α := ℝ≥0) (⨅ (l : List X), (zipWith d (x :: l) (l ++ [y])).sum)
    (⨅ (l : List X), (zipWith d (y :: l) (l ++ [x])).sum)

Tactic:
refine reverse_surjective.iInf_congr _ fun l ↦ ?_

Premises used: List.reverse_surjective, Function.Surjective.iInf_congr
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
l : List X
rw : (y :: l.reverse).length = (l.reverse ++ [x]).length
⊢ (zipWith d (y :: l.reverse) (l.reverse ++ [x])).sum = (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
rw [← sum_reverse, reverse_zipWith, reverse_append, reverse_reverse,
        reverse_singleton, singleton_append, reverse_cons, reverse_reverse,
        zipWith_comm_of_comm dist_comm]

Premises used: List.reverse_singleton, List.sum_reverse, List.reverse_cons, List.singleton_append, List.reverse_reverse, List.reverse_append, List.zipWith_comm_of_comm, List.reverse_zipWith
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length

Tactic:
simp only [length, length_append]

Premises used: List.length_append, List.length
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
⊢ ⨅ (l : List X), (zipWith d (x :: l) (l ++ [z])).sum ≤
    HAdd.hAdd (α := ℝ≥0) (⨅ (l : List X), (zipWith d (x :: l) (l ++ [y])).sum)
      (⨅ (l : List X), (zipWith d (y :: l) (l ++ [z])).sum)

Tactic:
NNReal.le_iInf_add_iInf fun lxy lyz ↦ ?_

Premises used: NNReal.le_iInf_add_iInf
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
refine :
  ∀ (lxy lyz : List X),
    ⨅ (l : List X), (zipWith d (x :: l) (l ++ [z])).sum ≤
      (zipWith d (x :: lxy) (lxy ++ [y])).sum + (zipWith d (y :: lyz) (lyz ++ [z])).sum
⊢ ⨅ (l : List X), (zipWith d (x :: l) (l ++ [z])).sum ≤
    HAdd.hAdd (α := ℝ≥0) (⨅ (l : List X), (zipWith d (x :: l) (l ++ [y])).sum)
      (⨅ (l : List X), (zipWith d (y :: l) (l ++ [z])).sum)

Tactic:
refine NNReal.le_iInf_add_iInf fun lxy lyz ↦ ?_

Premises used: NNReal.le_iInf_add_iInf
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ ⨅ (l : List X), (zipWith d (x :: l) (l ++ [z])).sum ≤ (zipWith d (x :: lxy ++ y :: lyz) (lxy ++ y :: lyz ++ [z])).sum

Tactic:
ciInf_le (OrderBot.bddBelow _) (lxy ++ y::lyz)

Premises used: List.cons, List.append, ciInf_le, OrderBot.bddBelow, HAppend.hAppend
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
rw : (x :: lxy).length = (lxy ++ [y]).length
⊢ (zipWith d (x :: lxy ++ y :: lyz) (lxy ++ y :: lyz ++ [z])).sum =
    (zipWith d (x :: lxy) (lxy ++ [y])).sum + (zipWith d (y :: lyz) (lyz ++ [z])).sum

Tactic:
rw [← sum_append, ← zipWith_append, cons_append, ← @singleton_append _ y, append_assoc,
          append_assoc, append_assoc]

Premises used: List.append_assoc, List.zipWith_append, List.singleton_append, List.sum_append, List.cons_append
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
rw : lxy.length + 1 = (lxy ++ [y]).length
rw₁ : lxy.length + 1 = lxy.length + [y].length
rw₂ rw₃ : lxy.length + 1 = lxy.length + 1
⊢ (x :: lxy).length = (lxy ++ [y]).length

Tactic:
rw [length_cons, length_append, length_singleton]

Premises used: List.length_cons, List.length_singleton, List.length_append
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
d₁ :
  (zipWith d (x :: lxy ++ y :: lyz) (lxy ++ y :: lyz ++ [z])).sum =
    (zipWith d (x :: lxy) (lxy ++ [y])).sum + (zipWith d (y :: lyz) (lyz ++ [z])).sum
⊢ ⨅ (l : List X), (zipWith d (x :: l) (l ++ [z])).sum ≤
    (zipWith d (x :: lxy) (lxy ++ [y])).sum + (zipWith d (y :: lyz) (lyz ++ [z])).sum

Tactic:
calc
      ⨅ l, (zipWith d (x::l) (l ++ [z])).sum ≤
          (zipWith d (x::lxy ++ y::lyz) ((lxy ++ y::lyz) ++ [z])).sum :=
        ciInf_le (OrderBot.bddBelow _) (lxy ++ y::lyz)
      _ = (zipWith d (x::lxy) (lxy ++ [y])).sum + (zipWith d (y::lyz) (lyz ++ [z])).sum := by
        rw [← sum_append, ← zipWith_append, cons_append, ← @singleton_append _ y, append_assoc,
          append_assoc, append_assoc]
        rw [length_cons, length_append, length_singleton]

Premises used: List.zipWith, List.sum, List.cons, ciInf_le, OrderBot.bddBelow, HAppend.hAppend, List.nil
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
⊢ dist x y = (↑(⨅ (l : List X), (zipWith d (x :: l) (l ++ [y])).sum) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
⊢ (zipWith d [x] ([] ++ [y])).sum = d x y

Tactic:
simp
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
rw : d x y ≤ ⨅ (i : List X), 2 * (zipWith d (x :: i) (i ++ [y])).sum
⊢ (↑(d x y) : ℝ) ≤ 2 * dist x y

Tactic:
rw [dist_ofPreNNDist, ← NNReal.coe_two, ← NNReal.coe_mul, NNReal.mul_iInf, NNReal.coe_le_coe]

Premises used: PseudoMetricSpace.dist_ofPreNNDist, NNReal.coe_two, NNReal.mul_iInf, NNReal.coe_mul, NNReal.coe_le_coe
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
⊢ d x y ≤ ⨅ (i : List X), 2 * (zipWith d (x :: i) (i ++ [y])).sum

Tactic:
le_ciInf fun l => ?_

Premises used: le_ciInf
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
refine : ∀ (l : List X), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
⊢ d x y ≤ ⨅ (i : List X), 2 * (zipWith d (x :: i) (i ++ [y])).sum

Tactic:
refine le_ciInf fun l => ?_

Premises used: le_ciInf
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
⊢ IsTrans X fun (x y : X) ↦ d x y = 0

Tactic:
⟨fun a b c hab hbc ↦ ?_⟩

Premises used: IsTrans.mk
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
refine : ∀ (a b c : X) (hab : d a b = 0) (hbc : d b c = 0), d a c = 0
⊢ IsTrans X fun (x y : X) ↦ d x y = 0

Tactic:
refine ⟨fun a b c hab hbc ↦ ?_⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
a b c : X
hab : d a b = 0
hbc : d b c = 0
rw : d a c ≤ 0
⊢ d a c = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
a b c : X
hab : d a b = 0
hbc : d b c = 0
⊢ d a c ≤ 0

Tactic:
simpa only [nonpos_iff_eq_zero, hab, hbc, dist_self c, max_self, mul_zero] using hd a b c c

Premises used: max_self, MulZeroClass.mul_zero, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
⊢ IsTrans X fun (x y : X) ↦ d x y = 0

Tactic:
haveI : IsTrans X fun x y => d x y = 0 := by
    refine ⟨fun a b c hab hbc ↦ ?_⟩
    rw [← nonpos_iff_eq_zero]
    simpa only [nonpos_iff_eq_zero, hab, hbc, dist_self c, max_self, mul_zero] using hd a b c c
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
this_1 : IsTrans X fun (x y : X) ↦ d x y = 0
this : ∀ (n : ℕ), l.length = n → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
this _ rfl

Premises used: rfl
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
this_1 : IsTrans X fun (x y : X) ↦ d x y = 0
this : ∀ (n : ℕ), l.length = n → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
exact this _ rfl

Premises used: rfl
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
this : IsTrans X fun (x y : X) ↦ d x y = 0
suffices : ∀ (n : ℕ), l.length = n → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
suffices ∀ n, length l = n → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum by exact this _ rfl
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
n : ℕ
ihn : ∀ m < n, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
x y : X
l : List X
hn : l.length = n
⊢ ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
subst n
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
h :
  let L := zipWith d (x :: l) (l ++ [y]);
  d x y ≤ 2 * L.sum
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
set L := zipWith d (x::l) (l ++ [y])

Premises used: List.zipWith, List.cons, HAppend.hAppend, List.nil
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
⊢ L.length = l.length + 1

Tactic:
simp [L]
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
⊢ L.length = l.length + 1

Tactic:
have hL_len : length L = length l + 1 := by simp [L]
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
h : ∀ (hd₀ : d x y = 0), d x y ≤ 2 * L.sum
h₁ : ∀ (hd₀ : d x y ≠ 0), d x y ≤ 2 * L.sum
⊢ d x y ≤ 2 * L.sum

Tactic:
rcases eq_or_ne (d x y) 0 with hd₀ | hd₀

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y = 0
⊢ d x y ≤ 2 * L.sum

Tactic:
simp only [hd₀, zero_le]

Premises used: zero_le
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
h : ∀ (z z' : X) (hxz : d x z ≤ L.sum) (hzz' : d z z' ≤ L.sum) (hz'y : d z' y ≤ L.sum), d x y ≤ 2 * L.sum
rsuffices : ∃ (z : X) (z' : X), d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum
⊢ d x y ≤ 2 * L.sum

Tactic:
rsuffices ⟨z, z', hxz, hzz', hz'y⟩ : ∃ z z' : X, d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum

Premises used: List.sum
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
z z' : X
hxz : d x z ≤ L.sum
hzz' : d z z' ≤ L.sum
hz'y : d z' y ≤ L.sum
h : 2 * max (d x z) (max (d z z') (d z' y)) ≤ 2 * L.sum
h₁ h₂ : 2 * L.sum ≤ 2 * L.sum
⊢ d x y ≤ 2 * L.sum

Tactic:
grw [hd x z z' y, max_le hxz (max_le hzz' hz'y)]

Premises used: max_le
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m : ℕ | 2 * (take m L).sum ≤ L.sum}
⊢ 0 ∈ s

Tactic:
simp [s]
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m : ℕ | 2 * (take m L).sum ≤ L.sum}
⊢ 0 ∈ s

Tactic:
have hs₀ : 0 ∈ s := by simp [s]
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : l.length = m), d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m : ℕ | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
⊢ s.Nonempty

Tactic:
have hsne : s.Nonempty := ⟨0, hs₀⟩