awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ dist (convexCombPair s t hs ht h x y) y = s * dist x y
have rw : dist (convexCombPair t s ht hs sorry y x) y = s * dist x y
Tactic: rw [convexCombPair_symm, dist_convexCombPair_left, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
rw : dist (convexCombPair t s ht hs ⋯ y x) y = s * dist x y
⊢ dist (convexCombPair s t hs ht h x y) y = s * dist x y
have rw₁ : s * dist y x = s * dist x y
Tactic: rw [convexCombPair_symm, dist_convexCombPair_left, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
rw : dist (convexCombPair t s ht hs ⋯ y x) y = s * dist x y
rw₁ : s * dist y x = s * dist x y
⊢ dist (convexCombPair s t hs ht h x y) y = s * dist x y
have rw₂ : s * dist x y = s * dist x y
Tactic: rw [convexCombPair_symm, dist_convexCombPair_left, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ dist x (convexCombPair s t hs ht h x y) = t * dist x y
have rw : dist (convexCombPair s t hs ht h x y) x = t * dist x y
Tactic: rw [dist_comm, dist_convexCombPair_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
rw : dist (convexCombPair s t hs ht h x y) x = t * dist x y
⊢ dist x (convexCombPair s t hs ht h x y) = t * dist x y
have rw₁ : t * dist x y = t * dist x y
Tactic: rw [dist_comm, dist_convexCombPair_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ dist y (convexCombPair s t hs ht h x y) = s * dist x y
have rw : dist (convexCombPair s t hs ht h x y) y = s * dist x y
Tactic: rw [dist_comm, dist_convexCombPair_right]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
rw : dist (convexCombPair s t hs ht h x y) y = s * dist x y
⊢ dist y (convexCombPair s t hs ht h x y) = s * dist x y
have rw₁ : s * dist x y = s * dist x y
Tactic: rw [dist_comm, dist_convexCombPair_right]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
x y : X
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
have inr : ∀
  (this :
    ∀ {s t s' t' : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1)
      (hss' : s' ≤ s),
      dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y)
  (hss' : ¬s' ≤ s), dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
Tactic: wlog hss' : s' ≤ s generalizing s t s' t'
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
x y : X
inr :
  ∀
    (this :
      ∀ {s t s' t' : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1)
        (hss' : s' ≤ s),
        dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y)
    (hss' : ¬s' ≤ s), dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
have wlog : ∀ {s t s' t' : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1)
  (hss' : s' ≤ s), dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
Tactic: wlog hss' : s' ≤ s generalizing s t s' t'
Cleared hypotheses: s, t, s', t', hs, ht, h, hs', ht', h'
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
x y : X
this :
  ∀ {s t s' t' : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1)
    (hss' : s' ≤ s), dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
hss' : ¬s' ≤ s
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
have inr : s ≤ s'
Tactic: rw [dist_comm, this, abs_sub_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
this : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
have refine : |s - s'| * dist x y ≤ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y)
Tactic: refine this.antisymm ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
this : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
⊢ |s - s'| * dist x y ≤ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y)
have nth_grw : |s - s'| * dist x y ≤ |dist (convexCombPair s t hs ht h x y) x - dist (convexCombPair s' t' hs' ht' h' x y) x|
Tactic: nth_grw 2 [← abs_dist_sub_le (z := x)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
this : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
⊢ |t - t'| = |s - s'|
have rw : |t - t'| = |1 - t - (1 - t')|
Tactic: rw [eq_sub_iff_add_eq.mpr h, eq_sub_iff_add_eq.mpr h']
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (hypothesis)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
this : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
⊢ |s - s'| * dist x y ≤ |dist (convexCombPair s t hs ht h x y) x - dist (convexCombPair s' t' hs' ht' h' x y) x|
have this₁ : |t - t'| = |s - s'|
Tactic: have : |t - t'| = |s - s'| := by
      rw [eq_sub_iff_add_eq.mpr h, eq_sub_iff_add_eq.mpr h']; simp [abs_sub_comm t t']
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
have suffices : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
Tactic: suffices dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤
      |s - s'| * dist x y by
    refine this.antisymm ?_
    nth_grw 2 [← abs_dist_sub_le (z := x)]
    have : |t - t'| = |s - s'| := by
      rw [eq_sub_iff_add_eq.mpr h, eq_sub_iff_add_eq.mpr h']; simp [abs_sub_comm t t']
    simp [← sub_mul, this]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
i : Fin 3
⊢ LE.le (α := ℝ) ((0 : (a : Fin 3) → ℝ) i : ℝ)
    ((((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t] : Fin 3 →₀ ℝ) :
          (a : Fin 3) → ℝ)
        i :
      ℝ)
have 0 : LE.le (α := ℝ) ((0 : (a : Fin 3) → ℝ) ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) : ℝ)
  ((((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t] : Fin 3 →₀ ℝ) :
        (a : Fin 3) → ℝ)
      ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) :
    ℝ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
i : Fin 3
0 :
  LE.le (α := ℝ) ((0 : (a : Fin 3) → ℝ) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : ℝ)
    ((((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t] : Fin 3 →₀ ℝ) :
          (a : Fin 3) → ℝ)
        ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
⊢ LE.le (α := ℝ) ((0 : (a : Fin 3) → ℝ) i : ℝ)
    ((((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t] : Fin 3 →₀ ℝ) :
          (a : Fin 3) → ℝ)
        i :
      ℝ)
have 1 : LE.le (α := ℝ) ((0 : (a : Fin 3) → ℝ) ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩) : ℝ)
  ((((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t] : Fin 3 →₀ ℝ) :
        (a : Fin 3) → ℝ)
      ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩) :
    ℝ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
i : Fin 3
0 :
  LE.le (α := ℝ) ((0 : (a : Fin 3) → ℝ) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : ℝ)
    ((((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t] : Fin 3 →₀ ℝ) :
          (a : Fin 3) → ℝ)
        ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
1 :
  LE.le (α := ℝ) ((0 : (a : Fin 3) → ℝ) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : ℝ)
    ((((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t] : Fin 3 →₀ ℝ) :
          (a : Fin 3) → ℝ)
        ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
⊢ LE.le (α := ℝ) ((0 : (a : Fin 3) → ℝ) i : ℝ)
    ((((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t] : Fin 3 →₀ ℝ) :
          (a : Fin 3) → ℝ)
        i :
      ℝ)
have 2 : LE.le (α := ℝ) ((0 : (a : Fin 3) → ℝ) ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩) : ℝ)
  ((((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t] : Fin 3 →₀ ℝ) :
        (a : Fin 3) → ℝ)
      ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩) :
    ℝ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) :=
  { weights := (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t], nonneg := ⋯,
    total := ⋯ }
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
have h₁ : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) =
  dist (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y])
Tactic: convert dist_iConvexComb_le f ![x, x, y] ![x, y, y] using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) :=
  { weights := (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t], nonneg := ⋯,
    total := ⋯ }
h₁ :
  dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) =
    dist (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y])
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
have h₂ : |s - s'| * dist x y = iConvexComb f fun (i : Fin 3) ↦ dist (![x, x, y] i) (![x, y, y] i)
Tactic: convert dist_iConvexComb_le f ![x, x, y] ![x, y, y] using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) :=
  { weights := (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t], nonneg := ⋯,
    total := ⋯ }
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) =
    dist (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y])
