awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
⊢ (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
have refine_2 : 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) ⊆
  t
Tactic: rw [Finset.coe_add, Finset.coe_image, Finset.coe_univ, Set.image_univ, convexHull_add]
-- 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
      (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))
have refine_1 : ∀ (i : E) (j : 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} ⊆
    interior
        ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))) +
      (↑u : Set E)
Tactic: grw [hu₃, ← subset_interior_add_left, Set.iUnion₂_subset_iff, ← subset_convexHull _ (u : Set E)]
-- 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}
i : E
j : 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} ⊆
    interior
        ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))) +
      (↑u : Set E)
have refine_1 : {i} ⊆ (↑u : Set E)
Tactic: gcongr
-- 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}
⊢ 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) ⊆
    t
have refine_2 : 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) s : Set E) ⊆
  t
Tactic: grw [hu₁, hs₁.convexHull_eq, hb₂, hV₂, 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}
refine_2 :
  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) s : Set E) ⊆
    t
⊢ 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) ⊆
    t
have refine_2₁ : HAdd.hAdd (α := Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
      Set E)
    s ⊆
  t
Tactic: grw [hu₁, hs₁.convexHull_eq, hb₂, hV₂, 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}
refine_2 :
  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) s : Set E) ⊆
    t
refine_2₁ :
  HAdd.hAdd (α := Set E)
      ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
        Set E)
      s ⊆
    t
⊢ 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) ⊆
    t
have refine_2₂ : V + s ⊆ t
Tactic: grw [hu₁, hs₁.convexHull_eq, hb₂, hV₂, 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}
refine_2 :
  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) s : Set E) ⊆
    t
refine_2₁ :
  HAdd.hAdd (α := Set E)
      ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
        Set E)
      s ⊆
    t
refine_2₂ : V + s ⊆ t
refine_2₃ : U ⊆ t
⊢ 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) ⊆
    t
