awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
ε : ℝ
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))
have simp : ∀ (y : Fin (finrank ℝ E + 1)), ε' * norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) y : E) ≤ ε / 2
Tactic: simp [d, abs_of_nonneg hε'.le, range_subset_iff, norm_smul]
-- 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
hε₀ : 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
have hdnorm : 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
-- 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))
ε : ℝ
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
have 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
Tactic: refine ⟨d, ?_, ?_⟩
-- 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))
ε : ℝ
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
⊢ ∃ (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 refine_2 : (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑d : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ s
Tactic: refine ⟨d, ?_, ?_⟩
-- 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))
ε : ℝ
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))
⊢ ε / 2 < ε
have linarith : ε ≤ ε / 2 → 2 / 2 = 1
Tactic: linarith
-- 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))
ε : ℝ
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
⊢ ε / 2 < ε
have linarith₁ : ε ≤ ε / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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))
ε : ℝ
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
⊢ ε / 2 < ε
have linarith₂ : ε ≤ ε / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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))
ε : ℝ
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
⊢ ε / 2 < ε
have linarith₆ : ε ≤ ε / 2 → 0 - ε + (2 * ε - 1 * ε) = 0
Tactic: linarith
-- 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 t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
have 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
Tactic: rcases mem_nhdsSet_iff_exists.1 ht with ⟨U, hU₁, hU₂, hU₃⟩
-- 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 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
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
have 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
Tactic: rcases compact_open_separated_add_left hs₂ hU₁ hU₂ with ⟨V, hV₁, hV₂⟩
-- 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 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
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
have 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
Tactic: rcases exists_mem_interior_convexHull_affineBasis hV₁ with ⟨b, hb₁, hb₂⟩
-- 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 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
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
have rcases : ∀ (u : Set E) (hu₁ : u ⊆ s) (hu₂ : u.Finite)
  (hu₃ :
    s ⊆
      ⋃ i ∈ u,
        HAdd.hAdd (α := Set E)
          (interior
            ((convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
          {i}),
  ∃ (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 hs₂.elim_finite_subcover_image (b := s)
      (c := fun x => interior (convexHull ℝ (Set.range b)) + {x})
      (fun _ _ => isOpen_interior.add_right)
      (fun x hx => Set.mem_iUnion₂_of_mem hx <| by simpa using hb₁)
    with ⟨u, hu₁, hu₂, hu₃⟩
-- 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 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
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 : Set E
hu₁ : u ⊆ s
hu₂ : u.Finite
hu₃ :
  s ⊆
    ⋃ i ∈ u,
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
have lift : ∀ (u : Finset E) (hu₁ : (↑u : Set E) ⊆ s)
  (hu₃ :
    s ⊆
      ⋃ i ∈ (↑u : Set E),
        HAdd.hAdd (α := Set E)
          (interior
            ((convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
          {i}),
  ∃ (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: lift u to Finset E using hu₂
Cleared hypotheses: u, hu₁, hu₂, hu₃
-- 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 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
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
hu₁ : (↑u : Set E) ⊆ s
hu₃ :
  s ⊆
    ⋃ i ∈ (↑u : Set E),
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
have refine_1 : s ⊆
  interior
    ((convexHull ℝ : (a : Set E) → Set E)
      (↑(Finset.image (α := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E) Finset.univ + u) : Set E))
Tactic: refine ⟨Finset.univ.image b + u, ?_, ?_⟩
-- 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 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
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
hu₁ : (↑u : Set E) ⊆ s
hu₃ :
  s ⊆
    ⋃ i ∈ (↑u : Set E),
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
refine_1 :
  s ⊆
    interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (↑(Finset.image (α := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E) Finset.univ + u) : Set E))
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
have refine_2 : (convexHull ℝ : (a : Set E) → Set E)
    (↑(Finset.image (α := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E) Finset.univ + u) : Set E) ⊆
  t
Tactic: refine ⟨Finset.univ.image b + u, ?_, ?_⟩
-- 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 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
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
hu₁ : (↑u : Set E) ⊆ s
hu₃ :
  s ⊆
    ⋃ i ∈ (↑u : Set E),
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
⊢ s ⊆
    interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (↑(Finset.image (α := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E) Finset.univ + u) : Set E))
have refine_1 : s ⊆
  interior
    (HAdd.hAdd (α := Set E) (β := Set E)
      ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
        Set E)
      ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) : Set E))
Tactic: rw [Finset.coe_add, Finset.coe_image, Finset.coe_univ, Set.image_univ, convexHull_add]