awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
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₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
hull_sub_span : (↑(hull ℝ s) : Set E) ⊆ (↑(Submodule.span ℝ s) : Set E)
b : Basis (↑s : Type u_1) ℝ E := Basis.mk hs_lin ⋯
h_coord_dual :
  ∀ (i : (↑s : Type u_1)),
    Membership.mem (γ := PointedCone ℝ (Dual ℝ E)) (dual (Dual.eval ℝ E) (↑C₁ : Set E)) (b.coord i)
z : E ⊗[ℝ] F
i : (↑s : Type u_1)
h : Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i
f : F →L[ℝ] ℝ
hf : Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑C₂ : Set F)) (↑f : F →ₗ[ℝ] ℝ)
hz :
  ∀ (φ : Dual ℝ E),
    Membership.mem (γ := PointedCone ℝ (Dual ℝ E)) (dual (Dual.eval ℝ E) (↑C₁ : Set E)) φ →
      ∀ (ψ : Dual ℝ F),
        Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑(↑C₂ : PointedCone ℝ F) : Set F)) ψ →
          LE.le (α := ℝ) (0 : ℝ)
            ((((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (φ ⊗ₜ[ℝ] ψ) : Dual ℝ (E ⊗[ℝ] F)) :
                  (a : E ⊗[ℝ] F) → ℝ)
                z :
              ℝ)
h_nonneg :
  LE.le (α := ℝ) (0 : ℝ)
    ((((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (b.coord i ⊗ₜ[ℝ] (↑f : F →ₗ[ℝ] ℝ)) :
            Dual ℝ (E ⊗[ℝ] F)) :
          (a : E ⊗[ℝ] F) → ℝ)
        z :
      ℝ)
⊢ (dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (b.coord i ⊗ₜ[ℝ] (↑f : F →ₗ[ℝ] ℝ)) =
    (↑f : F →ₗ[ℝ] ℝ) ∘ₗ (↑(TensorProduct.lid ℝ F) : ℝ ⊗[ℝ] F →ₗ[ℝ] F) ∘ₗ LinearMap.rTensor F (b.coord i)

Tactic:
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]
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
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₁_gen : Eq (α := Submodule ℝ E) (Submodule.span ℝ (↑C₁ : Set E)) ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype (↑s : Type u_1)
hull_sub_span : (↑(hull ℝ s) : Set E) ⊆ (↑(Submodule.span ℝ s) : Set E)
b : Basis (↑s : Type u_1) ℝ E := Basis.mk hs_lin ⋯
h_coord_dual :
  ∀ (i : (↑s : Type u_1)),
    Membership.mem (γ := PointedCone ℝ (Dual ℝ E)) (dual (Dual.eval ℝ E) (↑C₁ : Set E)) (b.coord i)
z : E ⊗[ℝ] F
i : (↑s : Type u_1)
h : Membership.mem (γ := Finset (↑s : Type u_1)) Finset.univ i
f : F →L[ℝ] ℝ
hf : Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑C₂ : Set F)) (↑f : F →ₗ[ℝ] ℝ)
hz :
  ∀ (φ : Dual ℝ E),
    Membership.mem (γ := PointedCone ℝ (Dual ℝ E)) (dual (Dual.eval ℝ E) (↑C₁ : Set E)) φ →
      ∀ (ψ : Dual ℝ F),
        Membership.mem (γ := PointedCone ℝ (Dual ℝ F)) (dual (Dual.eval ℝ F) (↑(↑C₂ : PointedCone ℝ F) : Set F)) ψ →
          LE.le (α := ℝ) (0 : ℝ)
            ((((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (φ ⊗ₜ[ℝ] ψ) : Dual ℝ (E ⊗[ℝ] F)) :
                  (a : E ⊗[ℝ] F) → ℝ)
                z :
              ℝ)
h_nonneg :
  LE.le (α := ℝ) (0 : ℝ)
    ((((dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (b.coord i ⊗ₜ[ℝ] (↑f : F →ₗ[ℝ] ℝ)) :
            Dual ℝ (E ⊗[ℝ] F)) :
          (a : E ⊗[ℝ] F) → ℝ)
        z :
      ℝ)
h_eq :
  (dualDistrib ℝ E F : (a : Dual ℝ E ⊗[ℝ] Dual ℝ F) → Dual ℝ (E ⊗[ℝ] F)) (b.coord i ⊗ₜ[ℝ] (↑f : F →ₗ[ℝ] ℝ)) =
    (↑f : F →ₗ[ℝ] ℝ) ∘ₗ (↑(TensorProduct.lid ℝ F) : ℝ ⊗[ℝ] F →ₗ[ℝ] F) ∘ₗ LinearMap.rTensor F (b.coord i)
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((((topDualPairing ℝ F : (a : F →L[ℝ] ℝ) → F →ₗ[ℝ] ℝ) f : F →ₗ[ℝ] ℝ) : (a : F) → ℝ)
        ((TensorProduct.lid ℝ F : (a : ℝ ⊗[ℝ] F) → F)
            ((LinearMap.rTensor F (b.coord i) : (a : E ⊗[ℝ] F) → ℝ ⊗[ℝ] F) z : ℝ ⊗[ℝ] F) :
          F) :
      ℝ)

Tactic:
simpa only [h_eq, LinearMap.comp_apply, LinearEquiv.coe_coe] using h_nonneg

Premises used: LinearMap.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.Analysis.Convex.Cone.TensorProduct
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))
rw₂ 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))
⊢ Eq (α := PointedCone ℝ (F ⊗[ℝ] E)) ((↑C₁ : PointedCone ℝ F).minTensorProduct C₂ : 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]

