awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
rw : dist x y - s * dist x y
| t * dist x y

Tactic:
rw [eq_sub_iff_add_eq'.mpr h, sub_mul, one_mul]

Premises used: Iff.mpr, eq_sub_iff_add_eq', sub_mul, one_mul
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
conv_lhs : dist x y - s * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
⊢ t * dist x y ≤ dist (convexCombPair s t hs ht h x y) x

Tactic:
conv_lhs => rw [eq_sub_iff_add_eq'.mpr h, sub_mul, one_mul]

Premises used: Iff.mpr, eq_sub_iff_add_eq', sub_mul, one_mul
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
grw : dist x y ≤ dist (convexCombPair s t hs ht h x y) x + s * dist x y
grw₁ : dist y x ≤ dist (convexCombPair s t hs ht h x y) x + s * dist y x
grw₂ : dist y x ≤ dist (convexCombPair s t hs ht h x y) x + dist (convexCombPair t s ht hs ⋯ y x) y
grw₃ : dist x y ≤ dist (convexCombPair s t hs ht h x y) x + dist (convexCombPair t s ht hs ⋯ y x) y
grw₄ : dist x y ≤ dist (convexCombPair t s ht hs ⋯ y x) x + dist (convexCombPair t s ht hs ⋯ y x) y
grw₅ grw₆ : dist x y ≤ dist x y
⊢ dist x y - s * dist x y ≤ dist (convexCombPair s t hs ht h x y) x

Tactic:
grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]

Premises used: sub_le_iff_le_add, Convexity.convexCombPair_symm, dist_triangle_left, dist_comm, add_comm, Eq.trans
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
suffices :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
⊢ dist (convexCombPair s t hs ht h x y) x = t * dist x y

Tactic:
suffices H : ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
      dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y by
    refine (H ..).antisymm ?_
    conv_lhs => rw [eq_sub_iff_add_eq'.mpr h, sub_mul, one_mul]
    grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s_1 t_1 : ℝ
hs_1 : 0 ≤ s_1
ht_1 : 0 ≤ t_1
h_1 : s_1 + t_1 = 1
x_1 y_1 : X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
grw : (iConvexComb (StdSimplex.duple x y hs ht h) fun (x_2 : X) ↦ dist x_2 x) ≤ t * dist x y
⊢ dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y

Tactic:
grw [convexCombPair, dist_sConvexComb_left_le]

Premises used: Convexity.dist_sConvexComb_left_le, Convexity.convexCombPair
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s_1 t_1 : ℝ
hs_1 : 0 ≤ s_1
ht_1 : 0 ≤ t_1
h_1 : s_1 + t_1 = 1
x_1 y_1 : X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ (iConvexComb (StdSimplex.duple x y hs ht h) fun (x_2 : X) ↦ dist x_2 x) ≤ t * dist x y

Tactic:
simp [iConvexComb_eq_sum, Finsupp.sum_add_index, add_mul, dist_comm y x]

Premises used: add_mul, Convexity.iConvexComb_eq_sum, dist_comm, Finsupp.sum_add_index
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
suffices suffices₁ suffices₂ suffices₃ :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
suffices₄ :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    (iConvexComb (StdSimplex.duple x y hs ht h) fun (x_1 : X) ↦ dist x_1 x) ≤ t * dist x y
⊢ dist (convexCombPair s t hs ht h x y) x = t * dist x y

Tactic:
classical
  suffices H : ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
      dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y by
    refine (H ..).antisymm ?_
    conv_lhs => rw [eq_sub_iff_add_eq'.mpr h, sub_mul, one_mul]
    grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]
  intro s t hs ht h x y
  grw [convexCombPair, dist_sConvexComb_left_le]
  simp [iConvexComb_eq_sum, Finsupp.sum_add_index, add_mul, dist_comm y x]

Premises used: add_mul, Convexity.iConvexComb_eq_sum, Convexity.dist_sConvexComb_left_le, dist_comm, Finsupp.sum_add_index, Convexity.convexCombPair
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
rw₂ rw₃ : s * dist x y = s * dist x y
⊢ dist (convexCombPair s t hs ht h x y) y = s * dist x y

Tactic:
rw [convexCombPair_symm, dist_convexCombPair_left, dist_comm]

Premises used: Convexity.convexCombPair_symm, dist_comm, Convexity.dist_convexCombPair_left
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
rw₁ rw₂ : t * dist x y = t * dist x y
⊢ dist x (convexCombPair s t hs ht h x y) = t * dist x y

Tactic:
rw [dist_comm, dist_convexCombPair_left]

Premises used: dist_comm, Convexity.dist_convexCombPair_left
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
rw₁ rw₂ : s * dist x y = s * dist x y
⊢ dist y (convexCombPair s t hs ht h x y) = s * dist x y

Tactic:
rw [dist_comm, dist_convexCombPair_right]

Premises used: dist_comm, Convexity.dist_convexCombPair_right
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
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
⊢ 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'
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
inr : 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:
rw [dist_comm, this, abs_sub_comm]

Premises used: dist_comm, abs_sub_comm
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
⊢ s ≤ s'

Tactic:
le_of_not_ge hss'

Premises used: le_of_not_ge
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
⊢ s ≤ s'

Tactic:
exact le_of_not_ge hss'

Premises used: le_of_not_ge
-- Module: Mathlib.Analysis.Convex.MetricSpace
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

Tactic:
this.antisymm ?_

Premises used: LE.le.antisymm
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
refine : |s - s'| * dist x y ≤ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y)
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y

Tactic:
refine this.antisymm ?_

Premises used: LE.le.antisymm
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
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|
⊢ |s - s'| * dist x y ≤ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y)

Tactic:
nth_grw 2 [← abs_dist_sub_le (z := x)]

Premises used: abs_dist_sub_le
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
rw : |t - t'| = |1 - t - (1 - t')|
⊢ |t - t'| = |s - s'|

Tactic:
rw [eq_sub_iff_add_eq.mpr h, eq_sub_iff_add_eq.mpr h']

Premises used: Iff.mpr, eq_sub_iff_add_eq
-- Module: Mathlib.Analysis.Convex.MetricSpace
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'| = |1 - t - (1 - t')|

Tactic:
simp [abs_sub_comm t t']

Premises used: abs_sub_comm
-- Module: Mathlib.Analysis.Convex.MetricSpace
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'|

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']
-- Module: Mathlib.Analysis.Convex.MetricSpace
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_1 : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
this : |t - t'| = |s - s'|
⊢ |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:
simp [← sub_mul, this]

Premises used: sub_mul
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
suffices : 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

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]
-- Module: Mathlib.Analysis.Convex.MetricSpace
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, ⋯⟩) :
      ℝ)
