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
i : (↑(Set.Icc 0 1) : Type)
x y : X × X
⊢ (↑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)
have 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)
Tactic: nth_grw 2 [le_max_right (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 : ℝ)) * 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 : ℝ)) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)
have h₁ : 0 ≤ 1 - (↑i : ℝ)
Tactic: nth_grw 2 [le_max_right (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
⊢ (↑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)
have 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)
Tactic: rw [← add_mul, add_sub_cancel, one_mul]
-- 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 : ℝ) + (1 - (↑i : ℝ))) * 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)
have ha₁ : 1 * 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]
-- 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 : ℝ) + (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)
⊢ (↑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)
have ha₂ : 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]
-- 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
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
have hb : ∀ (x y : (↑(Set.Icc 0 1) : Type)),
  edist (convexCombPair (↑(x, b).1 : ℝ) (1 - (↑(x, b).1 : ℝ)) sorry sorry sorry (x, b).2.1 (x, b).2.2)
      (convexCombPair (↑(y, b).1 : ℝ) (1 - (↑(y, b).1 : ℝ)) sorry sorry sorry (y, b).2.1 (y, b).2.2) ≤
    (↑(nndist b.1 b.2) : ENNReal) * edist x y
Tactic: refine LipschitzWith.continuous (K := nndist b.1 b.2) fun 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
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) ≤
    (↑(nndist b.1 b.2) : ENNReal) * edist x y
have hb : edist (convexCombPair (↑(x, b).1 : ℝ) (1 - (↑(x, b).1 : ℝ)) sorry sorry sorry (x, b).2.1 (x, b).2.2)
    (convexCombPair (↑(y, b).1 : ℝ) (1 - (↑(y, b).1 : ℝ)) sorry sorry sorry (y, b).2.1 (y, b).2.2) ≤
  edist x y * (↑(nndist b.1 b.2) : ENNReal)
Tactic: rw [mul_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
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)
⊢ Continuous.{u_3, u_2} (Y := X) fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)
have 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) sorry sorry sorry (x i) (y i)
Tactic: obtain ⟨D, hD, hD'⟩ := ((Metric.isBounded_iff_eventually.mp (hx'.union hy')).and
    (Filter.eventually_gt_atTop 0)).exists
-- 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
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
⊢ Continuous.{u_3, u_2} (Y := X) fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)
have hD₁ : ∀ (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₂))
Cleared hypotheses: hD
-- 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
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
⊢ Continuous.{u_3, u_2} (Y := X) fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)
have rw : ∀ (x_1 : T), ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) sorry sorry sorry (x i) (y i)) x_1
Tactic: rw [continuous_iff_continuousAt]
-- 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
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
⊢ ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t
have 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) sorry sorry sorry (x i) (y i)) t
Tactic: by_cases ht : f t ∈ Set.Ioo 0 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
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
⊢ ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t
have neg : ∀ (ht : f t ∉ Set.Ioo 0 1),
  ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) sorry sorry sorry (x i) (y i)) t
Tactic: by_cases ht : f t ∈ Set.Ioo 0 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
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)
⊢ ∀ (x : (↑(f ⁻¹' Set.Ioo 0 1) : Type u_3)), (↑x : T) ∈ f ⁻¹' {0}ᶜ
have 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
Tactic: simp_all
Cleared hypotheses: hx, hy, hx', hy', hD', hD, ht
-- 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
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)
⊢ ∀ (x : (↑(f ⁻¹' Set.Ioo 0 1) : Type u_3)), (↑x : T) ∈ f ⁻¹' {1}ᶜ
have 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
Tactic: simp_all
Cleared hypotheses: hx, hy, hx', hy', hD', hD, ht
-- 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
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
⊢ ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t
have neg : ∀ (ht : f t = 0), ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) sorry sorry sorry (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
-- 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
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
⊢ ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t
have neg₁ : ∀ (ht : f t = 1), ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) sorry sorry sorry (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
-- 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
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
⊢ ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t
have neg : Filter.Tendsto (fun (i : T) ↦ convexCombPair (f i) (1 - f i) sorry sorry sorry (x i) (y i)) (nhds t) (nhds (y t))
Tactic: simp only [ContinuousAt, ht, sub_zero, convexCombPair_zero]
-- 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
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
⊢ Filter.Tendsto (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) (nhds t) (nhds (y t))
have neg : ∀ (i : ℝ),
  0 < i → ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) sorry sorry sorry (x x_1) (y x_1) ∈ Metric.ball (y t) i
Tactic: rw [Metric.nhds_basis_ball.tendsto_right_iff]
-- 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
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
⊢ ∀ᶠ (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
have 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) sorry sorry sorry (x j) (y j) ∈ 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'
-- 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
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)
⊢ convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j) ∈ Metric.ball (y t) r
have hj₁ : 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' ⊢
Cleared hypotheses: hj, hj'
-- 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
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
⊢ convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j) ∈ Metric.ball (y t) r
have hj'₁ : |f j| < r / D / 3
Tactic: simp only [Set.mem_preimage, Metric.mem_ball, dist_zero_right, Real.norm_eq_abs] at hj hj' ⊢
Cleared hypotheses: hj, hj'
-- 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
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
⊢ dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j)) (y t) < r
have h : f j * dist (x j) (x j) + (1 - f j) * dist (y j) (y t) + dist (convexCombPair (f j) (1 - f j) sorry sorry sorry (x j) (y t)) (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]
-- 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
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
⊢ 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
have h : (1 - f j) * dist (y j) (y t) + f j * dist (x j) (y t) < r
Tactic: simp only [dist_self, mul_zero, zero_add, 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
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
⊢ (1 - f j) * dist (y j) (y t) + f j * dist (x j) (y t) < r
have h : 1 * (r / 3) + r / D / 3 * D < r
Tactic: grw [sub_le_self _ (hf0 _), hj, hD, (le_abs_self _).trans hj'.le]
-- 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
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
⊢ (1 - f j) * dist (y j) (y t) + f j * dist (x j) (y t) < r
have h₁ : 0 ≤ f j
Tactic: grw [sub_le_self _ (hf0 _), hj, hD, (le_abs_self _).trans hj'.le]
-- 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
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
⊢ 1 * (r / 3) + r / D / 3 * D < r
have h : HAdd.hAdd (α := ℝ) 1 1 < 3
Tactic: field_simp
-- 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
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
⊢ ContinuousAt.{u_3, u_2} (Y := X) (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t
have neg : Filter.Tendsto (fun (i : T) ↦ convexCombPair (f i) (1 - f i) sorry sorry sorry (x i) (y i)) (nhds t) (nhds (x t))
Tactic: simp only [ContinuousAt, ht, sub_self, convexCombPair_one]
-- 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
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
⊢ Filter.Tendsto (fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) (nhds t) (nhds (x t))
have neg : ∀ (i : ℝ),
  0 < i → ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) sorry sorry sorry (x x_1) (y x_1) ∈ Metric.ball (x t) i
Tactic: rw [Metric.nhds_basis_ball.tendsto_right_iff]
-- 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
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
⊢ ∀ᶠ (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
have 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) sorry sorry sorry (x j) (y j) ∈ 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'