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
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, y, y] f).weights : (a : X) → ℝ) a : ℝ)
⊢ StdSimplex.duple x y hs' ht' h' = StdSimplex.map ![x, y, 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
⊢ t' = s - s' + t

Tactic:
grind
-- 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, y, y] f).weights : (a : X) → ℝ) a : ℝ)

Tactic:
simp [StdSimplex.duple, StdSimplex.map, Finsupp.mapDomain,
      Finsupp.sum_fintype, Fin.sum_univ_succ, f, show t' = s - s' + t by grind]

Premises used: 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
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y x' y' : X
⊢ dist (iConvexComb (StdSimplex.duple 0 1 hs ht h) ![x, y]) (iConvexComb (StdSimplex.duple 0 1 hs ht h) ![x', y']) ≤
    iConvexComb (StdSimplex.duple 0 1 hs ht h) fun (i : Fin 2) ↦ dist (![x, y] i) (![x', y'] i)

Tactic:
dist_iConvexComb_le (.duple (M := Fin 2) 0 1 hs ht h) ![x, y] ![x', y']

Premises used: Convexity.dist_iConvexComb_le, Convexity.StdSimplex.duple, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- 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' 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']
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)
⊢ 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'

Tactic:
convert dist_iConvexComb_le (.duple (M := Fin 2) 0 1 hs ht h) ![x, y] ![x', y']

Premises used: Convexity.dist_iConvexComb_le, Convexity.StdSimplex.duple, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- 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' y' : X
⊢ convexCombPair s t hs ht h x y = iConvexComb (StdSimplex.duple 0 1 hs ht h) ![x, y]

Tactic:
simp [convexCombPair_def]

Premises used: Convexity.convexCombPair_def
-- 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' y' : X
⊢ convexCombPair s t hs ht h x' y' = iConvexComb (StdSimplex.duple 0 1 hs ht h) ![x', y']

Tactic:
simp [convexCombPair_def]

Premises used: Convexity.convexCombPair_def
-- 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' y' : X
⊢ 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:
simp [Finsupp.sum_fintype, Fin.sum_univ_succ, StdSimplex.duple, iConvexComb_eq_sum]

Premises used: Convexity.iConvexComb_eq_sum, Finsupp.sum_fintype, Convexity.StdSimplex.duple, Fin.sum_univ_succ
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x : (↑(Set.Icc 0 1) : Type) × X × X
⊢ 0 ≤ 1 - (↑x.1 : ℝ)

Tactic:
simpa using x.1.prop.right

Premises used: Prod.fst, And.right, Subtype.prop
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
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 : ℝ)) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).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

Tactic:
apply continuous_prod_of_continuous_lipschitzWith' (K := 1)

Premises used: OfNat.ofNat, continuous_prod_of_continuous_lipschitzWith'
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 :
  dist (convexCombPair (↑i : ℝ) (1 - (↑i : ℝ)) ⋯ ⋯ ⋯ x.1 x.2) (convexCombPair (↑i : ℝ) (1 - (↑i : ℝ)) ⋯ ⋯ ⋯ y.1 y.2) ≤
    dist x y
⊢ 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

Tactic:
simp only [← coe_nnreal_ennreal_nndist, ENNReal.coe_one, one_mul, ENNReal.coe_le_coe,
      NNReal.toReal_le, coe_nndist]

Premises used: coe_nndist, ENNReal.coe_le_coe, coe_nnreal_ennreal_nndist, ENNReal.coe_one, NNReal.toReal_le, one_mul
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 : ℝ) * dist x.1 y.1 + (1 - (↑i : ℝ)) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)
⊢ dist (convexCombPair (↑i : ℝ) (1 - (↑i : ℝ)) ⋯ ⋯ ⋯ x.1 x.2) (convexCombPair (↑i : ℝ) (1 - (↑i : ℝ)) ⋯ ⋯ ⋯ y.1 y.2) ≤
    dist x y

