awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
x y z : X
refine_1 :
  HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) y z : R) ≤
    HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
      ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
⊢ (d : (a : X) → X → R) x z ≤
      HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
        ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R) ∧
    (d' : (a : X) → X → R) x z ≤
      HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
        ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
have refine_2 : HAdd.hAdd (α := R) (β := R) ((d' : (a : X) → X → R) x y : R) ((d' : (a : X) → X → R) y z : R) ≤
  HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
    ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
Tactic: refine ⟨(d.triangle x y z).trans ?_, (d'.triangle x y z).trans ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) y z : R) ≤
    HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
      ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
have refine_1 : LE.le.{u_2} (α := R) ((d : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
x y z : X
refine_1 :
  LE.le.{u_2} (α := R) ((d : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
⊢ HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) y z : R) ≤
    HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
      ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
have refine_1₁ : LE.le.{u_2} (α := R) ((d : (a : X) → X → R) y z : R) ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ HAdd.hAdd (α := R) (β := R) ((d' : (a : X) → X → R) x y : R) ((d' : (a : X) → X → R) y z : R) ≤
    HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
      ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
have refine_2 : LE.le.{u_2} (α := R) ((d' : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
x y z : X
refine_2 :
  LE.le.{u_2} (α := R) ((d' : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
⊢ HAdd.hAdd (α := R) (β := R) ((d' : (a : X) → X → R) x y : R) ((d' : (a : X) → X → R) y z : R) ≤
    HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
      ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
have refine_2₁ : LE.le.{u_2} (α := R) ((d' : (a : X) → X → R) y z : R) ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
d : PseudoMetric X R
x y : X
⊢ LE.le.{u_2} (α := R) (0 : R) ((d : (a : X) → X → R) x y : R)
have by_contra! : ∀ (H : LT.lt.{u_2} (α := R) ((d : (a : X) → X → R) x y : R) (0 : R)), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
d : PseudoMetric X R
x y : X
H : LT.lt.{u_2} (α := R) ((d : (a : X) → X → R) x y : R) (0 : R)
⊢ LT.lt.{u_2} (α := R) ((d : (a : X) → X → R) x x : R) (0 : R)
have calc : HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) y x : R) < HAdd.hAdd (α := R) 0 0
Tactic: calc d x x ≤ d x y + d y x := d.triangle' x y x
      _ < 0 + 0 := by refine add_lt_add H (d.symm x y ▸ H)
      _ = 0 := by simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
d : PseudoMetric X R
x y : X
H : LT.lt.{u_2} (α := R) ((d : (a : X) → X → R) x y : R) (0 : R)
calc :
  HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) y x : R) < HAdd.hAdd (α := R) 0 0
⊢ LT.lt.{u_2} (α := R) ((d : (a : X) → X → R) x x : R) (0 : R)
have calc₁ : HAdd.hAdd (α := R) 0 0 = 0
Tactic: calc d x x ≤ d x y + d y x := d.triangle' x y x
      _ < 0 + 0 := by refine add_lt_add H (d.symm x y ▸ H)
      _ = 0 := by simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (hypothesis)
Goal:
X : Type u_1
R : Type u_2
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
d : PseudoMetric X R
x y : X
H : LT.lt.{u_2} (α := R) ((d : (a : X) → X → R) x y : R) (0 : R)
⊢ False
have this : LT.lt.{u_2} (α := R) ((d : (a : X) → X → R) x x : R) (0 : R)
Tactic: have : d x x < 0 := by
    calc d x x ≤ d x y + d y x := d.triangle' x y x
      _ < 0 + 0 := by refine add_lt_add H (d.symm x y ▸ H)
      _ = 0 := by simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
Y : Type u_3
f : Y → PseudoMetric X R
s : Finset Y
hs : s.Nonempty
x y : X
⊢ Eq.{u_2 + 1} (α := R) ((s.sup f : (a : X) → X → R) x y : R) (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) x y : R)
have singleton : ∀ (i : Y),
  Eq.{u_2 + 1} (α := R) ((Finset.sup {i} f : (a : X) → X → R) x y : R)
    (Finset.sup' {i} sorry fun (i : Y) ↦ (f i : (a : X) → X → R) x y : R)
Tactic: induction hs using Finset.Nonempty.cons_induction with
  | singleton i => simp
  | cons a s ha hs ih => simp [hs, ih]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
Y : Type u_3
f : Y → PseudoMetric X R
s : Finset Y
hs : s.Nonempty
x y : X
singleton :
  ∀ (i : Y),
    Eq.{u_2 + 1} (α := R) ((Finset.sup {i} f : (a : X) → X → R) x y : R)
      (Finset.sup' {i} ⋯ fun (i : Y) ↦ (f i : (a : X) → X → R) x y : R)
⊢ Eq.{u_2 + 1} (α := R) ((s.sup f : (a : X) → X → R) x y : R) (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) x y : R)
have cons : ∀ (a : Y) (s : Finset Y) (ha : a ∉ s) (hs : s.Nonempty)
  (ih :
    Eq.{u_2 + 1} (α := R) ((s.sup f : (a : X) → X → R) x y : R)
      (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) x y : R)),
  Eq.{u_2 + 1} (α := R) (((Finset.cons a s ha).sup f : (a : X) → X → R) x y : R)
    ((Finset.cons a s ha).sup' sorry fun (i : Y) ↦ (f i : (a : X) → X → R) x y : R)
Tactic: induction hs using Finset.Nonempty.cons_induction with
  | singleton i => simp
  | cons a s ha hs ih => simp [hs, ih]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
inst_4 : d.IsUltra
inst_5 : d'.IsUltra
⊢ (d ⊔ d').IsUltra
have le_sup' : ∀ (x y z : X),
  LE.le.{u_2} (α := R) ((d ⊔ d' : (a : X) → X → R) x z : R)
    ((d ⊔ d' : (a : X) → X → R) x y ⊔ (d ⊔ d' : (a : X) → X → R) y z : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
inst_4 : d.IsUltra
inst_5 : d'.IsUltra
x y z : X
⊢ LE.le.{u_2} (α := R) ((d ⊔ d' : (a : X) → X → R) x z : R)
    ((d ⊔ d' : (a : X) → X → R) x y ⊔ (d ⊔ d' : (a : X) → X → R) y z : R)
have le_sup' : LE.le.{u_2} (α := R) ((d : (a : X) → X → R) x z ⊔ (d' : (a : X) → X → R) x z : R)
  ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y ⊔ ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z) :
    R)
Tactic: simp only [PseudoMetric.sup_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
inst_4 : d.IsUltra
inst_5 : d'.IsUltra
x y z : X
⊢ LE.le.{u_2} (α := R) ((d : (a : X) → X → R) x z ⊔ (d' : (a : X) → X → R) x z : R)
    ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y ⊔ ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z) :
      R)
have calc : LE.le.{u_2} (α := R)
  ((d : (a : X) → X → R) x y ⊔ (d : (a : X) → X → R) y z ⊔ ((d' : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) y z) :
    R)
  ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y ⊔ ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z) :
    R)
Tactic: calc d x z ⊔ d' x z ≤ d x y ⊔ d y z ⊔ (d' x y ⊔ d' y z) := sup_le_sup le_sup le_sup
  _ ≤ d x y ⊔ d' x y ⊔ (d y z ⊔ d' y z) := by simp [sup_comm, sup_left_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
⊢ (s.sup f).IsUltra
have le_sup' : ∀ (x y z : X),
  LE.le.{u_2} (α := R) ((s.sup f : (a : X) → X → R) x z : R)
    (max ((s.sup f : (a : X) → X → R) x y) ((s.sup f : (a : X) → X → R) y z) : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
⊢ LE.le.{u_2} (α := R) ((s.sup f : (a : X) → X → R) x z : R)
    (max ((s.sup f : (a : X) → X → R) x y) ((s.sup f : (a : X) → X → R) y z) : R)
have le_sup' : ∀ (h : ∀ (d : Y), Membership.mem (γ := Finset Y) ∅ d → (f d).IsUltra),
  LE.le.{u_2} (α := R) ((Finset.sup ∅ f : (a : X) → X → R) x z : R)
    (max ((Finset.sup ∅ f : (a : X) → X → R) x y) ((Finset.sup ∅ f : (a : X) → X → R) y z) : R)
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
le_sup' :
  ∀ (h : ∀ (d : Y), Membership.mem (γ := Finset Y) ∅ d → (f d).IsUltra),
    LE.le.{u_2} (α := R) ((Finset.sup ∅ f : (a : X) → X → R) x z : R)
      (max ((Finset.sup ∅ f : (a : X) → X → R) x y) ((Finset.sup ∅ f : (a : X) → X → R) y z) : R)
⊢ LE.le.{u_2} (α := R) ((s.sup f : (a : X) → X → R) x z : R)
    (max ((s.sup f : (a : X) → X → R) x y) ((s.sup f : (a : X) → X → R) y z) : R)
have le_sup'₁ : ∀ (hs : s.Nonempty),
  LE.le.{u_2} (α := R) ((s.sup f : (a : X) → X → R) x z : R)
    (max ((s.sup f : (a : X) → X → R) x y) ((s.sup f : (a : X) → X → R) y z) : R)
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
⊢ LE.le.{u_2} (α := R) ((s.sup f : (a : X) → X → R) x z : R)
    (max ((s.sup f : (a : X) → X → R) x y) ((s.sup f : (a : X) → X → R) y z) : R)
have le_sup' : LE.le.{u_2} (α := R) (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) x z)
  (max (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) x y) (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) y z))
Tactic: simp_rw [finsetSup_apply hs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
⊢ LE.le.{u_2} (α := R) (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) x z)
    (max (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) x y) (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) y z))
have le_sup' : ∀ b ∈ s,
  LE.le.{u_2} (α := R) ((f b : (a : X) → X → R) x z : R)
    (max (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) x y) (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) y z) :
      R)
Tactic: apply Finset.sup'_le
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
⊢ ∀ b ∈ s,
    LE.le.{u_2} (α := R) ((f b : (a : X) → X → R) x z : R)
      (max (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) x y) (s.sup' hs fun (i : Y) ↦ (f i : (a : X) → X → R) y z) :
        R)
have le_sup' : ∀ b ∈ s,
  (∃ b_1 ∈ s, LE.le.{u_2} (α := R) ((f b : (a : X) → X → R) x z : R) ((f b_1 : (a : X) → X → R) x y : R)) ∨
    ∃ b_1 ∈ s, LE.le.{u_2} (α := R) ((f b : (a : X) → X → R) x z : R) ((f b_1 : (a : X) → X → R) y z : R)
Tactic: simp only [le_sup_iff, Finset.le_sup'_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (hypothesis)
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
⊢ (∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) x y : R)) ∨
    ∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) y z : R)
have h₁ : LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R)
  (max ((f i : (a : X) → X → R) x y) ((f i : (a : X) → X → R) y z) : R)
