awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
f : V →ᴬ[𝕜] W
⊢ Eq (α := V →L[𝕜] W) ((toConstProdContinuousLinearMap 𝕜 V W : (a : V →ᴬ[𝕜] W) → W × (V →L[𝕜] W)) f).2 f.contLinear

Tactic:
rfl

Premises used: ContinuousAffineMap.contLinear, rfl
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
x y z : P
h : Wbtw ℝ x y z
obtain :
  ∀ (a : ℝ) (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1),
    dist x ((AffineMap.lineMap x z : (a : ℝ) → P) a) + dist ((AffineMap.lineMap x z : (a : ℝ) → P) a) z = dist x z
⊢ dist x y + dist y z = dist x z

Tactic:
obtain ⟨a, ⟨ha₀, ha₁⟩, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
x z : P
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ dist x ((AffineMap.lineMap x z : (a : ℝ) → P) a) + dist ((AffineMap.lineMap x z : (a : ℝ) → P) a) z = dist x z

Tactic:
simp [abs_of_nonneg, ha₀, ha₁, sub_mul]

Premises used: sub_mul, abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y z : E
h : y ∈ [x -[ℝ] z]
⊢ dist x y + dist y z = dist x z

Tactic:
(mem_segment_iff_wbtw.1 h).dist_add_dist

Premises used: Wbtw.dist_add_dist, mem_segment_iff_wbtw, 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 : Set E
x : E
hs : s ∈ 𝓝 x
inr :
  ∀
    (this :
      ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
        {x : E} (hs : s ∈ 𝓝 x) (hx : x = 0),
        ∃ (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))))
              x ∧
            (convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
              s)
    (hx : ¬x = 0),
    ∃ (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))))
          x ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
          s
wlog :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E}
    (hs : s ∈ 𝓝 x) (hx : x = 0),
    ∃ (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))))
          x ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (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))))
        x ∧
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        s

Tactic:
wlog hx : x = 0
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E}
    (hs : s ∈ 𝓝 x) (hx : x = 0),
    ∃ (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))))
          x ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
          s
hx : ¬x = 0
⊢ Membership.mem (γ := Filter E) (𝓝 0) (-x +ᵥ s)

Tactic:
simpa using vadd_mem_nhds_vadd (-x) hs

Premises used: vadd_mem_nhds_vadd, Neg.neg
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E}
    (hs : s ∈ 𝓝 x) (hx : x = 0),
    ∃ (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))))
          x ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
          s
hx : ¬x = 0
inr :
  ∀ (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 ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
          -x +ᵥ 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))))
          x ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (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))))
        x ∧
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        s

Tactic:
obtain ⟨b, hb⟩ := this (s := -x +ᵥ s) (by simpa using vadd_mem_nhds_vadd (-x) hs) rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E}
    (hs : s ∈ 𝓝 x) (hx : x = 0),
    ∃ (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))))
          x ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
          s
hx : ¬x = 0
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 ∧
    (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
      -x +ᵥ s
h :
  Membership.mem (γ := Set E)
      (interior
        ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑(x +ᵥ b) : (a : Fin (finrank ℝ E + 1)) → E))))
      x ∧
    (convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑(x +ᵥ b) : (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))))
        x ∧
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        s

Tactic:
use x +ᵥ b
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E}
    (hs : s ∈ 𝓝 x) (hx : x = 0),
    ∃ (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))))
          x ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
          s
