awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
carrier : Set V
convex' : Convex ℝ carrier
isCompact' : IsCompact carrier
nonempty' : carrier.Nonempty
carrier_1 : Set V
convex'_1 : Convex ℝ carrier_1
isCompact'_1 : IsCompact carrier_1
nonempty'_1 : carrier_1.Nonempty
h :
  { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' : ConvexBody V }.carrier =
    { carrier := carrier_1, convex' := convex'_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 :
        ConvexBody V }.carrier
⊢ { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' : ConvexBody V } =
    { carrier := carrier_1, convex' := convex'_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
⊢ Convex ℝ (↑K : Set V)

Tactic:
K.convex'

Premises used: ConvexBody.convex'
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
⊢ IsCompact (↑K : Set V)

Tactic:
K.isCompact'

Premises used: ConvexBody.isCompact'
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : T2Space V
K : ConvexBody V
⊢ IsClosed[inst] (↑K : Set V)

Tactic:
K.isCompact.isClosed

Premises used: ConvexBody.isCompact, IsCompact.isClosed
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
⊢ (↑K : Set V).Nonempty

Tactic:
K.nonempty'

Premises used: ConvexBody.nonempty'
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K L : ConvexBody V
h : (↑K : Set V) = (↑L : Set V)
⊢ K = L

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
s : Set V
h₁ : Convex ℝ s
h₂ : IsCompact s
h₃ : s.Nonempty
⊢ (↑{ carrier := s, convex' := h₁, isCompact' := h₂, nonempty' := h₃ : ConvexBody V } : Set V) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
obtain : ∀ (x : V) (hx : x ∈ (↑K : Set V)), 0 ∈ K
⊢ 0 ∈ K

Tactic:
obtain ⟨x, hx⟩ := K.nonempty

Premises used: ConvexBody.nonempty
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
⊢ 0 = (1 / 2) • x + (1 / 2) • -x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
rw : (1 / 2) • x + (1 / 2) • -x ∈ K
⊢ 0 ∈ K

Tactic:
rw [show 0 = (1 / 2 : ℝ) • x + (1 / 2 : ℝ) • (-x) by simp]
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
a a₁ : 0 < 1 / 2
a₂ : 1 / 2 + 1 / 2 = 1
⊢ (1 / 2) • x + (1 / 2) • -x ∈ K

Tactic:
apply convex_iff_forall_pos.mp K.convex hx (h_symm x hx)

Premises used: ConvexBody.convex, Iff.mp, convex_iff_forall_pos
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
linarith : 1 / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : 1 / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 / 2 ≤ 0 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
⊢ 0 < 1 / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
linarith : 1 / 2 + 1 / 2 < 1 → HMul.hMul (α := ℝ) 1 0 = 0
linarith₁ : 1 < 1 / 2 + 1 / 2 → HMul.hMul (α := ℝ) 1 0 = 0
⊢ 1 / 2 + 1 / 2 = 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
⊢ (↑0 : Set V) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousAdd V
K L : ConvexBody V
⊢ (↑(K + L) : Set V) = (↑K : Set V) + (↑L : Set V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
c : ℝ
K : ConvexBody V
⊢ (↑(c • K) : Set V) = c • (↑K : Set V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
c : ℝ≥0
K : ConvexBody V
⊢ (↑(c • K) : Set V) = c • (↑K : Set V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
inl : ∀ (h : 0 ≤ b), HSMul.hSMul (α := ℝ≥0) 0 (↑K : Set V) ⊆ b • (↑K : Set V)
inr : ∀ (ha : 0 < a), a • (↑K : Set V) ⊆ b • (↑K : Set V)
⊢ a • (↑K : Set V) ⊆ b • (↑K : Set V)

Tactic:
obtain rfl | ha := eq_zero_or_pos a

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
inl : 0 ∈ b • (↑K : Set V)
⊢ HSMul.hSMul (α := ℝ≥0) 0 (↑K : Set V) ⊆ b • (↑K : Set V)

Tactic:
rw [Set.zero_smul_set K.nonempty, Set.zero_subset]

Premises used: Set.zero_smul_set, Set.zero_subset, ConvexBody.nonempty
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
⊢ 0 ∈ b • (↑K : Set V)

Tactic:
Set.mem_smul_set.mpr ⟨0, h_zero, smul_zero _⟩

Premises used: Iff.mpr, Set.Mem, Set.mem_smul_set, smul_zero, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
⊢ 0 ∈ b • (↑K : Set V)

Tactic:
exact Set.mem_smul_set.mpr ⟨0, h_zero, smul_zero _⟩

Premises used: Iff.mpr, Set.mem_smul_set, smul_zero, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
x : V
hx : x ∈ a • (↑K : Set V)
inr : ∀ (y : V) (hy : y ∈ (↑K : Set V)) (hx : a • y ∈ a • (↑K : Set V)), a • y ∈ b • (↑K : Set V)
⊢ x ∈ b • (↑K : Set V)

Tactic:
obtain ⟨y, hy, rfl⟩ := Set.mem_smul_set.mp hx

Premises used: Set.mem_smul_set, Iff.mp, rfl
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ (↑K : Set V)
hx : a • y ∈ a • (↑K : Set V)
inr : y ∈ (a⁻¹ * b) • (↑K : Set V)
⊢ a • y ∈ b • (↑K : Set V)

Tactic:
rw [← Set.mem_inv_smul_set_iff₀ ha.ne', smul_smul]

Premises used: Set.mem_inv_smul_set_iff₀, smul_smul, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ (↑K : Set V)
hx : a • y ∈ a • (↑K : Set V)
⊢ y ∈ (a⁻¹ * b) • (↑K : Set V)

Tactic:
Convex.mem_smul_of_zero_mem K.convex h_zero hy (?_ : 1 ≤ a⁻¹ * b)

Premises used: Set.Mem, ConvexBody.convex, Convex.mem_smul_of_zero_mem
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ (↑K : Set V)
hx : a • y ∈ a • (↑K : Set V)
inr : 1 ≤ a⁻¹ * b
⊢ y ∈ (a⁻¹ * b) • (↑K : Set V)

Tactic:
refine Convex.mem_smul_of_zero_mem K.convex h_zero hy (?_ : 1 ≤ a⁻¹ * b)

Premises used: ConvexBody.convex, Convex.mem_smul_of_zero_mem
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ (↑K : Set V)
hx : a • y ∈ a • (↑K : Set V)
inr : a * 1 ≤ b
inr₁ inr₂ inr₃ inr₄ : a ≤ b
⊢ 1 ≤ a⁻¹ * b

Tactic:
rwa [le_inv_mul_iff₀ ha, mul_one]

Premises used: le_inv_mul_iff₀, mul_one
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
K : ConvexBody V
⊢ Bornology.IsBounded (↑K : Set V)

Tactic:
K.isCompact.isBounded

Premises used: IsCompact.isBounded, ConvexBody.isCompact
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
K L : ConvexBody V
⊢ Metric.hausdorffEDist (↑K : Set V) (↑L : Set V) ≠ ⊤

Tactic:
apply_rules [Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded, ConvexBody.nonempty,
    ConvexBody.isBounded]

Premises used: Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded, ConvexBody.isBounded, ConvexBody.nonempty
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
K L : ConvexBody V
⊢ Metric.hausdorffDist (↑K : Set V) (↑L : Set V) = dist K L

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
K L : ConvexBody V
rw : Metric.hausdorffEDist (↑K : Set V) (↑L : Set V) = ENNReal.ofReal (dist K L)
⊢ Metric.hausdorffEDist (↑K : Set V) (↑L : Set V) = edist K L

Tactic:
rw [edist_dist]

Premises used: edist_dist
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
K L : ConvexBody V
⊢ Metric.hausdorffEDist (↑K : Set V) (↑L : Set V) = ENNReal.ofReal (dist K L)

Tactic:
(ENNReal.ofReal_toReal hausdorffEDist_ne_top).symm

Premises used: Metric.hausdorffDist, ENNReal.ofReal_toReal, ENNReal.toReal, ConvexBody.hausdorffEDist_ne_top, Eq.symm, NNReal.toReal
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
K L : ConvexBody V
⊢ Metric.hausdorffEDist (↑K : Set V) (↑L : Set V) = ENNReal.ofReal (dist K L)

Tactic:
exact (ENNReal.ofReal_toReal hausdorffEDist_ne_top).symm

Premises used: ENNReal.ofReal_toReal, ConvexBody.hausdorffEDist_ne_top, Eq.symm
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
h : ∀ (x : V), Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x ↔ x ∈ (↑K : Set V)
⊢ ⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V) = (↑K : Set V)

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
⊢ Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x ↔ x ∈ (↑K : Set V)

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : ∀ (h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x), x ∈ (↑K : Set V)
h₁ : ∀ (h : x ∈ (↑K : Set V)), Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
⊢ Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x ↔ x ∈ (↑K : Set V)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
h₁ : ∀ (C : ℝ) (hC_pos : C > 0) (hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C), x ∈ (↑K : Set V)
⊢ x ∈ (↑K : Set V)

Tactic:
obtain ⟨C, hC_pos, hC_bdd⟩ := K.isBounded.exists_pos_norm_le

Premises used: ConvexBody.isBounded, Bornology.IsBounded.exists_pos_norm_le
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
h₁ : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε
⊢ x ∈ (↑K : Set V)

Tactic:
rw [← K.isClosed.closure_eq, SeminormedAddCommGroup.mem_closure_iff]

Premises used: IsClosed.closure_eq, SeminormedAddCommGroup.mem_closure_iff, ConvexBody.isClosed
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
h₁ :
  ∀ (hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε) (x : V)
    (h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x) (C : ℝ) (hC_pos : C > 0)
    (hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C) (ε : ℝ), 0 < ε → ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε

Tactic:
rw [← NNReal.tendsto_coe, NormedAddCommGroup.tendsto_atTop] at hu

Premises used: NormedAddCommGroup.tendsto_atTop, NNReal.tendsto_coe
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
x : V
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
h₁ : ∀ (n : ℕ) (hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C), ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε
⊢ ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε

Tactic:
obtain ⟨n, hn⟩ := hu (ε / C) (div_pos hε hC_pos)

Premises used: HDiv.hDiv, div_pos
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
x : V
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
h₁ :
  ∀ (y : V) (hyK : y ∈ (↑K : Set V))
    (h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)),
    ∃ b ∈ (↑K : Set V), ‖(1 + (↑(u n) : ℝ)) • y - b‖ < ε
⊢ ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε

Tactic:
obtain ⟨y, hyK, rfl⟩ := Set.mem_smul_set.mp (Set.mem_iInter.mp h n)

Premises used: Set.mem_smul_set, Set.mem_iInter, Iff.mp, rfl
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
⊢ ∃ b ∈ (↑K : Set V), ‖(1 + (↑(u n) : ℝ)) • y - b‖ < ε

Tactic:
⟨y, hyK, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
h₁ : ‖(1 + (↑(u n) : ℝ)) • y - y‖ < ε
⊢ ∃ b ∈ (↑K : Set V), ‖(1 + (↑(u n) : ℝ)) • y - b‖ < ε

Tactic:
refine ⟨y, hyK, ?_⟩
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
rw : HSMul.hSMul (α := ℝ) 1 y + (↑(u n) : ℝ) • y - y = (↑(u n) : ℝ) • y
rw₁ : y + (↑(u n) : ℝ) • y - y = (↑(u n) : ℝ) • y
rw₂ rw₃ : (↑(u n) : ℝ) • y = (↑(u n) : ℝ) • y
⊢ (1 + (↑(u n) : ℝ)) • y - y = (↑(u n) : ℝ) • y

Tactic:
rw [add_smul, one_smul, add_sub_cancel_left]

Premises used: add_sub_cancel_left, one_smul, add_smul
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
h₁ : |(↑(u n) : ℝ)| * ‖y‖ < ε
⊢ ‖(1 + (↑(u n) : ℝ)) • y - y‖ < ε

Tactic:
rw [show (1 + u n : ℝ) • y - y = (u n : ℝ) • y by rw [add_smul, one_smul, add_sub_cancel_left],
      norm_smul, Real.norm_eq_abs]

Premises used: norm_smul, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
⊢ ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε / C

Tactic:
specialize hn n le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
hn : ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε / C
⊢ |(↑(u n) : ℝ)| * C < ε

Tactic:
rw [lt_div_iff₀' hC_pos, mul_comm, NNReal.coe_zero, sub_zero, Real.norm_eq_abs] at hn

Premises used: lt_div_iff₀', sub_zero, NNReal.coe_zero, mul_comm, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
hn : |(↑(u n) : ℝ)| * C < ε
⊢ |(↑(u n) : ℝ)| * ‖y‖ < ε

Tactic:
lt_of_le_of_lt ?_ hn

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
hn : |(↑(u n) : ℝ)| * C < ε
h₁ : |(↑(u n) : ℝ)| * ‖y‖ ≤ |(↑(u n) : ℝ)| * C
⊢ |(↑(u n) : ℝ)| * ‖y‖ < ε

Tactic:
refine lt_of_le_of_lt ?_ hn

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
hn : |(↑(u n) : ℝ)| * C < ε
h₁ : ‖y‖ ≤ C
⊢ |(↑(u n) : ℝ)| * ‖y‖ ≤ |(↑(u n) : ℝ)| * C

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
hn : |(↑(u n) : ℝ)| * C < ε
⊢ ‖y‖ ≤ C

Tactic:
hC_bdd _ hyK
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
hn : |(↑(u n) : ℝ)| * C < ε
⊢ ‖y‖ ≤ C

Tactic:
exact hC_bdd _ hyK
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ (↑K : Set V)
⊢ Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x

Tactic:
Set.mem_iInter.mpr (fun n => Convex.mem_smul_of_zero_mem K.convex h_zero h ?_)

Premises used: Iff.mpr, ConvexBody.convex, Set.mem_iInter, Convex.mem_smul_of_zero_mem
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ (↑K : Set V)
h₁ : ∀ (n : ℕ), 1 ≤ 1 + (↑(u n) : ℝ)
⊢ Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x

Tactic:
refine Set.mem_iInter.mpr (fun n => Convex.mem_smul_of_zero_mem K.convex h_zero h ?_)

Premises used: Iff.mpr, ConvexBody.convex, Set.mem_iInter, Convex.mem_smul_of_zero_mem