Tactic:
grw [dist_convexCombPair_convexCombPair_le, Prod.dist_eq]

Premises used: Prod.dist_eq, Convexity.dist_convexCombPair_convexCombPair_le
-- Module: Mathlib.Analysis.Convex.MetricSpace
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)
h₁ : 0 ≤ (↑i : ℝ)
⊢ (↑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:
nth_grw 1 [le_max_left (dist x.1 y.1) (dist x.2 y.2)]

Premises used: Prod.fst, Dist.dist, le_max_left, Prod.snd
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
⊢ 0 ≤ (↑i : ℝ)

Tactic:
simpa using i.prop.left

Premises used: And.left, Subtype.prop
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 : ℝ)) * max (dist x.1 y.1) (dist x.2 y.2) ≤
    max (dist x.1 y.1) (dist x.2 y.2)
h₁ : 0 ≤ 1 - (↑i : ℝ)
⊢ (↑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 2 [le_max_right (dist x.1 y.1) (dist x.2 y.2)]

Premises used: le_max_right, Prod.fst, Dist.dist, Prod.snd
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
⊢ 0 ≤ 1 - (↑i : ℝ)

Tactic:
simpa using i.prop.right

Premises used: And.right, Subtype.prop
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 : ℝ) + (1 - (↑i : ℝ))) * max (dist x.1 y.1) (dist x.2 y.2) ≤ max (dist x.1 y.1) (dist x.2 y.2)
ha₁ : 1 * max (dist x.1 y.1) (dist x.2 y.2) ≤ max (dist x.1 y.1) (dist x.2 y.2)
ha₂ ha₃ : max (dist x.1 y.1) (dist x.2 y.2) ≤ max (dist x.1 y.1) (dist x.2 y.2)
⊢ (↑i : ℝ) * max (dist x.1 y.1) (dist x.2 y.2) + (1 - (↑i : ℝ)) * max (dist x.1 y.1) (dist x.2 y.2) ≤
    max (dist x.1 y.1) (dist x.2 y.2)

Tactic:
rw [← add_mul, add_sub_cancel, one_mul]

Premises used: add_mul, add_sub_cancel, one_mul
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
b : X × X
⊢ Continuous.{0, u_2} (Y := X) fun (x : (↑(Set.Icc 0 1) : Type)) ↦
    convexCombPair (↑(x, b).1 : ℝ) (1 - (↑(x, b).1 : ℝ)) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).2.2

Tactic:
LipschitzWith.continuous (K := nndist b.1 b.2) fun x y ↦ ?_

Premises used: LipschitzWith.continuous
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
b : X × X
hb :
  ∀ (x y : (↑(Set.Icc 0 1) : Type)),
    edist (convexCombPair (↑(x, b).1 : ℝ) (1 - (↑(x, b).1 : ℝ)) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).2.2)
        (convexCombPair (↑(y, b).1 : ℝ) (1 - (↑(y, b).1 : ℝ)) ⋯ ⋯ ⋯ (y, b).2.1 (y, b).2.2) ≤
      (↑(nndist b.1 b.2) : ENNReal) * edist x y
⊢ Continuous.{0, u_2} (Y := X) fun (x : (↑(Set.Icc 0 1) : Type)) ↦
    convexCombPair (↑(x, b).1 : ℝ) (1 - (↑(x, b).1 : ℝ)) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).2.2

Tactic:
refine LipschitzWith.continuous (K := nndist b.1 b.2) fun x y ↦ ?_

Premises used: LipschitzWith.continuous
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
b : X × X
x y : (↑(Set.Icc 0 1) : Type)
hb :
  edist (convexCombPair (↑(x, b).1 : ℝ) (1 - (↑(x, b).1 : ℝ)) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).2.2)
      (convexCombPair (↑(y, b).1 : ℝ) (1 - (↑(y, b).1 : ℝ)) ⋯ ⋯ ⋯ (y, b).2.1 (y, b).2.2) ≤
    edist x y * (↑(nndist b.1 b.2) : ENNReal)