have h₁ : convexCombPair s t hs ht h x y = iConvexComb f ![x, x, y]
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) :=
  { weights := (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t], nonneg := ⋯,
    total := ⋯ }
h₁ : convexCombPair s t hs ht h x y = iConvexComb f ![x, x, y]
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) =
    dist (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y])
have h₂ : convexCombPair s' t' hs' ht' h' x y = iConvexComb f ![x, y, y]
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) :=
  { weights := (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t], nonneg := ⋯,
    total := ⋯ }
⊢ convexCombPair s t hs ht h x y = iConvexComb f ![x, x, y]
have h₁ : sConvexComb (StdSimplex.duple x y hs ht h) = iConvexComb f ![x, x, y]
Tactic: delta convexCombPair
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) :=
  { weights := (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t], nonneg := ⋯,
    total := ⋯ }
⊢ sConvexComb (StdSimplex.duple x y hs ht h) = iConvexComb f ![x, x, y]
have h₁ : StdSimplex.duple x y hs ht h = StdSimplex.map ![x, x, y] f
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) :=
  { weights := (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t], nonneg := ⋯,
    total := ⋯ }
⊢ StdSimplex.duple x y hs ht h = StdSimplex.map ![x, x, y] f
have h₁ : ∀ (a : X),
  Eq (α := ℝ) (((StdSimplex.duple x y hs ht h).weights : (a : X) → ℝ) a : ℝ)
    (((StdSimplex.map ![x, x, y] f).weights : (a : X) → ℝ) a : ℝ)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) :=
  { weights := (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t], nonneg := ⋯,
    total := ⋯ }
