awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
⊢ (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)

Tactic:
⟨(d.triangle x y z).trans ?_, (d'.triangle x y z).trans ?_⟩

Premises used: PseudoMetric.triangle, And.intro, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
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)
⊢ (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)

Tactic:
refine ⟨(d.triangle x y z).trans ?_, (d'.triangle x y z).trans ?_⟩
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
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)
⊢ 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:
apply add_le_add

Premises used: add_le_add
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
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)
⊢ 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:
apply add_le_add

Premises used: add_le_add
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
⊢ 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:
simp
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
⊢ 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:
simp
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
⊢ 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:
simp
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
⊢ 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:
simp
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
⊢ Eq (α := (a : X) → X → R) (⇑(d ⊔ d') : (a : X) → X → R) ((⇑d : (a : X) → X → R) ⊔ (⇑d' : (a : X) → X → R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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 : X
⊢ Eq.{u_2 + 1} (α := R) ((d ⊔ d' : (a : X) → X → R) x y : R)
    ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
⊢ ∀ (a b : PseudoMetric X R), a ≤ a ⊔ b

Tactic:
simp [← PseudoMetric.coe_le_coe]

Premises used: PseudoMetric.coe_le_coe
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
⊢ ∀ (a b : PseudoMetric X R), b ≤ a ⊔ b

Tactic:
simp [← PseudoMetric.coe_le_coe]

Premises used: PseudoMetric.coe_le_coe
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
by_contra! : ∀ (H : LT.lt.{u_2} (α := R) ((d : (a : X) → X → R) x y : R) (0 : R)), False
⊢ LE.le.{u_2} (α := R) (0 : R) ((d : (a : X) → X → R) x y : R)

Tactic:
by_contra! H
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
⊢ (d : (a : X) → X → R) x x ≤
    HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) y x : R)

Tactic:
d.triangle' x y x

Premises used: PseudoMetric.triangle'
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
⊢ 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:
add_lt_add H (d.symm x y ▸ H)

Premises used: Eq.rec, add_lt_add, PseudoMetric.symm
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
⊢ 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:
refine add_lt_add H (d.symm x y ▸ H)

Premises used: add_lt_add
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
⊢ HAdd.hAdd (α := R) 0 0 = 0

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
calc₁ : HAdd.hAdd (α := R) 0 0 = 0
⊢ LT.lt.{u_2} (α := R) ((d : (a : X) → X → R) x x : R) (0 : R)

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

Premises used: PseudoMetric.triangle', DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)

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
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
this : LT.lt.{u_2} (α := R) ((d : (a : X) → X → R) x x : R) (0 : R)
⊢ False

Tactic:
this.ne (d.refl x)

Premises used: PseudoMetric.refl, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
this : LT.lt.{u_2} (α := R) ((d : (a : X) → X → R) x x : R) (0 : R)
⊢ False

Tactic:
exact this.ne (d.refl x)

Premises used: PseudoMetric.refl, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
⊢ Eq (α := (a : X) → X → R) (⇑(s.sup f) : (a : X) → X → R) (⇑(s.sup' hs fun (x : Y) ↦ f x) : (a : X) → X → R)

Tactic:
simpa using (Finset.sup'_eq_sup hs (f ·)).symm

Premises used: Eq.symm, Finset.sup'_eq_sup
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
x y : X
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)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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_1 : Finset Y
x y : X
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' ⋯ fun (i : Y) ↦ (f i : (a : X) → X → R) x y : R)

Tactic:
simp [hs, ih]
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
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' ⋯ 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)

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton i => simp
  | cons a s ha hs ih => simp [hs, ih]

Premises used: Singleton.singleton
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : Add R
inst_2 : LE R
inst_3 : Max R
d : PseudoMetric X R
hd : d.IsUltra
x y z : X
⊢ LE.le.{u_2} (α := R) ((d : (a : X) → X → R) x z : R) ((d : (a : X) → X → R) x y ⊔ (d : (a : X) → X → R) y z : R)

Tactic:
hd.le_sup' x y z

Premises used: PseudoMetric.IsUltra.le_sup'
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
⊢ ∀ (x y z : X),
    LE.le.{u_2} (α := R) ((⊥ : (a : X) → X → R) x z : R) ((⊥ : (a : X) → X → R) x y ⊔ (⊥ : (a : X) → X → R) y z : R)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
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)
⊢ (d ⊔ d').IsUltra

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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_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)
⊢ 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:
simp only [PseudoMetric.sup_apply]

Premises used: PseudoMetric.sup_apply
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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) y z ⊔ ((d' : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) y z) :
      R)

Tactic:
sup_le_sup le_sup le_sup

Premises used: sup_le_sup, PseudoMetric.IsUltra.le_sup
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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 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:
simp [sup_comm, sup_left_comm]

Premises used: sup_comm, sup_left_comm
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
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)
⊢ 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:
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]

Premises used: sup_le_sup, PseudoMetric.IsUltra.le_sup, Max.max, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
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)
⊢ (s.sup f).IsUltra

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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_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)
⊢ 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

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
x y z : X
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:
simp
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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_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))
⊢ 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:
simp_rw [finsetSup_apply hs]

Premises used: PseudoMetric.finsetSup_apply
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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_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)
⊢ 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:
apply Finset.sup'_le

Premises used: Finset.sup'_le
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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_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)
⊢ ∀ 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:
simp only [le_sup_iff, Finset.le_sup'_iff]

Premises used: Finset.le_sup'_iff, le_sup_iff
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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
⊢ 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
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
⊢ 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

Premises used: le_sup_iff
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)

Tactic:
h.imp ?_ ?_

Premises used: Or.imp
-- Module: Mathlib.Topology.MetricSpace.BundledFun
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)
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)
⊢ (∃ 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)

Tactic:
refine h.imp ?_ ?_

Premises used: Or.imp