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
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
r : ℝ
hr : 0 < r
⊢ 0 < r / D / 3

Tactic:
simp [*]
-- 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
r : ℝ
hr : 0 < r
⊢ t ∈ f ⁻¹' {1}ᶜ

Tactic:
simp [*]
-- 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
r : ℝ
hr : 0 < r
⊢ 0 < r / 3

Tactic:
simpa
-- 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
r : ℝ
hr : 0 < r
h :
  ∀ (j : T) (hj : j ∈ y ⁻¹' Metric.ball (y t) (r / 3)) (hj' : j ∈ f ⁻¹' Metric.ball 0 (r / D / 3)),
    convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j) ∈ Metric.ball (y t) r
⊢ ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) ⋯ ⋯ ⋯ (x x_1) (y x_1) ∈ Metric.ball (y t) r

Tactic:
filter_upwards [hy.continuousAt ((hf.isOpen_preimage _ isClosed_singleton.isOpen_compl).mem_nhds
      (x := t) (by simp [*])) (Metric.ball_mem_nhds _ (show 0 < r / 3 by simpa)),
      hf.tendsto' _ _ ht (Metric.ball_mem_nhds _ (show 0 < r / D / 3 by simp [*]))] with j hj hj'

Premises used: IsClosed.isOpen_compl, Metric.ball_mem_nhds, IsOpen.mem_nhds, Continuous.tendsto', ContinuousOn.continuousAt, Continuous.isOpen_preimage
-- 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
r : ℝ
hr : 0 < r
j : T
hj : j ∈ y ⁻¹' Metric.ball (y t) (r / 3)
hj' : j ∈ f ⁻¹' Metric.ball 0 (r / D / 3)
⊢ dist (y j) (y t) < r / 3

Tactic:
simp only [Set.mem_preimage, Metric.mem_ball, dist_zero_right, Real.norm_eq_abs] at hj hj' ⊢

Premises used: Metric.mem_ball, dist_zero_right, Real.norm_eq_abs, Set.mem_preimage
-- 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
r : ℝ
hr : 0 < r
j : T
hj : j ∈ y ⁻¹' Metric.ball (y t) (r / 3)
hj' : j ∈ f ⁻¹' Metric.ball 0 (r / D / 3)
hj₁ : dist (y j) (y t) < r / 3
⊢ |f j| < r / D / 3

Tactic:
simp only [Set.mem_preimage, Metric.mem_ball, dist_zero_right, Real.norm_eq_abs] at hj hj' ⊢

Premises used: Metric.mem_ball, dist_zero_right, Real.norm_eq_abs, Set.mem_preimage
-- 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
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
⊢ 0 ≤ 1 - f j

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)
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
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
h :
  f j * dist (x j) (x j) + (1 - f j) * dist (y j) (y t) +
      dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y t)) (y t) <
    r
⊢ dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j)) (y t) < r

Tactic:
grw [dist_triangle _ (convexCombPair (f j) (1 - f j) (hf0 _) (by simpa using hf1 _)
      (add_sub_cancel ..) (x j) (y t)), dist_convexCombPair_convexCombPair_le]

Premises used: dist_triangle, HSub.hSub, add_sub_cancel, Convexity.convexCombPair, OfNat.ofNat, 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
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
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
h : (1 - f j) * dist (y j) (y t) + f j * dist (x j) (y t) < r
⊢ f j * dist (x j) (x j) + (1 - f j) * dist (y j) (y t) +
      dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y t)) (y t) <
    r

Tactic:
simp only [dist_self, mul_zero, zero_add, dist_convexCombPair_right]

Premises used: zero_add, MulZeroClass.mul_zero, dist_self, 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
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
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
h : 1 * (r / 3) + r / D / 3 * D < r
h₁ : 0 ≤ f j
⊢ (1 - f j) * dist (y j) (y t) + f j * dist (x j) (y t) < r