hx : ¬x = 0
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 ∧
    (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
      -x +ᵥ s
⊢ Membership.mem (γ := Set E)
      (interior
        ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑(x +ᵥ b) : (a : Fin (finrank ℝ E + 1)) → E))))
      x ∧
    (convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑(x +ᵥ b) : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
      s

Tactic:
simpa [subset_vadd_set_iff, mem_vadd_set_iff_neg_vadd_mem, convexHull_vadd, interior_vadd,
      Pi.vadd_def, -vadd_eq_add, vadd_eq_add (a := -x), ← Set.vadd_set_range] using hb

Premises used: Set.vadd_set_range, convexHull_vadd, Pi.vadd_def, interior_vadd, vadd_eq_add, Set.subset_vadd_set_iff, Set.mem_vadd_set_iff_neg_vadd_mem, Neg.neg
-- 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_1 : E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
hx : x = 0
subst :
  ∀ (hs : Membership.mem (γ := Filter E) (𝓝 0) 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
⊢ ∃ (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))))
        x ∧
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        s

Tactic:
subst hx
-- 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
⊢ Fintype.card (Fin (finrank ℝ E + 1)) = finrank ℝ E + 1

Tactic:
simp
-- 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
obtain :
  ∀ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
    ∃ (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
⊢ ∃ (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:
obtain ⟨b⟩ := exists_affineBasis_of_finiteDimensional
    (ι := Fin (finrank ℝ E + 1)) (k := ℝ) (P := E) (by simp)

Premises used: AffineBasis.exists_affineBasis_of_finiteDimensional
-- 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
⊢ Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0

Tactic:
simpa [c, convexHull_vadd, interior_vadd, range_add, Pi.vadd_def, mem_vadd_set_iff_neg_vadd_mem]
      using b.centroid_mem_interior_convexHull

Premises used: convexHull_vadd, Pi.vadd_def, interior_vadd, Set.range_add, AffineBasis.centroid_mem_interior_convexHull, Set.mem_vadd_set_iff_neg_vadd_mem
-- 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
⊢ Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
    0

Tactic:
have hc₀ : 0 ∈ interior (convexHull ℝ (range c) : Set E) := by
    simpa [c, convexHull_vadd, interior_vadd, range_add, Pi.vadd_def, mem_vadd_set_iff_neg_vadd_mem]
      using b.centroid_mem_interior_convexHull
-- 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)
i : Fin (finrank ℝ E + 1)
⊢ Membership.mem (γ := Finset (Fin (finrank ℝ E + 1))) Finset.univ i ∧
    norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E) - 1 ≤
      norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E)

Tactic:
simp
-- 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)
⊢ Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))

Tactic:
simpa only [cnorm, subset_def, Finset.mem_coe, mem_closedBall, dist_zero_right,
      ← sub_le_iff_le_add, Finset.le_sup'_iff, forall_mem_range] using fun i ↦ ⟨i, by simp⟩

Premises used: Finset.le_sup'_iff, Set.forall_mem_range, Set.subset_def, sub_le_iff_le_add, Metric.mem_closedBall, dist_zero_right, Finset.mem_coe
-- 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)
⊢ Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
    (closedBall 0 (cnorm + 1))

Tactic:
have hcnorm : range c ⊆ closedBall 0 (cnorm + 1) := by
    simpa only [cnorm, subset_def, Finset.mem_coe, mem_closedBall, dist_zero_right,
      ← sub_le_iff_le_add, Finset.le_sup'_iff, forall_mem_range] using fun i ↦ ⟨i, by simp⟩
-- 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))
obtain :
  ∀ (ε : ℝ) (hε : ε > 0) (hεs : ball 0 ε ⊆ 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
⊢ ∃ (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:
obtain ⟨ε, hε, hεs⟩ := Metric.mem_nhds_iff.1 hs

Premises used: Metric.mem_nhds_iff, Iff.mp
-- 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)
⊢ 0 ≤ cnorm

Tactic:
have : 0 ≤ cnorm := Finset.le_sup'_of_le _ (Finset.mem_univ 0) (norm_nonneg _)
-- 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)
this : 0 ≤ cnorm
⊢ 0 < cnorm + 1

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)
⊢ 0 < cnorm + 1

Tactic:
have hc' : 0 < cnorm + 1 := by
    have : 0 ≤ cnorm := Finset.le_sup'_of_le _ (Finset.mem_univ 0) (norm_nonneg _)
    positivity