have refine_2₄ : t ⊆ t
Tactic: grw [hu₁, hs₁.convexHull_eq, hb₂, hV₂, 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 : 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: classical
  rcases mem_nhdsSet_iff_exists.1 ht with ⟨U, hU₁, hU₂, hU₃⟩
  rcases compact_open_separated_add_left hs₂ hU₁ hU₂ with ⟨V, hV₁, hV₂⟩
  rcases exists_mem_interior_convexHull_affineBasis hV₁ with ⟨b, hb₁, hb₂⟩
  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₃⟩
  lift u to Finset E using hu₂
  refine ⟨Finset.univ.image b + u, ?_, ?_⟩
  all_goals rw [Finset.coe_add, Finset.coe_image, Finset.coe_univ, Set.image_univ, convexHull_add]
  · grw [hu₃, ← subset_interior_add_left, Set.iUnion₂_subset_iff, ← subset_convexHull _ (u : Set E)]
    intros
    gcongr
    simpa
  · grw [hu₁, hs₁.convexHull_eq, hb₂, hV₂, 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
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
have rcases₁ : ∀ (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
Tactic: classical
  rcases mem_nhdsSet_iff_exists.1 ht with ⟨U, hU₁, hU₂, hU₃⟩
  rcases compact_open_separated_add_left hs₂ hU₁ hU₂ with ⟨V, hV₁, hV₂⟩
  rcases exists_mem_interior_convexHull_affineBasis hV₁ with ⟨b, hb₁, hb₂⟩
  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₃⟩
  lift u to Finset E using hu₂
  refine ⟨Finset.univ.image b + u, ?_, ?_⟩
  all_goals rw [Finset.coe_add, Finset.coe_image, Finset.coe_univ, Set.image_univ, convexHull_add]
  · grw [hu₃, ← subset_interior_add_left, Set.iUnion₂_subset_iff, ← subset_convexHull _ (u : Set E)]
    intros
    gcongr
    simpa
  · grw [hu₁, hs₁.convexHull_eq, hb₂, hV₂, 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
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
rcases₁ :
  ∀ (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
⊢ ∃ (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)
  (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
Tactic: classical
  rcases mem_nhdsSet_iff_exists.1 ht with ⟨U, hU₁, hU₂, hU₃⟩
  rcases compact_open_separated_add_left hs₂ hU₁ hU₂ with ⟨V, hV₁, hV₂⟩
  rcases exists_mem_interior_convexHull_affineBasis hV₁ with ⟨b, hb₁, hb₂⟩
  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₃⟩
  lift u to Finset E using hu₂
  refine ⟨Finset.univ.image b + u, ?_, ?_⟩
  all_goals rw [Finset.coe_add, Finset.coe_image, Finset.coe_univ, Set.image_univ, convexHull_add]
  · grw [hu₃, ← subset_interior_add_left, Set.iUnion₂_subset_iff, ← subset_convexHull _ (u : Set E)]
    intros
    gcongr
    simpa
  · grw [hu₁, hs₁.convexHull_eq, hb₂, hV₂, hU₃]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
⊢ f.linear = f.linearIsometry.toLinearMap
have h : ∀ (x : V),
  Eq.{u_5 + 1} (α := V₂) ((f.linear : (a : V) → V₂) x : V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) x : V₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₁
inst_6 : NormedSpace 𝕜 V₁
inst_7 : PseudoMetricSpace P₁
inst_8 : NormedAddTorsor V₁ P₁
inst_9 : SeminormedAddCommGroup V₁'
inst_10 : NormedSpace 𝕜 V₁'
inst_11 : MetricSpace P₁'
inst_12 : NormedAddTorsor V₁' P₁'
inst_13 : SeminormedAddCommGroup V₂
inst_14 : NormedSpace 𝕜 V₂
inst_15 : PseudoMetricSpace P₂
inst_16 : NormedAddTorsor V₂ P₂
inst_17 : SeminormedAddCommGroup V₃
inst_18 : NormedSpace 𝕜 V₃
inst_19 : PseudoMetricSpace P₃
inst_20 : NormedAddTorsor V₃ P₃
inst_21 : SeminormedAddCommGroup V₄
inst_22 : NormedSpace 𝕜 V₄
inst_23 : PseudoMetricSpace P₄
inst_24 : NormedAddTorsor V₄ P₄
f_1 f g : P →ᵃⁱ[𝕜] P₂
⊢ Eq (α := (a : P) → P₂) ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) f) ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) g) → f = g
have mk : ∀ (toAffineMap : P →ᵃ[𝕜] P₂)
  (norm_map : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineMap.linear : (a : V) → V₂) x : V₂) = ‖x‖),
  Eq (α := (a : P) → P₂) ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) { toAffineMap := toAffineMap, norm_map := norm_map })
      ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) g) →
    { toAffineMap := toAffineMap, norm_map := norm_map : P →ᵃⁱ[𝕜] P₂ } = g
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₁
inst_6 : NormedSpace 𝕜 V₁
inst_7 : PseudoMetricSpace P₁
inst_8 : NormedAddTorsor V₁ P₁
inst_9 : SeminormedAddCommGroup V₁'
inst_10 : NormedSpace 𝕜 V₁'
inst_11 : MetricSpace P₁'
inst_12 : NormedAddTorsor V₁' P₁'
inst_13 : SeminormedAddCommGroup V₂
inst_14 : NormedSpace 𝕜 V₂
inst_15 : PseudoMetricSpace P₂
inst_16 : NormedAddTorsor V₂ P₂
inst_17 : SeminormedAddCommGroup V₃
inst_18 : NormedSpace 𝕜 V₃
inst_19 : PseudoMetricSpace P₃
inst_20 : NormedAddTorsor V₃ P₃
inst_21 : SeminormedAddCommGroup V₄
inst_22 : NormedSpace 𝕜 V₄
inst_23 : PseudoMetricSpace P₄
inst_24 : NormedAddTorsor V₄ P₄
f g : P →ᵃⁱ[𝕜] P₂
toAffineMap : P →ᵃ[𝕜] P₂
norm_map : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineMap.linear : (a : V) → V₂) x : V₂) = ‖x‖
⊢ Eq (α := (a : P) → P₂) ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) { toAffineMap := toAffineMap, norm_map := norm_map })
      ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) g) →
    { toAffineMap := toAffineMap, norm_map := norm_map : P →ᵃⁱ[𝕜] P₂ } = g
have mk : ∀ (toAffineMap_1 : P →ᵃ[𝕜] P₂)
  (norm_map_1 : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineMap_1.linear : (a : V) → V₂) x : V₂) = ‖x‖),
  Eq (α := (a : P) → P₂) ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) { toAffineMap := toAffineMap, norm_map := norm_map })
      ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) { toAffineMap := toAffineMap_1, norm_map := norm_map_1 }) →
    { toAffineMap := toAffineMap, norm_map := norm_map : P →ᵃⁱ[𝕜] P₂ } =
      { toAffineMap := toAffineMap_1, norm_map := norm_map_1 }
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : SeminormedAddCommGroup V₂
inst_4 : NormedSpace 𝕜 V₂
f : V →ₗᵢ[𝕜] V₂
⊢ f.toAffineIsometry.linearIsometry = f
have h : ∀ (x : V),
  Eq.{u_5 + 1} (α := V₂) ((f.toAffineIsometry.linearIsometry : (a : V) → V₂) x : V₂) ((f : (a : V) → V₂) x : V₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
x y : P
⊢ dist.{u_11} (α := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂) = dist x y
have rw : ‖VSub.vsub.{u_5, u_11} (P := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂)‖ = dist x y
Tactic: rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linearIsometry.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Isometry (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
x y : P
rw : ‖VSub.vsub.{u_5, u_11} (P := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂)‖ = dist x y
⊢ dist.{u_11} (α := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂) = dist x y
have rw₁ : ‖VSub.vsub.{u_5, u_11} (P := P₂) ((f : (a : P) → P₂) x : P₂) ((f : (a : P) → P₂) y : P₂)‖ = ‖x -ᵥ y‖
Tactic: rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linearIsometry.norm_map]