awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
a : Membership.mem (γ := Set F) (sphere 0 r) z
⊢ z ∈ U

Tactic:
apply hU_sub
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
⊢ Membership.mem (γ := Set F) (sphere 0 r) z

Tactic:
simp_all [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
⊢ z ∈ U

Tactic:
have hz : z ∈ U := by
    apply hU_sub
    simp_all [norm_smul]
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
⊢ 0 ≤ r⁻¹ * ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
⊢ (r⁻¹ * ‖x‖) • z ∈ U

Tactic:
have := StarConvex.smul_mem (hU.starConvex zero_mem) hz (by positivity) hr₁
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (‖x‖⁻¹ * ‖x‖) • x ∈ U
⊢ ‖x‖ ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₁ : ∀ (this : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₂ : ∀ (this : (r⁻¹ * ‖x‖ * (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₃ : ∀ (this : (r⁻¹ * ‖x‖ * r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₄ : ∀ (this : (‖x‖⁻¹ * (r⁻¹ * ‖x‖ * r)) • x ∈ U), x ∈ U
neg₅ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * r⁻¹ * r)) • x ∈ U), x ∈ U
neg₆ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * (r⁻¹ * r))) • x ∈ U), x ∈ U
neg₇ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * 1)) • x ∈ U), x ∈ U
neg₈ : ∀ (this : (‖x‖⁻¹ * ‖x‖) • x ∈ U), x ∈ U
neg₉ : ∀ (this : HSMul.hSMul (α := ℝ) 1 x ∈ U), x ∈ U
neg₁₀ neg₁₁ neg₁₂ neg₁₃ : ∀ (this : x ∈ U), x ∈ U
⊢ x ∈ U

Tactic:
rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this

Premises used: smul_assoc, mul_assoc, one_smul, Inv.inv, mul_comm, smul_eq_mul, mul_one, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
y : E
⊢ ∃ x' ∈ s, dist x y ≤ dist x' y

Tactic:
(convexOn_dist y (convex_convexHull ℝ _)).exists_ge_of_mem_convexHull (subset_convexHull ..) hx

Premises used: Real, ConvexOn.exists_ge_of_mem_convexHull, subset_convexHull, convexOn_dist, convex_convexHull
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
rw : Convex ℝ (s + ball 0 δ)
⊢ Convex ℝ (Metric.thickening δ s)

Tactic:
rw [← add_ball_zero]

Premises used: add_ball_zero
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (s + ball 0 δ)

Tactic:
hs.add (convex_ball 0 _)

Premises used: Convex.add, convex_ball, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (s + ball 0 δ)

Tactic:
exact hs.add (convex_ball 0 _)

Premises used: Convex.add, convex_ball, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
inl : ∀ (hδ : 0 ≤ δ), Convex ℝ (Metric.cthickening δ s)
inr : ∀ (hδ : δ ≤ 0), Convex ℝ (Metric.cthickening δ s)
⊢ Convex ℝ (Metric.cthickening δ s)

Tactic:
obtain hδ | hδ := le_total 0 δ

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
inl : Convex.{0, u_1} ℝ (E := E) (⋂ (ε : ℝ), ⋂ (_ : δ < ε), Metric.thickening ε s)
⊢ Convex ℝ (Metric.cthickening δ s)

Tactic:
rw [cthickening_eq_iInter_thickening hδ]

Premises used: Metric.cthickening_eq_iInter_thickening
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex.{0, u_1} ℝ (E := E) (⋂ (ε : ℝ), ⋂ (_ : δ < ε), Metric.thickening ε s)

Tactic:
convex_iInter₂ fun _ _ => hs.thickening _

Premises used: convex_iInter₂, Convex.thickening
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex.{0, u_1} ℝ (E := E) (⋂ (ε : ℝ), ⋂ (_ : δ < ε), Metric.thickening ε s)

Tactic:
exact convex_iInter₂ fun _ _ => hs.thickening _

Premises used: convex_iInter₂, Convex.thickening
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
inr : Convex ℝ (closure s)
⊢ Convex ℝ (Metric.cthickening δ s)

Tactic:
rw [cthickening_of_nonpos hδ]

Premises used: Metric.cthickening_of_nonpos
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (closure s)

Tactic:
hs.closure

Premises used: Convex.closure
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (closure s)

Tactic:
exact hs.closure

Premises used: Convex.closure
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set E
x y : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) y
rcases : ∀ (x' : E) (hx' : x' ∈ s) (Hx' : dist x y ≤ dist x' y), ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'

Tactic:
rcases convexHull_exists_dist_ge hx y with ⟨x', hx', Hx'⟩

Premises used: convexHull_exists_dist_ge
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set E
x y : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) y
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
rcases : ∀ (y' : E) (hy' : y' ∈ t) (Hy' : dist y x' ≤ dist y' x'), ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'

Tactic:
rcases convexHull_exists_dist_ge hy x' with ⟨y', hy', Hy'⟩

Premises used: convexHull_exists_dist_ge
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set E
x y : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) y
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
right : dist x y ≤ dist x' y'
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'