Premises used: PointedCone.minTensorProduct_comm, PointedCone.maxTensorProduct_comm, PointedCone.minTensorProduct_eq_max_of_simplicial_generating_left
-- Module: Mathlib.Analysis.Convex.Continuous
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
set :
  let K := 2 * M / ε;
  ∀ (hK : K = 2 * M / ε), LipschitzOnWith K.toNNReal f (ball x₀ (r - ε))
⊢ LipschitzOnWith (2 * M / ε).toNNReal f (ball x₀ (r - ε))

Tactic:
set K := 2 * M / ε with hK
-- Module: Mathlib.Analysis.Convex.Continuous
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‖
inr : ∀ (hxy : x ≠ y), f x - f y ≤ K * ‖x - y‖
⊢ f x - f y ≤ K * ‖x - y‖

Tactic:
obtain rfl | hxy := eq_or_ne x y

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Convex.Continuous
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 : E
hx hy : x ∈ ball x₀ (r - ε)
⊢ f x - f x ≤ K * ‖x - x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Continuous
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
linarith : r < r - ε → 0 - ε + (r - (r - ε)) = 0
⊢ r - ε ≤ r

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Continuous
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
⊢ ball x₀ (r - ε) ⊆ ball x₀ r

Tactic:
have hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r := ball_subset_ball <| by linarith
-- Module: Mathlib.Analysis.Convex.Continuous
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
⊢ x ∈ ball x₀ r

Tactic:
have hx' : x ∈ ball x₀ r := hx₀r hx
-- Module: Mathlib.Analysis.Convex.Continuous
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
⊢ y ∈ ball x₀ r

Tactic:
have hy' : y ∈ ball x₀ r := hx₀r hy
-- Module: Mathlib.Analysis.Convex.Continuous
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)
rwa rwa₁ rwa₂ rwa₃ : x ≠ y
⊢ 0 < ‖x - y‖

Tactic:
rwa [norm_sub_pos_iff]

Premises used: norm_sub_pos_iff
-- Module: Mathlib.Analysis.Convex.Continuous
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)
⊢ 0 < ‖x - y‖

Tactic:
replace hxy : 0 < ‖x - y‖ := by rwa [norm_sub_pos_iff]
-- Module: Mathlib.Analysis.Convex.Continuous
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)‖

Tactic:
simp only [z, add_sub_right_comm]

