awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_simp : C₁.IsSimplicial
h₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
⊢ Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
have obtain : ∀ (s : Set E) (hs_fin : s.Finite) (hs_lin : LinearIndepOn ℝ id s) (hs_span : hull ℝ s = C₁),
  Eq (α := PointedCone ℝ (E ⊗[ℝ] F)) (C₁.minTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
    (C₁.maxTensorProduct (↑C₂ : PointedCone ℝ F) : PointedCone ℝ (E ⊗[ℝ] F))
Tactic: classical
  obtain ⟨s, hs_fin, hs_lin, hs_span⟩ := h₁_simp
  haveI : Fintype s := hs_fin.fintype
  -- The conic hull (R≥0-span) is contained in the linear span (ℝ-span)
  have hull_sub_span : (hull ℝ s : Set E) ⊆ Submodule.span ℝ s := by
    intro x hx
    rw [SetLike.mem_coe, PointedCone.mem_hull_set] at hx
    obtain ⟨c, hc_supp, _, hc_sum⟩ := hx
    exact hc_sum ▸ Submodule.sum_mem _ fun m hm =>
      Submodule.smul_mem _ _ (Submodule.subset_span (hc_supp hm))
  -- Extract basis from `C₁.IsSimplicial` + generating
  let b := Basis.mk hs_lin <| by
    simpa only [id_eq, Subtype.range_coe] using
      h₁_gen ▸ hs_span ▸ Submodule.span_le.mpr hull_sub_span
  -- Dual basis elements are in C₁*
  have h_coord_dual : ∀ i, b.coord i ∈ dual (Dual.eval ℝ E) C₁ :=
    basis_coord_mem_dual _ _ (hs_span ▸ (Submodule.span_mono <| by simp [b]))
  -- Reduce to proving z ∈ max → z ∈ min
  apply le_antisymm (minTensorProduct_le_maxTensorProduct C₁ C₂.toPointedCone)
  intro z hz
  -- Express z using basis: z = ∑ b_i ⊗ y_i
  rw [← (equivFinsuppOfBasisLeft b).symm_apply_apply z,
    TensorProduct.equivFinsuppOfBasisLeft_symm_apply, Finsupp.sum_fintype _ _ (by simp)]
  -- Show z ∈ min by showing b_i ∈ C₁ and y_i ∈ C₂
  refine Submodule.sum_mem _ fun i _ => tmul_mem_minTensorProduct ?_ ?_
  · simpa only [b, Basis.coe_mk] using (hs_span ▸ subset_hull) i.prop
  · simp only [equivFinsuppOfBasisLeft_apply]
    rw [← ProperCone.dual_dual_flip (topDualPairing ℝ F) C₂]
    intro f (hf : (f : F →ₗ[ℝ] ℝ) ∈ dual (Dual.eval ℝ F) (C₂ : Set F))
    simp only [mem_maxTensorProduct] at hz
    have h_nonneg := hz (b.coord i) (h_coord_dual i) (f : F →ₗ[ℝ] ℝ) hf
    have h_eq : dualDistrib ℝ E F ((b.coord i) ⊗ₜ[ℝ] (f : F →ₗ[ℝ] ℝ)) =
        (f : F →ₗ[ℝ] ℝ) ∘ₗ (TensorProduct.lid ℝ F) ∘ₗ (b.coord i).rTensor F := by
      ext; simp [mul_comm]
    simpa only [h_eq, LinearMap.comp_apply, LinearEquiv.coe_coe] using h_nonneg
Cleared hypotheses: h₁_simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : ProperCone ℝ F
C₂ : PointedCone ℝ E
h₂_simp : C₂.IsSimplicial
h₂_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₂ : Set E)) ⊤
⊢ Eq (α := PointedCone ℝ (F ⊗[ℝ] E)) ((↑C₁ : PointedCone ℝ F).minTensorProduct C₂ : PointedCone ℝ (F ⊗[ℝ] E))
    ((↑C₁ : PointedCone ℝ F).maxTensorProduct C₂ : PointedCone ℝ (F ⊗[ℝ] E))