Tactic:
use x', hx', y', hy'
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set E
x y : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) y
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ dist x y ≤ dist x' y'

Tactic:
le_trans Hx' (dist_comm y x' ▸ dist_comm y' x' ▸ Hy')

Premises used: Eq.rec, dist_comm, le_trans
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set E
x y : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) y
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ dist x y ≤ dist x' y'

Tactic:
exact le_trans Hx' (dist_comm y x' ▸ dist_comm y' x' ▸ Hy')

Premises used: le_trans
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
⊢ ediam.{u_1} (X := E) ((convexHull ℝ : (a : Set E) → Set E) s) = ediam s

Tactic:
(ediam_le fun x hx y hy => ?_).antisymm (ediam_mono <| subset_convexHull ℝ s)

Premises used: Real, subset_convexHull, LE.le.antisymm, Metric.ediam_mono, Metric.ediam_le
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
refine :
  ∀ (x : E) (hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x) (y : E)
    (hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y), edist x y ≤ ediam s
⊢ ediam.{u_1} (X := E) ((convexHull ℝ : (a : Set E) → Set E) s) = ediam s

Tactic:
refine (ediam_le fun x hx y hy => ?_).antisymm (ediam_mono <| subset_convexHull ℝ s)

Premises used: Real, subset_convexHull, LE.le.antisymm, Metric.ediam_mono, Metric.ediam_le
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
y : E
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y
rcases : ∀ (x' : E) (hx' : x' ∈ s) (y' : E) (hy' : y' ∈ s) (H : dist x y ≤ dist x' y'), edist x y ≤ ediam s
⊢ edist x y ≤ ediam s

Tactic:
rcases convexHull_exists_dist_ge2 hx hy with ⟨x', hx', y', hy', H⟩

Premises used: convexHull_exists_dist_ge2
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
y : E
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
rw : ENNReal.ofReal (dist x y) ≤ ediam s
⊢ edist x y ≤ ediam s

Tactic:
rw [edist_dist]

Premises used: edist_dist
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
y : E
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
apply : ENNReal.ofReal (dist x' y') ≤ ediam s
⊢ ENNReal.ofReal (dist x y) ≤ ediam s

Tactic:
apply le_trans (ENNReal.ofReal_le_ofReal H)

Premises used: ENNReal.ofReal_le_ofReal, le_trans
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
y : E
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
rw : edist x' y' ≤ ediam s
⊢ ENNReal.ofReal (dist x' y') ≤ ediam s

Tactic:
rw [← edist_dist]

Premises used: edist_dist
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
y : E
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x' y' ≤ ediam s

Tactic:
edist_le_ediam_of_mem hx' hy'

Premises used: Metric.edist_le_ediam_of_mem
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
y : E
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x' y' ≤ ediam s

Tactic:
exact edist_le_ediam_of_mem hx' hy'

Premises used: Metric.edist_le_ediam_of_mem
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
⊢ diam.{u_1} (α := E) ((convexHull ℝ : (a : Set E) → Set E) s) = diam s

Tactic:
simp only [diam, convexHull_ediam]

Premises used: convexHull_ediam, Metric.diam
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
⊢ Bornology.IsBounded.{u_1} (α := E) ((convexHull ℝ : (a : Set E) → Set E) s) ↔ Bornology.IsBounded s

Tactic:
simp only [isBounded_iff_ediam_ne_top, convexHull_ediam]

Premises used: Metric.isBounded_iff_ediam_ne_top, convexHull_ediam
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
⊢ PathConnectedSpace E

Tactic:
IsTopologicalAddGroup.pathConnectedSpace

Premises used: IsTopologicalAddGroup.pathConnectedSpace
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
pos : ∀ (hx : x = 0), IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y}
neg : ∀ (hx : ¬x = 0), IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y}
⊢ IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y}

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : x = 0
⊢ IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y}

Tactic:
simpa [hx] using isConnected_univ (α := E)

Premises used: isConnected_univ
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ¬x = 0
neg : IsConnected.{u_1} (α := E) {y : E | ∃ (r : ℝ), 0 ≤ r ∧ r • x = y}
⊢ IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y}

Tactic:
simp_rw [← exists_nonneg_left_iff_sameRay hx]

Premises used: exists_nonneg_left_iff_sameRay
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ¬x = 0
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (r : ℝ) ↦ r • x) (Ici 0)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ¬x = 0
⊢ IsConnected.{u_1} (α := E) {y : E | ∃ (r : ℝ), 0 ≤ r ∧ r • x = y}

Tactic:
exact isConnected_Ici.image _ (by fun_prop)

Premises used: IsConnected.image, isConnected_Ici
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : x ≠ 0
simp_rw : IsConnected.{u_1} (α := E) {y : E | ∃ (r : ℝ), 0 < r ∧ r • x = y}
⊢ IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y ∧ y ≠ 0}

Tactic:
simp_rw [← exists_pos_left_iff_sameRay_and_ne_zero hx]