Tactic: have h := (h i hi).le_sup' x y z
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (hypothesis)
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h_1 : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h :
  LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R)
    (max ((f i : (a : X) → X → R) x y) ((f i : (a : X) → X → R) y z) : R)
⊢ (∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) x y : R)) ∨
    ∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) y z : R)
have h₁ : LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) x y : R) ∨
  LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) y z : R)
Tactic: simp only [le_sup_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h_1 : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h :
  LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) x y : R) ∨
    LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) y z : R)
⊢ (∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) x y : R)) ∨
    ∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) y z : R)
have le_sup' : LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) x y : R) →
  ∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) x y : R)
Tactic: refine h.imp ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
Y : Type u_3
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h_1 : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h :
  LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) x y : R) ∨
    LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) y z : R)
le_sup' :
  LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) x y : R) →
    ∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) x y : R)
⊢ (∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) x y : R)) ∨
    ∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) y z : R)
have le_sup'₁ : LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f i : (a : X) → X → R) y z : R) →
  ∃ b ∈ s, LE.le.{u_2} (α := R) ((f i : (a : X) → X → R) x z : R) ((f b : (a : X) → X → R) y z : R)
Tactic: refine h.imp ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (hypothesis)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
n : ℕ
⊢ (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x ∈ A (res (↑x : ℕ → β) n)
have this : Membership.mem (γ := Set α) (⋂ (n : ℕ), A (res (↑x : ℕ → β) n))
  (Set.Nonempty.some (s := ⋂ (n : ℕ), A (res (↑x : ℕ → β) n)) sorry)
Tactic: have := x.property.some_mem
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (hypothesis)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
n : ℕ
this :
  Membership.mem (γ := Set α) (⋂ (n : ℕ), A (res (↑x : ℕ → β) n))
    (Set.Nonempty.some (s := ⋂ (n : ℕ), A (res (↑x : ℕ → β) n)) ⋯)
⊢ (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x ∈ A (res (↑x : ℕ → β) n)
have this₁ : ∀ (i : ℕ), Set.Nonempty.some (s := ⋂ (n : ℕ), A (res (↑x : ℕ → β) n)) sorry ∈ A (res (↑x : ℕ → β) i)
Tactic: rw [mem_iInter] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
⊢ x = y
have a : (↑x : ℕ → β) = (↑y : ℕ → β)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
⊢ (↑x : ℕ → β) = (↑y : ℕ → β)
have a : res (↑x : ℕ → β) = res (↑y : ℕ → β)
Tactic: apply res_injective
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
⊢ res (↑x : ℕ → β) = res (↑y : ℕ → β)
have a : ∀ (n : ℕ), res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
Tactic: ext n : 1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
⊢ res (↑x : ℕ → β) (n + 1) = res (↑y : ℕ → β) (n + 1)
have a : (↑x : ℕ → β) n = (↑y : ℕ → β) n ∧ res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
Tactic: simp only [res_succ, cons.injEq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
⊢ (↑x : ℕ → β) n = (↑y : ℕ → β) n ∧ res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
have a : (↑x : ℕ → β) n = (↑y : ℕ → β) n
Tactic: refine ⟨?_, ih⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
⊢ (↑x : ℕ → β) n = (↑y : ℕ → β) n
have a : ∀ (hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n), ¬CantorScheme.Disjoint A
Tactic: contrapose hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
⊢ ¬CantorScheme.Disjoint A
have a : ∃ (x : List β) (x_1 : β) (x_2 : β), ¬x_1 = x_2 ∧ ¬_root_.Disjoint (A (x_1 :: x)) (A (x_2 :: x))
Tactic: simp only [CantorScheme.Disjoint, _root_.Pairwise, Ne, not_forall, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
x y : (↑((inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)) : Type u_1)
hxy :
  (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) x =
    (inducedMap A).snd (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) y
n : ℕ
ih : res (↑x : ℕ → β) n = res (↑y : ℕ → β) n
hA : ¬(↑x : ℕ → β) n = (↑y : ℕ → β) n
⊢ ∃ (x : List β) (x_1 : β) (x_2 : β), ¬x_1 = x_2 ∧ ¬_root_.Disjoint (A (x_1 :: x)) (A (x_2 :: x))
have a : ¬_root_.Disjoint (A ((↑x : ℕ → β) n :: res (↑x : ℕ → β) n)) (A ((↑y : ℕ → β) n :: res (↑x : ℕ → β) n))
Tactic: refine ⟨res x n, _, _, hA, ?_⟩