⊢ convexCombPair s' t' hs' ht' h' x y = iConvexComb f ![x, y, y]
have h₁ : sConvexComb (StdSimplex.duple x y hs' ht' h') = iConvexComb f ![x, y, y]
Tactic: delta convexCombPair
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) :=
  { weights := (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t], nonneg := ⋯,
    total := ⋯ }
⊢ sConvexComb (StdSimplex.duple x y hs' ht' h') = iConvexComb f ![x, y, y]
have h₁ : StdSimplex.duple x y hs' ht' h' = StdSimplex.map ![x, y, y] f
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) :=
  { weights := (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t], nonneg := ⋯,
    total := ⋯ }
⊢ StdSimplex.duple x y hs' ht' h' = StdSimplex.map ![x, y, y] f
have h₁ : ∀ (a : X),
  Eq (α := ℝ) (((StdSimplex.duple x y hs' ht' h').weights : (a : X) → ℝ) a : ℝ)
    (((StdSimplex.map ![x, y, y] f).weights : (a : X) → ℝ) a : ℝ)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y x' y' : X
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s t hs ht h x' y') ≤ s * dist x x' + t * dist y y'
have h₁ : convexCombPair s t hs ht h x y = iConvexComb (StdSimplex.duple 0 1 hs ht h) ![x, y]
Tactic: convert dist_iConvexComb_le (.duple (M := Fin 2) 0 1 hs ht h) ![x, y] ![x', y']
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y x' y' : X
h₁ : convexCombPair s t hs ht h x y = iConvexComb (StdSimplex.duple 0 1 hs ht h) ![x, y]
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s t hs ht h x' y') ≤ s * dist x x' + t * dist y y'
have h₂ : convexCombPair s t hs ht h x' y' = iConvexComb (StdSimplex.duple 0 1 hs ht h) ![x', y']
Tactic: convert dist_iConvexComb_le (.duple (M := Fin 2) 0 1 hs ht h) ![x, y] ![x', y']
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y x' y' : X
h₁ : convexCombPair s t hs ht h x y = iConvexComb (StdSimplex.duple 0 1 hs ht h) ![x, y]
h₂ : convexCombPair s t hs ht h x' y' = iConvexComb (StdSimplex.duple 0 1 hs ht h) ![x', y']
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s t hs ht h x' y') ≤ s * dist x x' + t * dist y y'
have h₃ : s * dist x x' + t * dist y y' =
  iConvexComb (StdSimplex.duple 0 1 hs ht h) fun (i : Fin 2) ↦ dist (![x, y] i) (![x', y'] i)
Tactic: convert dist_iConvexComb_le (.duple (M := Fin 2) 0 1 hs ht h) ![x, y] ![x', y']
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
⊢ Continuous (Y := X) fun (x : (↑(Set.Icc 0 1) : Type) × X × X) ↦
    convexCombPair (↑x.1 : ℝ) (1 - (↑x.1 : ℝ)) ⋯ ⋯ ⋯ x.2.1 x.2.2