⊢ edist (convexCombPair (↑(x, b).1 : ℝ) (1 - (↑(x, b).1 : ℝ)) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).2.2)
      (convexCombPair (↑(y, b).1 : ℝ) (1 - (↑(y, b).1 : ℝ)) ⋯ ⋯ ⋯ (y, b).2.1 (y, b).2.2) ≤
    (↑(nndist b.1 b.2) : ENNReal) * edist x y

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
b : X × X
x y : (↑(Set.Icc 0 1) : Type)
⊢ edist (convexCombPair (↑(x, b).1 : ℝ) (1 - (↑(x, b).1 : ℝ)) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).2.2)
      (convexCombPair (↑(y, b).1 : ℝ) (1 - (↑(y, b).1 : ℝ)) ⋯ ⋯ ⋯ (y, b).2.1 (y, b).2.2) ≤
    edist x y * (↑(nndist b.1 b.2) : ENNReal)

Tactic:
simp [← coe_nnreal_ennreal_nndist, ← ENNReal.coe_mul, NNReal.toReal_le,
      dist_convexCombPair_convexCombPair, Subtype.dist_eq, dist_eq_norm]

Premises used: dist_eq_norm, coe_nnreal_ennreal_nndist, Subtype.dist_eq, Convexity.dist_convexCombPair_convexCombPair, ENNReal.coe_mul, NNReal.toReal_le
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
i : T
⊢ 0 ≤ 1 - f i

Tactic:
simpa using hf1 _
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
obtain :
  ∀ (D : ℝ)
    (hD :
      ∀ ⦃x_1 : X⦄, x_1 ∈ Set.range x ∪ Set.range y → ∀ ⦃y_1 : X⦄, y_1 ∈ Set.range x ∪ Set.range y → dist x_1 y_1 ≤ D)
    (hD' : 0 < D), Continuous.{u_3, u_2} (Y := X) fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)
⊢ Continuous.{u_3, u_2} (Y := X) fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)

Tactic:
obtain ⟨D, hD, hD'⟩ := ((Metric.isBounded_iff_eventually.mp (hx'.union hy')).and
    (Filter.eventually_gt_atTop 0)).exists

Premises used: Metric.isBounded_iff_eventually, Filter.Eventually.and, Filter.Eventually.exists, Iff.mp, OfNat.ofNat, Bornology.IsBounded.union, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD : ∀ ⦃x_1 : X⦄, x_1 ∈ Set.range x ∪ Set.range y → ∀ ⦃y_1 : X⦄, y_1 ∈ Set.range x ∪ Set.range y → dist x_1 y_1 ≤ D
hD' : 0 < D
⊢ ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D

Tactic:
replace hD := fun t₁ t₂ ↦ hD (.inl (Set.mem_range_self t₁)) (.inr (Set.mem_range_self t₂))
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
rw : ∀ (x_1 : T), ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) x_1
⊢ Continuous.{u_3, u_2} (Y := X) fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
pos :
  ∀ (ht : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (f t)),
    ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t
neg :
  ∀ (ht : f t ∉ Set.Ioo 0 1),
    ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t
⊢ ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t

Tactic:
by_cases ht : f t ∈ Set.Ioo 0 1