Premises used: add_sub_right_comm
-- Module: Mathlib.Analysis.Convex.Continuous
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‖
⊢ ‖x - x₀ + (ε / ‖x - y‖) • (x - y)‖ ≤ ‖x - x₀‖ + ‖(ε / ‖x - y‖) • (x - y)‖

Tactic:
norm_add_le ..

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Convex.Continuous
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‖
⊢ ‖(ε / ‖x - y‖) • (x - y)‖ ≤ ε

Tactic:
simp [norm_smul, abs_of_nonneg, hε.le, hxy.ne']

Premises used: norm_smul, LT.lt.le, LT.lt.ne', abs_of_nonneg
-- Module: Mathlib.Analysis.Convex.Continuous
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‖
⊢ r - ε + ε = r

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Continuous
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)‖
_₁ : r - ε + ε = r
⊢ ‖z - x₀‖ < 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

Premises used: Norm.norm, HSub.hSub, norm_add_le, HDiv.hDiv, mem_ball_iff_norm, add_lt_add_of_lt_of_le, Iff.mp
-- Module: Mathlib.Analysis.Convex.Continuous
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 ∈ 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
-- Module: Mathlib.Analysis.Convex.Continuous
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‖)
⊢ a + b = 1

Tactic:
simp [field, a, b]
-- Module: Mathlib.Analysis.Convex.Continuous
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‖)
⊢ a + b = 1

Tactic:
have hab : a + b = 1 := by simp [field, a, b]
-- Module: Mathlib.Analysis.Convex.Continuous
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
rw rw₁ : x = x
⊢ x = a • x + b • x

Tactic:
rw [Convex.combo_self hab]

Premises used: Convex.combo_self
-- Module: Mathlib.Analysis.Convex.Continuous
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
simp :
  (ε / (ε + ‖x - y‖)) • x + (‖x - y‖ / (ε + ‖x - y‖)) • x =
    (ε / (ε + ‖x - y‖)) • y + ((‖x - y‖ / (ε + ‖x - y‖)) • x + ((ε / (ε + ‖x - y‖)) • x - (ε / (ε + ‖x - y‖)) • y))
⊢ a • x + b • x = a • y + b • z

Tactic:
simp [z, a, b, smul_smul, hxy.ne', smul_sub]

Premises used: smul_smul, LT.lt.ne', smul_sub
-- Module: Mathlib.Analysis.Convex.Continuous
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 - y‖)) • x + (‖x - y‖ / (ε + ‖x - y‖)) • x =
    (ε / (ε + ‖x - y‖)) • y + ((‖x - y‖ / (ε + ‖x - y‖)) • x + ((ε / (ε + ‖x - y‖)) • x - (ε / (ε + ‖x - y‖)) • y))

Tactic:
abel
-- Module: Mathlib.Analysis.Convex.Continuous
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 • x + b • x = a • y + b • z
⊢ 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
-- Module: Mathlib.Analysis.Convex.Continuous
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

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
-- Module: Mathlib.Analysis.Convex.Continuous
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
inr : ε * (f x - f y) ≤ ‖x - y‖ * (2 * M)
⊢ f x - f y ≤ K * ‖x - y‖

Tactic:
rw [hK, mul_comm, ← mul_div_assoc, le_div_iff₀' hε]

Premises used: le_div_iff₀', mul_div_assoc, mul_comm
-- Module: Mathlib.Analysis.Convex.Continuous
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
⊢ 0 ≤ a

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Continuous
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
⊢ 0 ≤ b

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Continuous
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 (a • y + b • z) ≤ a • f y + b • f z

Tactic:
have h := hf.2 hy' hz (by positivity) (by positivity) hab
-- Module: Mathlib.Analysis.Convex.Continuous
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 ≤ ε / (ε + ‖x - y‖) * f y + ‖x - y‖ / (ε + ‖x - y‖) * f z

Tactic:
simp only [← hxyz, smul_eq_mul, a, b] at h

Premises used: smul_eq_mul
-- Module: Mathlib.Analysis.Convex.Continuous
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 * (ε + ‖x - y‖) ≤ ε * f y + ‖x - y‖ * f z

Tactic:
field_simp at h