have ha : ∀ (a : (↑(Set.Icc 0 1) : Type)),
  LipschitzWith (β := X) 1 fun (y : X × X) ↦
    convexCombPair (↑(a, y).1 : ℝ) (1 - (↑(a, y).1 : ℝ)) sorry sorry sorry (a, y).2.1 (a, y).2.2
Tactic: apply continuous_prod_of_continuous_lipschitzWith' (K := 1)
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
ha :
  ∀ (a : (↑(Set.Icc 0 1) : Type)),
    LipschitzWith (β := X) 1 fun (y : X × X) ↦
      convexCombPair (↑(a, y).1 : ℝ) (1 - (↑(a, y).1 : ℝ)) ⋯ ⋯ ⋯ (a, y).2.1 (a, y).2.2
⊢ Continuous (Y := X) fun (x : (↑(Set.Icc 0 1) : Type) × X × X) ↦
    convexCombPair (↑x.1 : ℝ) (1 - (↑x.1 : ℝ)) ⋯ ⋯ ⋯ x.2.1 x.2.2
have hb : ∀ (b : X × X),
  Continuous.{0, u_2} (Y := X) fun (x : (↑(Set.Icc 0 1) : Type)) ↦
    convexCombPair (↑(x, b).1 : ℝ) (1 - (↑(x, b).1 : ℝ)) sorry sorry sorry (x, b).2.1 (x, b).2.2
Tactic: apply continuous_prod_of_continuous_lipschitzWith' (K := 1)
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
i : (↑(Set.Icc 0 1) : Type)
x y : X × X
⊢ edist.{u_2} (α := X)
      ((fun (y : X × X) ↦ convexCombPair (↑(i, y).1 : ℝ) (1 - (↑(i, y).1 : ℝ)) ⋯ ⋯ ⋯ (i, y).2.1 (i, y).2.2) x)
      ((fun (y : X × X) ↦ convexCombPair (↑(i, y).1 : ℝ) (1 - (↑(i, y).1 : ℝ)) ⋯ ⋯ ⋯ (i, y).2.1 (i, y).2.2) y) ≤
    (↑1 : ENNReal) * edist x y
have ha : dist (convexCombPair (↑i : ℝ) (1 - (↑i : ℝ)) sorry sorry sorry x.1 x.2) (convexCombPair (↑i : ℝ) (1 - (↑i : ℝ)) sorry sorry sorry y.1 y.2) ≤
  dist x y
Tactic: simp only [← coe_nnreal_ennreal_nndist, ENNReal.coe_one, one_mul, ENNReal.coe_le_coe,
      NNReal.toReal_le, coe_nndist]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
i : (↑(Set.Icc 0 1) : Type)
x y : X × X
⊢ dist (convexCombPair (↑i : ℝ) (1 - (↑i : ℝ)) ⋯ ⋯ ⋯ x.1 x.2) (convexCombPair (↑i : ℝ) (1 - (↑i : ℝ)) ⋯ ⋯ ⋯ y.1 y.2) ≤
    dist x y
have ha : (↑i : ℝ) * dist x.1 y.1 + (1 - (↑i : ℝ)) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)
Tactic: grw [dist_convexCombPair_convexCombPair_le, Prod.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
i : (↑(Set.Icc 0 1) : Type)
x y : X × X
⊢ (↑i : ℝ) * dist x.1 y.1 + (1 - (↑i : ℝ)) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)
have ha : (↑i : ℝ) * max (dist x.1 y.1) (dist x.2 y.2) + (1 - (↑i : ℝ)) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)
Tactic: nth_grw 1 [le_max_left (dist x.1 y.1) (dist x.2 y.2)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
i : (↑(Set.Icc 0 1) : Type)
x y : X × X
ha : (↑i : ℝ) * max (dist x.1 y.1) (dist x.2 y.2) + (1 - (↑i : ℝ)) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)
⊢ (↑i : ℝ) * dist x.1 y.1 + (1 - (↑i : ℝ)) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)
have h₁ : 0 ≤ (↑i : ℝ)
Tactic: nth_grw 1 [le_max_left (dist x.1 y.1) (dist x.2 y.2)]