Tactic:
grw [sub_le_self _ (hf0 _), hj, hD, (le_abs_self _).trans hj'.le]

Premises used: le_abs_self, LT.lt.le, sub_le_self, LE.le.trans
-- 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
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
h : HAdd.hAdd (α := ℝ) 1 1 < 3
⊢ 1 * (r / 3) + r / D / 3 * D < r

Tactic:
field_simp
-- 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
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
⊢ HAdd.hAdd (α := ℝ) 1 1 < 3

Tactic:
norm_num
-- 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
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
⊢ 0 ≤ f j

Tactic:
hf0 _
-- 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
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
⊢ 0 ≤ f j

Tactic:
exact hf0 _
-- 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 = 1
neg : Filter.Tendsto (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) (nhds t) (nhds (x 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_self, convexCombPair_one]

Premises used: sub_self, ContinuousAt, Convexity.convexCombPair_one
-- 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 = 1
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 (x t) i
⊢ Filter.Tendsto (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) (nhds t) (nhds (x t))

Tactic:
rw [Metric.nhds_basis_ball.tendsto_right_iff]

Premises used: Metric.nhds_basis_ball, Filter.HasBasis.tendsto_right_iff
-- 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 = 1
r : ℝ
hr : 0 < r
⊢ 0 < r / D / 3

Tactic:
simp [*]
-- 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 = 1
r : ℝ
hr : 0 < r
⊢ t ∈ f ⁻¹' {0}ᶜ

Tactic:
simp [*]
-- 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 = 1
r : ℝ
hr : 0 < r
⊢ 0 < r / 3

Tactic:
simpa
-- 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 = 1
r : ℝ
hr : 0 < r
h :
  ∀ (j : T) (hj : j ∈ x ⁻¹' Metric.ball (x t) (r / 3)) (hj' : j ∈ f ⁻¹' Metric.ball 1 (r / D / 3)),
    convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j) ∈ Metric.ball (x t) r
⊢ ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) ⋯ ⋯ ⋯ (x x_1) (y x_1) ∈ Metric.ball (x t) r

Tactic:
filter_upwards [hx.continuousAt ((hf.isOpen_preimage _ isClosed_singleton.isOpen_compl).mem_nhds
      (x := t) (by simp [*])) (Metric.ball_mem_nhds _ (show 0 < r / 3 by simpa)),
      hf.tendsto' _ _ ht (Metric.ball_mem_nhds _ (show 0 < r / D / 3 by simp [*]))] with j hj hj'

Premises used: IsClosed.isOpen_compl, Metric.ball_mem_nhds, IsOpen.mem_nhds, Continuous.tendsto', ContinuousOn.continuousAt, Continuous.isOpen_preimage
-- 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 = 1
r : ℝ
hr : 0 < r
j : T
hj : j ∈ x ⁻¹' Metric.ball (x t) (r / 3)
hj' : j ∈ f ⁻¹' Metric.ball 1 (r / D / 3)
⊢ dist (x j) (x t) < r / 3

Tactic:
simp only [Set.mem_preimage, Metric.mem_ball, Real.dist_eq] at hj hj' ⊢

Premises used: Metric.mem_ball, Real.dist_eq, Set.mem_preimage
-- 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 = 1
r : ℝ
hr : 0 < r
j : T
hj : j ∈ x ⁻¹' Metric.ball (x t) (r / 3)
hj' : j ∈ f ⁻¹' Metric.ball 1 (r / D / 3)
hj₁ : dist (x j) (x t) < r / 3
⊢ |f j - 1| < r / D / 3

Tactic:
simp only [Set.mem_preimage, Metric.mem_ball, Real.dist_eq] at hj hj' ⊢

Premises used: Metric.mem_ball, Real.dist_eq, Set.mem_preimage
-- 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 = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ 0 ≤ 1 - f j

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)
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 = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
h :
  f j * dist (x j) (x t) + (1 - f j) * dist (y j) (y j) +
      dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x t) (y j)) (x t) <
    r
⊢ dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j)) (x t) < r

Tactic:
grw [dist_triangle _ (convexCombPair (f j) (1 - f j) (hf0 _) (by simpa using hf1 _)
      (add_sub_cancel ..) (x t) (y j)), dist_convexCombPair_convexCombPair_le]

Premises used: dist_triangle, HSub.hSub, add_sub_cancel, Convexity.convexCombPair, OfNat.ofNat, 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
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 = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
h : f j * dist (x j) (x t) + (1 - f j) * dist (x t) (y j) < r
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (y j) (y j) +
      dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x t) (y j)) (x t) <
    r

Tactic:
simp only [dist_self, mul_zero, add_zero, dist_convexCombPair_left]

Premises used: MulZeroClass.mul_zero, dist_self, Convexity.dist_convexCombPair_left, add_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 = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ 1 - f j < r / D / 3

Tactic:
grw [abs_sub_comm, ← le_abs_self] at hj'

Premises used: le_abs_self, abs_sub_comm
-- 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 = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
h : 1 * (r / 3) + r / D / 3 * D < r
h₁ : 0 ≤ f j
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (x t) (y j) < r

Tactic:
grw [hj, hj', hf1, hD]
-- 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 = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
h : HAdd.hAdd (α := ℝ) 1 1 < 3
⊢ 1 * (r / 3) + r / D / 3 * D < r

Tactic:
field_simp
-- 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 = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ HAdd.hAdd (α := ℝ) 1 1 < 3

Tactic:
norm_num
-- 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 = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ 0 ≤ f j

Tactic:
hf0 _
-- 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 = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ 0 ≤ f j

Tactic:
exact hf0 _
-- 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
inst_3 : BoundedSpace X
T : Type u_3
inst_4 : 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}ᶜ)
i : T
⊢ 0 ≤ 1 - f i

Tactic:
simpa using hf1 _