awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
this : ∀ (x' y' : E), x + y = x' + y' + (x - x') + (y - y')
⊢ ‖x' + y' + (x - x') + (y - y')‖ ≤ ‖x' + y'‖ + ‖x - x'‖ + ‖y - y'‖

Tactic:
norm_add₃_le

Premises used: norm_add₃_le
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
h₃ : ‖x' + y'‖ ≤ 2 - δ
h₄ : ‖x' - x‖ ≤ δ'
h₅ : ‖y' - y‖ ≤ δ'
⊢ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ ≤ 2 - δ + δ' + δ'

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖x' + y'‖ ≤ 2 - δ

Tactic:
h (h₁ _ hx') (h₁ _ hy') hxy'
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖x' - x‖ ≤ δ'

Tactic:
h₂ _ hx hx'.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖y' - y‖ ≤ δ'

Tactic:
h₂ _ hy hy'.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖x' + y'‖ ≤ 2 - δ

Tactic:
exacts [h (h₁ _ hx') (h₁ _ hy') hxy', h₂ _ hx hx'.le, h₂ _ hy hy'.le]

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
this : δ' ≤ δ / 3
linarith : 2 - δ' < 2 - δ + δ' + δ' → 3 / 3 = 1
linarith₁ : 2 - δ' < 2 - δ + δ' + δ' → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : 2 - δ' < 2 - δ + δ' + δ' → GT.gt (α := ℝ) 3 0
linarith₃ : 2 - δ' < 2 - δ + δ' + δ' → 3 / 3 = 1
linarith₄ : 2 - δ' < 2 - δ + δ' + δ' → HMul.hMul (α := ℝ) 1 3 = 3
linarith₅ : 2 - δ' < 2 - δ + δ' + δ' → GT.gt (α := ℝ) 3 0
linarith₆ : 2 - δ' < 2 - δ + δ' + δ' → 3 / 3 = 1
linarith₇ : 2 - δ' < 2 - δ + δ' + δ' → HMul.hMul (α := ℝ) 1 3 = 3
linarith₈ : 2 - δ' < 2 - δ + δ' + δ' → GT.gt (α := ℝ) 3 0
linarith₉ : 2 - δ' < 2 - δ + δ' + δ' → 3 * δ' - 1 * δ + (2 - δ' - (2 - δ + δ' + δ')) = 0
⊢ 2 - δ + δ' + δ' ≤ 2 - δ'

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
suffices : δ' ≤ δ / 3
⊢ 2 - δ + δ' + δ' ≤ 2 - δ'

Tactic:
suffices δ' ≤ δ / 3 by linarith
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ δ' ≤ δ / 3

Tactic:
min_le_of_right_le <| min_le_right _ _

Premises used: min_le_right, min_le_of_right_le
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ δ' ≤ δ / 3

Tactic:
exact min_le_of_right_le <| min_le_right _ _

Premises used: min_le_right, min_le_of_right_le
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
have : ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖
have₁ : ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ ≤ 2 - δ + δ' + δ'
have₂ : 2 - δ + δ' + δ' ≤ 2 - δ'
⊢ ‖x + y‖ ≤ 2 - δ'

Tactic:
calc
    ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ := by
      have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := fun _ _ => by abel
      rw [norm_sub_rev, norm_sub_rev y', this]
      exact norm_add₃_le
    _ ≤ 2 - δ + δ' + δ' := by
      gcongr
      exacts [h (h₁ _ hx') (h₁ _ hy') hxy', h₂ _ hx hx'.le, h₂ _ hy hy'.le]
    _ ≤ 2 - δ' := by
      suffices δ' ≤ δ / 3 by linarith
      exact min_le_of_right_le <| min_le_right _ _
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
inl : ∀ (hr : r ≤ 0), ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
inr : ∀ (hr : 0 < r), ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ

Tactic:
obtain hr | hr := le_or_gt r 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : r ≤ 0
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ

Tactic:
⟨1, one_pos, fun x hx y hy h => (hε.not_ge <|
      h.trans <| (norm_sub_le _ _).trans <| add_nonpos (hx.trans hr) (hy.trans hr)).elim⟩

Premises used: False.elim, norm_sub_le, add_nonpos, And.intro, Exists.intro, LE.le.trans, LT.lt.not_ge, OfNat.ofNat, one_pos
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : r ≤ 0
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ

Tactic:
exact ⟨1, one_pos, fun x hx y hy h => (hε.not_ge <|
      h.trans <| (norm_sub_le _ _).trans <| add_nonpos (hx.trans hr) (hy.trans hr)).elim⟩
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
inr :
  ∀ (δ : ℝ) (hδ : 0 < δ) (h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ),
    ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ

Tactic:
obtain ⟨δ, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (div_pos hε hr)

Premises used: div_pos, exists_forall_closed_ball_dist_add_le_two_sub
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ

Tactic:
⟨δ * r, mul_pos hδ hr, fun x hx y hy hxy => ?_⟩

Premises used: HMul.hMul, mul_pos, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
inr : ∀ (x : E) (hx : ‖x‖ ≤ r) (y : E) (hy : ‖y‖ ≤ r) (hxy : ε ≤ ‖x - y‖), ‖x + y‖ ≤ 2 * r - δ * r
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ

Tactic:
refine ⟨δ * r, mul_pos hδ hr, fun x hx y hy hxy => ?_⟩
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖x‖ ≤ r
y : E
hy : ‖y‖ ≤ r
hxy : ε ≤ ‖x - y‖
inr : ∀ (hx : ‖r⁻¹ • x‖ ≤ 1) (y : E) (hy : ‖r⁻¹ • y‖ ≤ 1) (hxy : ε ≤ ‖x - y‖), ‖x + y‖ ≤ 2 * r - δ * r
⊢ ‖x + y‖ ≤ 2 * r - δ * r

Tactic:
rw [← div_le_one hr, div_eq_inv_mul, ← norm_smul_of_nonneg (inv_nonneg.2 hr.le)] at hx hy

Premises used: Iff.mpr, norm_smul_of_nonneg, LT.lt.le, div_le_one, inv_nonneg, div_eq_inv_mul
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
⊢ ε / r ≤ ‖r⁻¹ • x - r⁻¹ • y‖ → ‖r⁻¹ • x + r⁻¹ • y‖ ≤ 2 - δ

Tactic:
have := h hx hy
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
this : ε / r ≤ ‖r⁻¹ • x - r⁻¹ • y‖ → ‖r⁻¹ • x + r⁻¹ • y‖ ≤ 2 - δ
⊢ ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ * r

Tactic:
simp_rw [← smul_add, ← smul_sub, norm_smul_of_nonneg (inv_nonneg.2 hr.le), ← div_eq_inv_mul,
    div_le_div_iff_of_pos_right hr, div_le_iff₀ hr, sub_mul] at this

Premises used: Iff.mpr, div_le_iff₀, norm_smul_of_nonneg, LT.lt.le, div_le_div_iff_of_pos_right, sub_mul, smul_sub, inv_nonneg, div_eq_inv_mul, smul_add
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
this : ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ * r
⊢ ‖x + y‖ ≤ 2 * r - δ * r

Tactic:
this hxy
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
this : ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ * r
⊢ ‖x + y‖ ≤ 2 * r - δ * r

Tactic:
exact this hxy
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : UniformConvexSpace E
⊢ StrictConvexSpace ℝ E

Tactic:
StrictConvexSpace.of_norm_add_ne_two fun _ _ hx hy hxy =>
    let ⟨_, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (norm_sub_pos_iff.2 hxy)
    ((h hx.le hy.le le_rfl).trans_lt <| sub_lt_self _ hδ).ne

Premises used: Iff.mpr, Norm.norm, _private.0.UniformConvexSpace.toStrictConvexSpace.match_1, StrictConvexSpace.of_norm_add_ne_two, le_rfl, sub_lt_self, Eq.le, Ne, HAdd.hAdd, OfNat.ofNat, LE.le.trans_lt, exists_forall_closed_ball_dist_add_le_two_sub, norm_sub_pos_iff, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
inst_5 : AddTorsor V P
s : Set P
x : P
⊢ IsVisible 𝕜 s x x

Tactic:
simp [IsVisible]

Premises used: IsVisible
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
inst_5 : AddTorsor V P
s : Set P
x y : P
⊢ IsVisible 𝕜 s x y ↔ IsVisible 𝕜 s y x

Tactic:
simp [IsVisible, sbtw_comm]

Premises used: IsVisible, sbtw_comm
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : AddCommGroup V
inst_3 : Module 𝕜 V
inst_4 : AddTorsor V P
s t : Set P
x y : P
hst : s ⊆ t
ht : IsVisible 𝕜 t x y
⊢ IsVisible 𝕜 s x y

Tactic:
fun _z hz ↦ ht <| hst hz

Premises used: IsVisible
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
inst_5 : AddTorsor V P
s : Set P
x y : P
hxy : x ≠ y
simp :
  (∀ ⦃z : P⦄, z ∈ s → ∀ (x_1 : 𝕜), 0 < x_1 → x_1 < 1 → ¬(lineMap x y : (a : 𝕜) → P) x_1 = z) ↔
    ∀ (δ : 𝕜), 0 < δ → δ < 1 → ((lineMap x y : (a : 𝕜) → P) δ : P) ∉ s
⊢ IsVisible 𝕜 s x y ↔ ∀ (δ : 𝕜), Membership.mem (γ := Set 𝕜) (Set.Ioo 0 1) δ → ((lineMap x y : (a : 𝕜) → P) δ : P) ∉ s

Tactic:
simp [IsVisible, sbtw_iff_mem_image_Ioo_and_ne, hxy]

Premises used: sbtw_iff_mem_image_Ioo_and_ne, IsVisible
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
inst_5 : AddTorsor V P
s : Set P
x y : P
hxy : x ≠ y
⊢ (∀ ⦃z : P⦄, z ∈ s → ∀ (x_1 : 𝕜), 0 < x_1 → x_1 < 1 → ¬(lineMap x y : (a : 𝕜) → P) x_1 = z) ↔
    ∀ (δ : 𝕜), 0 < δ → δ < 1 → ((lineMap x y : (a : 𝕜) → P) δ : P) ∉ s

Tactic:
aesop
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi : 0 < w i
⊢ w i = 1 ∨ w i < 1

Tactic:
eq_or_lt_of_le <| (single_le_sum hw₀ hi).trans_eq hw₁

Premises used: LE.le.trans_eq, eq_or_lt_of_le, Finset.single_le_sum
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi : 0 < w i
inl : ∀ (hwi : w i = 1), IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
inr : ∀ (hwi : w i < 1), IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
⊢ IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)

Tactic:
obtain hwi | hwi : w i = 1 ∨ w i < 1 := eq_or_lt_of_le <| (single_le_sum hw₀ hi).trans_eq hw₁

Premises used: LE.le.trans_eq, eq_or_lt_of_le, Finset.single_le_sum
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
⊢ IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)

Tactic:
hw
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
h : a i = ∑ i ∈ t, w i • a i
⊢ IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)

Tactic:
convert! hw
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
h : ∑ i ∈ t, w i • a i = w i • a i
⊢ a i = ∑ i ∈ t, w i • a i

Tactic:
rw [← one_smul 𝕜 (a i), ← hwi, eq_comm]

Premises used: eq_comm, one_smul
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
⊢ ∀ i_1 ∈ t.erase i, w i_1 = 0

Tactic:
rw [← hwi, ← sub_eq_zero, ← sum_erase_eq_sub hi,
      sum_eq_zero_iff_of_nonneg fun j hj ↦ hw₀ _ <| erase_subset _ _ hj] at hw₁

Premises used: sub_eq_zero, Finset.sum_eq_zero_iff_of_nonneg, Finset.sum_erase_eq_sub, Finset.erase_subset
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
hw₂ : ∀ i_1 ∈ t.erase i, w i_1 = 0
⊢ i ∈ t

Tactic:
rw [← hwi, ← sub_eq_zero, ← sum_erase_eq_sub hi,
      sum_eq_zero_iff_of_nonneg fun j hj ↦ hw₀ _ <| erase_subset _ _ hj] at hw₁

Premises used: sub_eq_zero, Finset.sum_eq_zero_iff_of_nonneg, Finset.sum_erase_eq_sub, Finset.erase_subset
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
hw₂ : ∀ i_1 ∈ t.erase i, w i_1 = 0
hi₁ : i ∈ t
⊢ 0 < w i

Tactic:
rw [← hwi, ← sub_eq_zero, ← sum_erase_eq_sub hi,
      sum_eq_zero_iff_of_nonneg fun j hj ↦ hw₀ _ <| erase_subset _ _ hj] at hw₁

Premises used: sub_eq_zero, Finset.sum_eq_zero_iff_of_nonneg, Finset.sum_erase_eq_sub, Finset.erase_subset
-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
hw₂ : ∀ i_1 ∈ t.erase i, w i_1 = 0
hi₁ : i ∈ t
hwi₁ : 0 < w i
⊢ w i = 1

Tactic:
rw [← hwi, ← sub_eq_zero, ← sum_erase_eq_sub hi,
      sum_eq_zero_iff_of_nonneg fun j hj ↦ hw₀ _ <| erase_subset _ _ hj] at hw₁

Premises used: sub_eq_zero, Finset.sum_eq_zero_iff_of_nonneg, Finset.sum_erase_eq_sub, Finset.erase_subset