Premises used: exists_pos_left_iff_sameRay_and_ne_zero
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (r : ℝ) ↦ r • x) (Ioi 0)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ IsConnected.{u_1} (α := E) {y : E | ∃ (r : ℝ), 0 < r ∧ r • x = y}

Tactic:
exact isConnected_Ioi.image _ (by fun_prop)

Premises used: IsConnected.image, isConnected_Ioi
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y z : E
hy : y ∈ segment ℝ x z
⊢ Membership.mem (γ := Set E) ((fun (θ : ℝ) ↦ x + θ • (z - x)) '' Icc 0 1) y

Tactic:
rw [segment_eq_image'] at hy

Premises used: segment_eq_image'
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y z : E
hy : Membership.mem (γ := Set E) ((fun (θ : ℝ) ↦ x + θ • (z - x)) '' Icc 0 1) y
⊢ ∃ (x_1 : ℝ), (0 ≤ x_1 ∧ x_1 ≤ 1) ∧ x + x_1 • (z - x) = y

Tactic:
simp only [mem_image, mem_Icc] at hy

Premises used: Set.mem_image, Set.mem_Icc
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y z : E
hy : ∃ (x_1 : ℝ), (0 ≤ x_1 ∧ x_1 ≤ 1) ∧ x + x_1 • (z - x) = y
obtain : ∀ (u : ℝ) (hu_nonneg : 0 ≤ u) (hu_le_one : u ≤ 1), ‖x + u • (z - x) - x‖ ≤ ‖z - x‖
⊢ ‖y - x‖ ≤ ‖z - x‖

Tactic:
obtain ⟨u, ⟨hu_nonneg, hu_le_one⟩, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
u : ℝ
hu_nonneg : 0 ≤ u
hu_le_one : u ≤ 1
simp : |u| * ‖z - x‖ ≤ ‖z - x‖
⊢ ‖x + u • (z - x) - x‖ ≤ ‖z - x‖

Tactic:
simp only [add_sub_cancel_left, norm_smul, Real.norm_eq_abs]

Premises used: norm_smul, add_sub_cancel_left, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
u : ℝ
hu_nonneg : 0 ≤ u
hu_le_one : u ≤ 1
rw : u * ‖z - x‖ ≤ ‖z - x‖
⊢ |u| * ‖z - x‖ ≤ ‖z - x‖

Tactic:
rw [abs_of_nonneg hu_nonneg]

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
u : ℝ
hu_nonneg : 0 ≤ u
hu_le_one : u ≤ 1
rw : 1 * ‖z - x‖
| ‖z - x‖

Tactic:
rw [← one_mul (‖z - x‖)]

Premises used: Norm.norm, HSub.hSub, one_mul
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
u : ℝ
hu_nonneg : 0 ≤ u
hu_le_one : u ≤ 1
conv_rhs : u * ‖z - x‖ ≤ 1 * ‖z - x‖
⊢ u * ‖z - x‖ ≤ ‖z - x‖

Tactic:
conv_rhs => rw [← one_mul (‖z - x‖)]

Premises used: Norm.norm, HSub.hSub, one_mul
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
u : ℝ
hu_nonneg : 0 ≤ u
hu_le_one : u ≤ 1
ha : 0 ≤ ‖z - x‖
⊢ u * ‖z - x‖ ≤ 1 * ‖z - x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
obtain :
  ∀ (p : α → Prop) (hp : ∀ᶠ (i : α) in f, p i) (δ : ℝ) (hδ : δ > 0)
    (hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2),
    ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
obtain ⟨p, hp, δ, hδ, hr⟩ := eventually_prod_nhds_iff.mp hr

Premises used: Metric.eventually_prod_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr_1 : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
rw :
  ∀ (hy : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε) (hz : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε)
    (hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2) (p : α → Prop) (hp : ∀ᶠ (i : α) in f, p i) (δ : ℝ) (hδ : δ > 0)
    (hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2),
    ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
rw [Metric.tendsto_nhds] at hy hz

Premises used: Metric.tendsto_nhds
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε
hz : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε
hr_1 : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
h : ∀ (χ : α) (hp : p χ) (hy : dist (y χ) x < δ) (hz : dist (z χ) x < δ), ∀ v ∈ [y χ -[ℝ] z χ], r χ v
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
filter_upwards [hp, hy δ hδ, hz δ hδ] with χ hp hy hz
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy_1 : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε
hz_1 : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε
hr_1 : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp_1 : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
χ : α
hp : p χ
hy : dist (y χ) x < δ
hz : dist (z χ) x < δ
⊢ ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
fun v hv => hr hp <| convex_iff_segment_subset.mp (convex_ball x δ) hy hz hv

Premises used: convex_ball, Iff.mp, convex_iff_segment_subset
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy_1 : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε
hz_1 : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε
hr_1 : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp_1 : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
χ : α
hp : p χ
hy : dist (y χ) x < δ
hz : dist (z χ) x < δ
⊢ ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
exact fun v hv => hr hp <| convex_iff_segment_subset.mp (convex_ball x δ) hy hz hv

Premises used: convex_ball, Iff.mp, convex_iff_segment_subset