have rw : Eq (α := PointedCone ℝ (F ⊗[ℝ] E))
  (map (↑(TensorProduct.comm ℝ E F) : E ⊗[ℝ] F →ₗ[ℝ] F ⊗[ℝ] E) (C₂.minTensorProduct (↑C₁ : PointedCone ℝ F)) :
    PointedCone ℝ (F ⊗[ℝ] E))
  ((↑C₁ : PointedCone ℝ F).maxTensorProduct C₂ : PointedCone ℝ (F ⊗[ℝ] E))
Tactic: rw [← minTensorProduct_comm, ← maxTensorProduct_comm,
    minTensorProduct_eq_max_of_simplicial_generating_left C₂ C₁ h₂_simp h₂_gen]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : ProperCone ℝ F
C₂ : PointedCone ℝ E
h₂_simp : C₂.IsSimplicial
h₂_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₂ : Set E)) ⊤
rw :
  Eq (α := PointedCone ℝ (F ⊗[ℝ] E))
    (map (↑(TensorProduct.comm ℝ E F) : E ⊗[ℝ] F →ₗ[ℝ] F ⊗[ℝ] E) (C₂.minTensorProduct (↑C₁ : PointedCone ℝ F)) :
      PointedCone ℝ (F ⊗[ℝ] E))
    ((↑C₁ : PointedCone ℝ F).maxTensorProduct C₂ : PointedCone ℝ (F ⊗[ℝ] E))
⊢ Eq (α := PointedCone ℝ (F ⊗[ℝ] E)) ((↑C₁ : PointedCone ℝ F).minTensorProduct C₂ : PointedCone ℝ (F ⊗[ℝ] E))
    ((↑C₁ : PointedCone ℝ F).maxTensorProduct C₂ : PointedCone ℝ (F ⊗[ℝ] E))
have rw₁ : Eq (α := PointedCone ℝ (F ⊗[ℝ] E))
  (map (↑(TensorProduct.comm ℝ E F) : E ⊗[ℝ] F →ₗ[ℝ] F ⊗[ℝ] E) (C₂.minTensorProduct (↑C₁ : PointedCone ℝ F)) :
    PointedCone ℝ (F ⊗[ℝ] E))
  (map (↑(TensorProduct.comm ℝ E F) : E ⊗[ℝ] F →ₗ[ℝ] F ⊗[ℝ] E) (C₂.maxTensorProduct (↑C₁ : PointedCone ℝ F)) :
    PointedCone ℝ (F ⊗[ℝ] E))
Tactic: rw [← minTensorProduct_comm, ← maxTensorProduct_comm,
    minTensorProduct_eq_max_of_simplicial_generating_left C₂ C₁ h₂_simp h₂_gen]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.TensorProduct (goal)
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : AddCommGroup F
inst_3 : Module ℝ F
inst_4 : TopologicalSpace F
inst_5 : IsTopologicalAddGroup F
inst_6 : T2Space F
inst_7 : FiniteDimensional ℝ F
inst_8 : ContinuousSMul ℝ F
inst_9 : LocallyConvexSpace ℝ F
C₁ : ProperCone ℝ F
C₂ : PointedCone ℝ E
h₂_simp : C₂.IsSimplicial
h₂_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₂ : Set E)) ⊤
rw :
  Eq (α := PointedCone ℝ (F ⊗[ℝ] E))
    (map (↑(TensorProduct.comm ℝ E F) : E ⊗[ℝ] F →ₗ[ℝ] F ⊗[ℝ] E) (C₂.minTensorProduct (↑C₁ : PointedCone ℝ F)) :
      PointedCone ℝ (F ⊗[ℝ] E))
    ((↑C₁ : PointedCone ℝ F).maxTensorProduct C₂ : PointedCone ℝ (F ⊗[ℝ] E))
rw₁ :
  Eq (α := PointedCone ℝ (F ⊗[ℝ] E))
    (map (↑(TensorProduct.comm ℝ E F) : E ⊗[ℝ] F →ₗ[ℝ] F ⊗[ℝ] E) (C₂.minTensorProduct (↑C₁ : PointedCone ℝ F)) :
      PointedCone ℝ (F ⊗[ℝ] E))
    (map (↑(TensorProduct.comm ℝ E F) : E ⊗[ℝ] F →ₗ[ℝ] F ⊗[ℝ] E) (C₂.maxTensorProduct (↑C₁ : PointedCone ℝ F)) :
      PointedCone ℝ (F ⊗[ℝ] E))
