awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖f‖ * ‖g‖ ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have rw : 0 ≤ norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
Tactic: rw [le_add_iff_nonneg_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ norm (E := W₂ →L[𝕜] W) (f.comp g).contLinear ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have _ : norm (E := V →L[𝕜] W) f.contLinear * norm (E := W₂ →L[𝕜] V) g.contLinear ≤ ‖f‖ * ‖g‖
Tactic: calc
      ‖(f.comp g).contLinear‖ ≤ ‖f.contLinear‖ * ‖g.contLinear‖ :=
        (g.comp_contLinear f).symm ▸ f.contLinear.opNorm_comp_le _
      _ ≤ ‖f‖ * ‖g‖ := by grw [f.norm_contLinear_le, g.norm_contLinear_le]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by rw [le_add_iff_nonneg_right]; apply norm_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
_ : norm (E := V →L[𝕜] W) f.contLinear * norm (E := W₂ →L[𝕜] V) g.contLinear ≤ ‖f‖ * ‖g‖
⊢ norm (E := W₂ →L[𝕜] W) (f.comp g).contLinear ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have _₁ : ‖f‖ * ‖g‖ ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
Tactic: calc
      ‖(f.comp g).contLinear‖ ≤ ‖f.contLinear‖ * ‖g.contLinear‖ :=
        (g.comp_contLinear f).symm ▸ f.contLinear.opNorm_comp_le _
      _ ≤ ‖f‖ * ‖g‖ := by grw [f.norm_contLinear_le, g.norm_contLinear_le]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by rw [le_add_iff_nonneg_right]; apply norm_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (goal)
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
⊢ dist x y + dist y z = dist x z
have 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
Tactic: obtain ⟨a, ⟨ha₀, ha₁⟩, rfl⟩ := h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
⊢ ∃ (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
have 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
Tactic: wlog hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (goal)
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
⊢ ∃ (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
have 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
Tactic: wlog hx : x = 0
Cleared hypotheses: inst_2, hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (goal)
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),
    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
have 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
Tactic: obtain ⟨b, hb⟩ := this (s := -x +ᵥ s) (by simpa using vadd_mem_nhds_vadd (-x) hs) rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (goal)
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
⊢ ∃ (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
have 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
Tactic: use x +ᵥ b
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (goal)
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
⊢ ∃ (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
have 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
Tactic: subst hx
Cleared hypotheses: x, hs, hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (goal)
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),
    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
have 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
Tactic: obtain ⟨b⟩ := exists_affineBasis_of_finiteDimensional
    (ι := Fin (finrank ℝ E + 1)) (k := ℝ) (P := E) (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (hypothesis)
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
⊢ ∃ (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
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (hypothesis)
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)
⊢ ∃ (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
have hcnorm : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (goal)
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))
⊢ ∃ (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
have 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
Tactic: obtain ⟨ε, hε, hεs⟩ := Metric.mem_nhds_iff.1 hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (hypothesis)
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
have this : 0 ≤ cnorm
Tactic: have : 0 ≤ cnorm := Finset.le_sup'_of_le _ (Finset.mem_univ 0) (norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (hypothesis)
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)
⊢ ∃ (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
have hc' : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (hypothesis)
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
⊢ ∃ (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
have hε' : 0 < ε'
Tactic: have hε' : 0 < ε' := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (hypothesis)
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
⊢ ∃ (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
have hε₀ : 0 < ε / 2
Tactic: have hε₀ : 0 < ε / 2 := by positivity