Premises used: OfNat.ofNat, Set.Ioo
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (f t)
⊢ Continuous (Y := (↑(Set.Icc 0 1) : Type)) fun (i : (↑(f ⁻¹' Set.Ioo 0 1) : Type u_3)) ↦
    Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x) (f (↑i : T)) ⋯

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (f t)
simp_all :
  ∀ (hx : ContinuousOn x (f ⁻¹' {0})ᶜ) (hy : ContinuousOn y (f ⁻¹' {1})ᶜ) (hx' : Bornology.IsBounded (Set.range x))
    (hy' : Bornology.IsBounded (Set.range y)) (hD' : 0 < D) (hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D)
    (ht : 0 < f t ∧ f t < 1) (a : T), 0 < f a → f a < 1 → ¬f a = 0
⊢ ∀ (x : (↑(f ⁻¹' Set.Ioo 0 1) : Type u_3)), (↑x : T) ∈ f ⁻¹' {0}ᶜ

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
D : ℝ
t : T
hx : ContinuousOn x (f ⁻¹' {0})ᶜ
hy : ContinuousOn y (f ⁻¹' {1})ᶜ
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
ht : 0 < f t ∧ f t < 1
⊢ ∀ (a : T), 0 < f a → f a < 1 → ¬f a = 0

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (f t)
simp_all :
  ∀ (hx : ContinuousOn x (f ⁻¹' {0})ᶜ) (hy : ContinuousOn y (f ⁻¹' {1})ᶜ) (hx' : Bornology.IsBounded (Set.range x))
    (hy' : Bornology.IsBounded (Set.range y)) (hD' : 0 < D) (hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D)
    (ht : 0 < f t ∧ f t < 1) (a : T), 0 < f a → f a < 1 → ¬f a = 1
⊢ ∀ (x : (↑(f ⁻¹' Set.Ioo 0 1) : Type u_3)), (↑x : T) ∈ f ⁻¹' {1}ᶜ

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
D : ℝ
t : T
hx : ContinuousOn x (f ⁻¹' {0})ᶜ
hy : ContinuousOn y (f ⁻¹' {1})ᶜ
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
ht : 0 < f t ∧ f t < 1
⊢ ∀ (a : T), 0 < f a → f a < 1 → ¬f a = 1

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (f t)
⊢ ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t

Tactic:
exact ((isOpen_Ioo.preimage hf).isOpenEmbedding_subtypeVal.continuousAt_iff
      (x := ⟨t, ht⟩)).mp ((continuous_convexCombPair (X := X)).comp₃ (W := f ⁻¹' Set.Ioo 0 1)
      (e := fun i ↦ ⟨f i, Set.Ioo_subset_Icc_self i.prop⟩) (f := x ∘ (↑)) (k := y ∘ (↑))
      (by fun_prop) (hx.comp_continuous continuous_subtype_val (by simp_all; grind))
      (hy.comp_continuous continuous_subtype_val (by simp_all; grind))).continuousAt
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht : f t ∉ Set.Ioo 0 1
⊢ f t = 0 ∨ f t = 1

Tactic:
simpa [le_antisymm_iff, hf0, hf1, -not_and, not_and_or] using ht

Premises used: le_antisymm_iff, not_and_or, not_and
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht : f t ∉ Set.Ioo 0 1
neg :
  ∀ (ht : f t = 0), ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t
neg₁ :
  ∀ (ht : f t = 1), ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t
⊢ ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t

Tactic:
obtain ht | ht : f t = 0 ∨ f t = 1 := by
    simpa [le_antisymm_iff, hf0, hf1, -not_and, not_and_or] using ht
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht_1 : f t ∉ Set.Ioo 0 1
ht : f t = 0
neg : Filter.Tendsto (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) (nhds t) (nhds (y t))
⊢ ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t

Tactic:
simp only [ContinuousAt, ht, sub_zero, convexCombPair_zero]

Premises used: ContinuousAt, sub_zero, Convexity.convexCombPair_zero
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht_1 : f t ∉ Set.Ioo 0 1
ht : f t = 0
neg :
  ∀ (i : ℝ),
    0 < i → ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) ⋯ ⋯ ⋯ (x x_1) (y x_1) ∈ Metric.ball (y t) i
⊢ Filter.Tendsto (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) (nhds t) (nhds (y t))

Tactic:
rw [Metric.nhds_basis_ball.tendsto_right_iff]

Premises used: Metric.nhds_basis_ball, Filter.HasBasis.tendsto_right_iff