⊢ Eq (α := PointedCone ℝ (F ⊗[ℝ] E)) ((↑C₁ : PointedCone ℝ F).minTensorProduct C₂ : PointedCone ℝ (F ⊗[ℝ] E))
    ((↑C₁ : PointedCone ℝ F).maxTensorProduct C₂ : PointedCone ℝ (F ⊗[ℝ] E))
have rw₂ : Eq (α := PointedCone ℝ (F ⊗[ℝ] E))
  (map (↑(TensorProduct.comm ℝ E F) : E ⊗[ℝ] F →ₗ[ℝ] F ⊗[ℝ] E) (C₂.maxTensorProduct (↑C₁ : PointedCone ℝ F)) :
    PointedCone ℝ (F ⊗[ℝ] E))
  (map (↑(TensorProduct.comm ℝ E F) : E ⊗[ℝ] F →ₗ[ℝ] F ⊗[ℝ] E) (C₂.maxTensorProduct (↑C₁ : PointedCone ℝ F)) :
    PointedCone ℝ (F ⊗[ℝ] E))
Tactic: rw [← minTensorProduct_comm, ← maxTensorProduct_comm,
    minTensorProduct_eq_max_of_simplicial_generating_left C₂ C₁ h₂_simp h₂_gen]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
⊢ LipschitzOnWith (2 * M / ε).toNNReal f (ball x₀ (r - ε))
have set : let K := 2 * M / ε;
∀ (hK : K = 2 * M / ε), LipschitzOnWith K.toNNReal f (ball x₀ (r - ε))
Tactic: set K := 2 * M / ε with hK
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
⊢ f x - f y ≤ K * ‖x - y‖
have inl : ∀ (hy : x ∈ ball x₀ (r - ε)), f x - f x ≤ K * ‖x - x‖
Tactic: obtain rfl | hxy := eq_or_ne x y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
inl : ∀ (hy : x ∈ ball x₀ (r - ε)), f x - f x ≤ K * ‖x - x‖
⊢ f x - f y ≤ K * ‖x - y‖
have inr : ∀ (hxy : x ≠ y), f x - f y ≤ K * ‖x - y‖
Tactic: obtain rfl | hxy := eq_or_ne x y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hxy : x ≠ y
⊢ r - ε ≤ r
have linarith : r < r - ε → 0 - ε + (r - (r - ε)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hxy : x ≠ y
⊢ f x - f y ≤ K * ‖x - y‖
have hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
Tactic: have hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r := ball_subset_ball <| by linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hxy : x ≠ y
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
⊢ f x - f y ≤ K * ‖x - y‖
have hx' : x ∈ ball x₀ r
Tactic: have hx' : x ∈ ball x₀ r := hx₀r hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hxy : x ≠ y
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
⊢ f x - f y ≤ K * ‖x - y‖
have hy' : y ∈ ball x₀ r
Tactic: have hy' : y ∈ ball x₀ r := hx₀r hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hxy : x ≠ y
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
⊢ f x - f y ≤ K * ‖x - y‖
have hxy₁ : 0 < ‖x - y‖
Tactic: replace hxy : 0 < ‖x - y‖ := by rwa [norm_sub_pos_iff]
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
⊢ ‖z - x₀‖ < r
have _ : ‖z - x₀‖ = ‖x - x₀ + (ε / ‖x - y‖) • (x - y)‖
Tactic: calc
        _ = ‖(x - x₀) + (ε / ‖x - y‖) • (x - y)‖ := by simp only [z, add_sub_right_comm]
        _ ≤ ‖x - x₀‖ + ‖(ε / ‖x - y‖) • (x - y)‖ := norm_add_le ..
        _ < r - ε + ε :=
          add_lt_add_of_lt_of_le (mem_ball_iff_norm.1 hx) <| by
            simp [norm_smul, abs_of_nonneg, hε.le, hxy.ne']
        _ = r := by simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
_ : ‖z - x₀‖ = ‖x - x₀ + (ε / ‖x - y‖) • (x - y)‖
⊢ ‖z - x₀‖ < r
have _₁ : r - ε + ε = r
Tactic: calc
        _ = ‖(x - x₀) + (ε / ‖x - y‖) • (x - y)‖ := by simp only [z, add_sub_right_comm]
        _ ≤ ‖x - x₀‖ + ‖(ε / ‖x - y‖) • (x - y)‖ := norm_add_le ..
        _ < r - ε + ε :=
          add_lt_add_of_lt_of_le (mem_ball_iff_norm.1 hx) <| by
            simp [norm_smul, abs_of_nonneg, hε.le, hxy.ne']
        _ = r := by simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
⊢ f x - f y ≤ K * ‖x - y‖
have hz : z ∈ ball x₀ r
Tactic: have hz : z ∈ ball x₀ r := mem_ball_iff_norm.2 <| by
      calc
        _ = ‖(x - x₀) + (ε / ‖x - y‖) • (x - y)‖ := by simp only [z, add_sub_right_comm]
        _ ≤ ‖x - x₀‖ + ‖(ε / ‖x - y‖) • (x - y)‖ := norm_add_le ..
        _ < r - ε + ε :=
          add_lt_add_of_lt_of_le (mem_ball_iff_norm.1 hx) <| by
            simp [norm_smul, abs_of_nonneg, hε.le, hxy.ne']
        _ = r := by simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
⊢ f x - f y ≤ K * ‖x - y‖
have hab : a + b = 1
Tactic: have hab : a + b = 1 := by simp [field, a, b]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
⊢ x = a • x + b • x
have rw : x = x
Tactic: rw [Convex.combo_self hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
⊢ a • x + b • x = a • y + b • z
have simp : (ε / (ε + ‖x - y‖)) • x + (‖x - y‖ / (ε + ‖x - y‖)) • x =
  (ε / (ε + ‖x - y‖)) • y + ((‖x - y‖ / (ε + ‖x - y‖)) • x + ((ε / (ε + ‖x - y‖)) • x - (ε / (ε + ‖x - y‖)) • y))
Tactic: simp [z, a, b, smul_smul, hxy.ne', smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
⊢ x = a • y + b • z
have x₁ : x = a • x + b • x
Tactic: calc
        x = a • x + b • x := by rw [Convex.combo_self hab]
        _ = a • y + b • z := by simp [z, a, b, smul_smul, hxy.ne', smul_sub]; abel
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
x₁ : x = a • x + b • x
⊢ x = a • y + b • z
have x₂ : a • x + b • x = a • y + b • z
Tactic: calc
        x = a • x + b • x := by rw [Convex.combo_self hab]
        _ = a • y + b • z := by simp [z, a, b, smul_smul, hxy.ne', smul_sub]; abel
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
⊢ f x - f y ≤ K * ‖x - y‖
have hxyz : x = a • y + b • z
Tactic: have hxyz : x = a • y + b • z := by
      calc
        x = a • x + b • x := by rw [Convex.combo_self hab]
        _ = a • y + b • z := by simp [z, a, b, smul_smul, hxy.ne', smul_sub]; abel
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
⊢ f x - f y ≤ K * ‖x - y‖
have inr : ε * (f x - f y) ≤ ‖x - y‖ * (2 * M)
Tactic: rw [hK, mul_comm, ← mul_div_assoc, le_div_iff₀' hε]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
⊢ ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x)
have h : f (a • y + b • z) ≤ a • f y + b • f z
Tactic: have h := hf.2 hy' hz (by positivity) (by positivity) hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
h : f (a • y + b • z) ≤ a • f y + b • f z
⊢ ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x)
have h₁ : f x ≤ ε / (ε + ‖x - y‖) * f y + ‖x - y‖ / (ε + ‖x - y‖) * f z
Tactic: simp only [← hxyz, smul_eq_mul, a, b] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
h : f x ≤ ε / (ε + ‖x - y‖) * f y + ‖x - y‖ / (ε + ‖x - y‖) * f z
⊢ ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x)
have h₁ : f x * (ε + ‖x - y‖) ≤ ε * f y + ‖x - y‖ * f z
Tactic: field_simp at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
⊢ ‖x - y‖ * (f z - f x) ≤ ‖x - y‖ * (2 * M)
have rw : ‖x - y‖ * (f z + -f x) ≤ ‖x - y‖ * (M + M)
Tactic: rw [sub_eq_add_neg (f _), two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
⊢ ‖x - y‖ * (f z + -f x) ≤ ‖x - y‖ * (M + M)
have hbc : f z ≤ M
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
hbc : f z ≤ M
⊢ ‖x - y‖ * (f z + -f x) ≤ ‖x - y‖ * (M + M)
have hbc₁ : -f x ≤ M
Tactic: gcongr