2 :
  LE.le (α := ℝ) ((0 : (a : Fin 3) → ℝ) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : ℝ)
    ((((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t] : Fin 3 →₀ ℝ) :
          (a : Fin 3) → ℝ)
        ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      ℝ)
⊢ 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 :
      ℝ)

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
⊢ 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, ⋯⟩) :
      ℝ)

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
⊢ 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, ⋯⟩) :
      ℝ)

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
⊢ LE.le (α := ℝ) ((0 : (a : Fin 3) → ℝ) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : ℝ)
    ((((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t] : Fin 3 →₀ ℝ) :
          (a : Fin 3) → ℝ)
        ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      ℝ)

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
⊢ Eq (α := ℝ)
    (Finsupp.sum ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin 3 → ℝ) → Fin 3 →₀ ℝ) ![s', s - s', t])
      fun (x : Fin 3) (r : ℝ) ↦ r)
    1

Tactic:
simp [Finsupp.sum_fintype, Fin.sum_univ_succ, ← add_assoc, h]

Premises used: add_assoc, Finsupp.sum_fintype, Fin.sum_univ_succ
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y]) ≤
    iConvexComb f fun (i : Fin 3) ↦ dist (![x, x, y] i) (![x, y, y] i)

Tactic:
dist_iConvexComb_le f ![x, x, y] ![x, y, y]

Premises used: Convexity.dist_iConvexComb_le, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.Analysis.Convex.MetricSpace
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])
h₂ : |s - s'| * dist x y = iConvexComb f fun (i : Fin 3) ↦ dist (![x, x, y] i) (![x, y, y] i)
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y

Tactic:
convert dist_iConvexComb_le f ![x, x, y] ![x, y, y] using 1

Premises used: Convexity.dist_iConvexComb_le, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 := ⋯ }
⊢ |s - s'| * dist x y = iConvexComb f fun (i : Fin 3) ↦ dist (![x, x, y] i) (![x, y, y] i)

Tactic:
simp [Finsupp.sum_fintype, Fin.sum_univ_succ, f, hss', iConvexComb_eq_sum]

Premises used: Convexity.iConvexComb_eq_sum, Finsupp.sum_fintype, Fin.sum_univ_succ
-- Module: Mathlib.Analysis.Convex.MetricSpace
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]
h₂ : convexCombPair s' t' hs' ht' h' x y = iConvexComb f ![x, y, 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])

Tactic:
congr 1
-- Module: Mathlib.Analysis.Convex.MetricSpace
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₁ : sConvexComb (StdSimplex.duple x y hs ht h) = iConvexComb f ![x, x, y]
⊢ convexCombPair s t hs ht h x y = iConvexComb f ![x, x, y]

Tactic:
delta convexCombPair

Premises used: Convexity.convexCombPair
-- Module: Mathlib.Analysis.Convex.MetricSpace
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₁ : StdSimplex.duple x y hs ht h = StdSimplex.map ![x, x, y] f
⊢ sConvexComb (StdSimplex.duple x y hs ht h) = iConvexComb f ![x, x, y]

Tactic:
congr 1
-- Module: Mathlib.Analysis.Convex.MetricSpace
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₁ :
  ∀ (a : X),
    Eq (α := ℝ) (((StdSimplex.duple x y hs ht h).weights : (a : X) → ℝ) a : ℝ)
      (((StdSimplex.map ![x, x, y] f).weights : (a : X) → ℝ) a : ℝ)
⊢ StdSimplex.duple x y hs ht h = StdSimplex.map ![x, x, y] f

Tactic:
ext a
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 := ⋯ }
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:
simp [StdSimplex.duple, StdSimplex.map, Finsupp.mapDomain,
      Finsupp.sum_fintype, Fin.sum_univ_succ, f, ← add_assoc]

Premises used: add_assoc, Finsupp.mapDomain, Finsupp.sum_fintype, Convexity.StdSimplex.duple, Convexity.StdSimplex.map, Fin.sum_univ_succ
-- Module: Mathlib.Analysis.Convex.MetricSpace
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₁ : sConvexComb (StdSimplex.duple x y hs' ht' h') = iConvexComb f ![x, y, y]
⊢ convexCombPair s' t' hs' ht' h' x y = iConvexComb f ![x, y, y]

Tactic:
delta convexCombPair

Premises used: Convexity.convexCombPair
-- Module: Mathlib.Analysis.Convex.MetricSpace
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₁ : StdSimplex.duple x y hs' ht' h' = StdSimplex.map ![x, y, y] f
⊢ sConvexComb (StdSimplex.duple x y hs' ht' h') = iConvexComb f ![x, y, y]

Tactic:
congr 1