awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
⊢ 0 < ε'

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
⊢ 0 < ε'

Tactic:
have hε' : 0 < ε' := by positivity
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
⊢ 0 < ε / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
⊢ 0 < ε / 2

Tactic:
have hε₀ : 0 < ε / 2 := by positivity
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
simp : ∀ (y : Fin (finrank ℝ E + 1)), ε' * norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) y : E) ≤ ε / 2
⊢ Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) (closedBall 0 (ε / 2))

Tactic:
simp [d, abs_of_nonneg hε'.le, range_subset_iff, norm_smul]

Premises used: norm_smul, LT.lt.le, abs_of_nonneg, Set.range_subset_iff
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
⊢ ∀ (y : Fin (finrank ℝ E + 1)), ε' * norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) y : E) ≤ ε / 2

Tactic:
simpa [ε', hε₀.ne', range_subset_iff, ← mul_div_right_comm (ε / 2), div_le_iff₀ hc', hε₀]
      using hcnorm

Premises used: div_le_iff₀, HDiv.hDiv, mul_div_right_comm, LT.lt.ne', Set.range_subset_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
⊢ Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) (closedBall 0 (ε / 2))

Tactic:
have hdnorm : (range d : Set E) ⊆ closedBall 0 (ε / 2) := by
    simp [d, abs_of_nonneg hε'.le, range_subset_iff, norm_smul]
    simpa [ε', hε₀.ne', range_subset_iff, ← mul_div_right_comm (ε / 2), div_le_iff₀ hc', hε₀]
      using hcnorm
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) (closedBall 0 (ε / 2))
⊢ ∃ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
    Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        0 ∧
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        s

Tactic:
⟨d, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) (closedBall 0 (ε / 2))
refine_1 :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E))))
    0
refine_2 :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ s
⊢ ∃ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
    Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        0 ∧
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        s

Tactic:
refine ⟨d, ?_, ?_⟩
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) (closedBall 0 (ε / 2))
⊢ Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E))))
    0

Tactic:
simpa [d, Pi.smul_def, range_smul, interior_smul₀, convexHull_smul, zero_mem_smul_set_iff,
      hε'.ne']

Premises used: interior_smul₀, Set.zero_mem_smul_set_iff, LT.lt.ne', Set.range_smul, convexHull_smul, Pi.smul_def
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) (closedBall 0 (ε / 2))
⊢ Subset (α := Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) :
      Set E)
    (closedBall 0 (ε / 2) : Set E)

Tactic:
convexHull_min hdnorm (convex_closedBall ..)

Premises used: convexHull_min, convex_closedBall
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) (closedBall 0 (ε / 2))
linarith : ε ≤ ε / 2 → 2 / 2 = 1
linarith₁ : ε ≤ ε / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε ≤ ε / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : ε ≤ ε / 2 → 2 / 2 = 1
linarith₄ : ε ≤ ε / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : ε ≤ ε / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : ε ≤ ε / 2 → 0 - ε + (2 * ε - 1 * ε) = 0
⊢ ε / 2 < ε

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) (closedBall 0 (ε / 2))
⊢ ball 0 ε ⊆ s

Tactic:
hεs
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
s_1 : Set E_1
x : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E :=
  HVAdd.hVAdd (α := E)
    (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b
hc₀ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0
cnorm : ℝ :=
  Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)
hcnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm :
  Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) (closedBall 0 (ε / 2))
⊢ (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ s

Tactic:
calc
      convexHull ℝ (range d) ⊆ closedBall 0 (ε / 2) := convexHull_min hdnorm (convex_closedBall ..)
      _ ⊆ ball 0 ε := closedBall_subset_ball (by linarith)
      _ ⊆ s := hεs

Premises used: Real, Metric.closedBall_subset_ball, HDiv.hDiv, Metric.ball, convexHull, convexHull_min, Set.range, Metric.closedBall, OfNat.ofNat, DFunLike.coe, convex_closedBall
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
rcases :
  ∀ (U : Set E) (hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hU₂ : s ⊆ U) (hU₃ : U ⊆ t),
    ∃ (u : Finset E),
      s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
        (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t

Tactic:
rcases mem_nhdsSet_iff_exists.1 ht with ⟨U, hU₁, hU₂, hU₃⟩

Premises used: mem_nhdsSet_iff_exists, Iff.mp
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
rcases :
  ∀ (V : Set E) (hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V) (hV₂ : V + s ⊆ U),
    ∃ (u : Finset E),
      s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
        (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t

Tactic:
rcases compact_open_separated_add_left hs₂ hU₁ hU₂ with ⟨V, hV₁, hV₂⟩

Premises used: compact_open_separated_add_left
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
rcases :
  ∀ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E)
    (hb₁ :
      Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        0)
    (hb₂ :
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        V),
    ∃ (u : Finset E),
      s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
        (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t

Tactic:
rcases exists_mem_interior_convexHull_affineBasis hV₁ with ⟨b, hb₁, hb₂⟩

Premises used: exists_mem_interior_convexHull_affineBasis