awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : TopologicalSpace 𝕜
inst_8 : OrderTopology 𝕜
inst_9 : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y : (a : 𝕜) → E) 1 = y
t : 𝕜
ht1 : 1 < t
ht : Membership.mem (α := E) (closure s) ((AffineMap.lineMap x y : (a : 𝕜) → E) t : E)
⊢ y ∈ interior s
have a : y ∈ openSegment 𝕜 x ((AffineMap.lineMap x y : (a : 𝕜) → E) t)
Tactic: apply hs.openSegment_interior_closure_subset_interior hx ht
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : TopologicalSpace 𝕜
inst_8 : OrderTopology 𝕜
inst_9 : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y : (a : 𝕜) → E) 1 = y
t : 𝕜
ht1 : 1 < t
ht : Membership.mem (α := E) (closure s) ((AffineMap.lineMap x y : (a : 𝕜) → E) t : E)
⊢ y ∈ openSegment 𝕜 x ((AffineMap.lineMap x y : (a : 𝕜) → E) t)
have a : Membership.mem (γ := Set E) ((⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) '' openSegment 𝕜 0 t) y
Tactic: nth_rw 1 [← AffineMap.lineMap_apply_zero (k := 𝕜) x y, ← image_openSegment]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
E : Type u_3
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : CompactIccSpace 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : AddCommGroup E
inst_8 : Module 𝕜 E
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Finite
⊢ IsCompact.{u_3} (X := E) ((convexHull 𝕜 : (a : Set E) → Set E) s)
have rw : IsCompact.{u_3} (X := E)
  (Set.image (α := (↑s : Type u_3) → 𝕜)
    (⇑(∑ x : (↑s : Type u_3),
          LinearMap.smulRight (S := 𝕜) (LinearMap.proj (φ := fun (i : (↑s : Type u_3)) ↦ 𝕜) x) (↑x : E)) :
      (a : (↑s : Type u_3) → 𝕜) → E)
    (stdSimplex 𝕜 (↑s : Type u_3)))
Tactic: rw [hs.convexHull_eq_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (hypothesis)
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
⊢ Membership.mem (γ := Set E) ((⇑(homothety x t) : (a : E) → E) '' interior s) y
have hne : t ≠ 0
Tactic: have hne : t ≠ 0 := (one_pos.trans ht).ne'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ Membership.mem (γ := Set E) ((⇑(homothety x t) : (a : E) → E) '' interior s) y
have x₁ : Membership.mem (α := E) (openSegment ℝ x y) ((homothety x t⁻¹ : (a : E) → E) y : E)
Tactic: refine
    ⟨homothety x t⁻¹ y, hs.openSegment_interior_closure_subset_interior hx hy ?_,
      (AffineEquiv.homothetyUnitsMulHom x (Units.mk0 t hne)).apply_symm_apply y⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ Membership.mem (α := E) (openSegment ℝ x y) ((homothety x t⁻¹ : (a : E) → E) y : E)
have rw : Membership.mem (α := E) (γ := Set E) ((fun (x_1 : ℝ) ↦ (lineMap x y : (a : ℝ) → E) x_1⁻¹) '' Ioi 1)
  ((lineMap x y : (a : ℝ) → E) t⁻¹ : E)
Tactic: rw [openSegment_eq_image_lineMap, ← inv_one, ← inv_Ioi₀ (zero_lt_one' ℝ), ← image_inv_eq_inv,
    image_image, homothety_eq_lineMap]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
⊢ s.Nontrivial ↔ (interior s).Nonempty
have mp : s.Nontrivial → (interior s).Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
mp : s.Nontrivial → (interior s).Nonempty
⊢ s.Nontrivial ↔ (interior s).Nonempty
have mpr : (interior s).Nonempty → s.Nontrivial
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (hypothesis)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
⊢ (interior s).Nonempty
have hs' : ∀ (hs : (interior [x -[𝕜] y]).Nonempty), (interior s).Nonempty
Tactic: have hs' := Nonempty.mono <| interior_mono <| hs.segment_subset hx hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (hypothesis)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
hs' : ∀ (hs : (interior [x -[𝕜] y]).Nonempty), (interior s).Nonempty
⊢ (interior s).Nonempty
have hs'₁ : ∀ (hs : x ≠ y), (interior s).Nonempty
Tactic: rw [segment_eq_Icc', interior_Icc, nonempty_Ioo, inf_lt_sup] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ interior s
⊢ s.Nontrivial
have mpr : ∀ (hs : Convex 𝕜 (E := 𝕜) {x}) (hx : Membership.mem (γ := Set 𝕜) (interior {x}) x), Set.Nontrivial (α := 𝕜) {x}
Tactic: rcases eq_singleton_or_nontrivial (interior_subset hx) with rfl | h
Cleared hypotheses: s, hs, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ interior s
mpr : ∀ (hs : Convex 𝕜 (E := 𝕜) {x}) (hx : Membership.mem (γ := Set 𝕜) (interior {x}) x), Set.Nontrivial (α := 𝕜) {x}
⊢ s.Nontrivial
have mpr₁ : ∀ (h : s.Nontrivial), s.Nontrivial
Tactic: rcases eq_singleton_or_nontrivial (interior_subset hx) with rfl | h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (hypothesis)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hs : Convex 𝕜 (E := 𝕜) {x}
hx : Membership.mem (γ := Set 𝕜) (interior {x}) x
⊢ Set.Nontrivial (α := 𝕜) {x}
have hx₁ : Membership.mem (γ := Set 𝕜) ∅ x
Tactic: rw [interior_singleton] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (hypothesis)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
hs_sub : Subsingleton.{u_4 + 1} (↑s : Type u_4)
⊢ Ioo a b ⊆ s
have hs_sub₁ : s.Subsingleton
Tactic: simp only [subsingleton_coe] at hs_sub
Cleared hypotheses: hs_sub
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (hypothesis)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
h' : Nontrivial.{u_4} (↑s : Type u_4)
⊢ Ioo a b ⊆ s
have h'₁ : s.Nontrivial
Tactic: simp only [nontrivial_coe_sort] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (hypothesis)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
⊢ Ioo a b ⊆ s
have x : Subsingleton.{u_4 + 1} (↑s : Type u_4) ∨ Nontrivial.{u_4} (↑s : Type u_4)
Tactic: cases subsingleton_or_nontrivial s with
  | inl hs_sub =>
    simp only [subsingleton_coe] at hs_sub
    simp [hs_sub.closure has hbs]
  | inr h' =>
    simp only [nontrivial_coe_sort] at h'
    calc Ioo a b
    _ = interior (Ioo a b) := interior_Ioo.symm
    _ ⊆ interior (openSegment 𝕜 a b) := interior_mono <| Ioo_subset_openSegment
    _ ⊆ interior (closure s) := interior_mono <| hs.closure.openSegment_subset has hbs
    _ = interior s := hs.interior_closure_eq_interior_of_nonempty_interior <|
      hs.nontrivial_iff_nonempty_interior.1 h'
    _ ⊆ s := interior_subset
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h' : (s ∩ Iio a).Nonempty
⊢ 𝓝[s ∩ Iio a] a = 𝓝[<] a
have obtain : ∀ (b : 𝕜) (hbs : b ∈ s) (hba : b ∈ Iio a), 𝓝[s ∩ Iio a] a = 𝓝[<] a
Tactic: obtain ⟨b, hbs, hba⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
⊢ 𝓝[s ∩ Iio a] a = 𝓝[<] a
have refine : Ioo b a ⊆ s
Tactic: refine nhdsWithin_inter_of_mem (mem_nhdsLT_iff_exists_Ioo_subset.2 ⟨b, hba, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h' : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s ∩ Ioi a] a = 𝓝[>] a
have obtain : ∀ (b : 𝕜) (hbs : b ∈ s) (hba : b ∈ Ioi a), 𝓝[s ∩ Ioi a] a = 𝓝[>] a
Tactic: obtain ⟨b, hbs, hba⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Ioi a
⊢ 𝓝[s ∩ Ioi a] a = 𝓝[>] a
have refine : Ioo a b ⊆ s
Tactic: refine nhdsWithin_inter_of_mem (mem_nhdsGT_iff_exists_Ioo_subset.2 ⟨b, hba, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s \ {a}] a = 𝓝[≠] a
have rw : 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[<] a ⊔ 𝓝[>] a
Tactic: rw [diff_eq, ← Iio_union_Ioi, inter_union_distrib_left, nhdsWithin_union, nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : s ∩ Ioi a = ∅
⊢ 𝓝[s \ {a}] a = 𝓝[<] a
have rw : 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[<] a
Tactic: rw [diff_eq, ← Iio_union_Ioi, inter_union_distrib_left, nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h_Iio : s ∩ Iio a = ∅
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s \ {a}] a = 𝓝[>] a
have rw : 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[>] a
Tactic: rw [diff_eq, ← Iio_union_Ioi, inter_union_distrib_left, nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
have inl : ∀ (hs' : s ∩ Iio a = ∅), ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
Tactic: rcases eq_empty_or_nonempty (s ∩ Iio a) with hs' | ⟨b, hbs, hba⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
inl : ∀ (hs' : s ∩ Iio a = ∅), ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
have inr : ∀ (b : 𝕜) (hbs : b ∈ s) (hba : b ∈ Iio a), ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
Tactic: rcases eq_empty_or_nonempty (s ∩ Iio a) with hs' | ⟨b, hbs, hba⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (hypothesis)
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
have this : Ioo b a ⊆ s
Tactic: have : Ioo b a ⊆ s := h b (subset_closure hbs)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
have apply : Ioo b a ∈ 𝓝[s ∩ Iio a] a
Tactic: apply eventually_of_mem (U := Ioo b a) ?_ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
apply : Ioo b a ∈ 𝓝[s ∩ Iio a] a
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
have apply₁ : ∀ (x : 𝕜) (hx : x ∈ Ioo b a), s \ {a} ∈ 𝓝 x
Tactic: apply eventually_of_mem (U := Ioo b a) ?_ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
have inl : ∀ (h : 𝓝[s \ {a}] a = ⊥), ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
Tactic: rcases eq_or_neBot (𝓝[s \ {a}] a) with h | has
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
inl : ∀ (h : 𝓝[s \ {a}] a = ⊥), ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
have inr : ∀ (has : (𝓝[s \ {a}] a).NeBot), ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
Tactic: rcases eq_or_neBot (𝓝[s \ {a}] a) with h | has
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
h : 𝓝[s \ {a}] a = ⊥
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
have inl : ∀ᶠ (x : 𝕜) in ⊥, s \ {a} ∈ 𝓝 x
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (hypothesis)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : (𝓝[s \ {a}] a).NeBot
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
have has₁ : a ∈ closure[inst_3] s
Tactic: replace has := closure_mono diff_subset (mem_closure_iff_nhdsWithin_neBot.2 has)
Cleared hypotheses: has
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
| 𝓝[s \ {a}] a
have rw : 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a
Tactic: rw [diff_eq, ← Iio_union_Ioi, inter_union_distrib_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
have inr : ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x
Tactic: conv in 𝓝[s \ {a}] a => rw [diff_eq, ← Iio_union_Ioi, inter_union_distrib_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x
have inr : (∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x) ∧ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x
Tactic: rw [nhdsWithin_union, eventually_sup]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : CompactIccSpace 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : AddCommGroup V
inst_8 : TopologicalSpace V
inst_9 : IsTopologicalAddGroup V
inst_10 : Module 𝕜 V
inst_11 : ContinuousSMul 𝕜 V
inst_12 : AffineSpace V P
inst_13 : TopologicalSpace P
inst_14 : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
this :
  IsCompact.{u_5} (X := V)
    ((⇑(↑(AffineEquiv.symm (AffineEquiv.vaddConst 𝕜 (s.points 0))) : P →ᵃ[𝕜] V) : (a : P) → V) '' s.closedInterior)
⊢ IsCompact s.closedInterior
have apply : IsCompact.{u_5} (X := V) ((⇑(Homeomorph.symm (Homeomorph.vaddConst (s.points 0))) : (a : P) → V) '' s.closedInterior)
Tactic: apply (Homeomorph.vaddConst (s.points 0)).symm.isCompact_image.mp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : CompactIccSpace 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : AddCommGroup V
inst_8 : TopologicalSpace V
inst_9 : IsTopologicalAddGroup V
inst_10 : Module 𝕜 V
inst_11 : ContinuousSMul 𝕜 V
inst_12 : AffineSpace V P
inst_13 : TopologicalSpace P
inst_14 : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
⊢ IsCompact s.closedInterior
have suffices : IsCompact.{u_5} (X := V)
  ((⇑(↑(AffineEquiv.symm (AffineEquiv.vaddConst 𝕜 (s.points 0))) : P →ᵃ[𝕜] V) : (a : P) → V) '' s.closedInterior)
Tactic: suffices IsCompact ((AffineEquiv.vaddConst 𝕜 (s.points 0)).symm.toAffineMap ''
      s.closedInterior) by
    apply (Homeomorph.vaddConst (s.points 0)).symm.isCompact_image.mp
    simpa
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : CompactIccSpace 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : AddCommGroup V
inst_8 : TopologicalSpace V
inst_9 : IsTopologicalAddGroup V
inst_10 : Module 𝕜 V
inst_11 : ContinuousSMul 𝕜 V
inst_12 : AffineSpace V P
inst_13 : TopologicalSpace P
inst_14 : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
⊢ IsCompact.{u_5} (X := V)
    ((⇑(↑(AffineEquiv.symm (AffineEquiv.vaddConst 𝕜 (s.points 0))) : P →ᵃ[𝕜] V) : (a : P) → V) '' s.closedInterior)
have rw : IsCompact.{u_5} (X := V)
  ((convexHull 𝕜 : (a : Set V) → Set V)
    (range (s.map (↑(AffineEquiv.symm (AffineEquiv.vaddConst 𝕜 (s.points 0))) : P →ᵃ[𝕜] V) sorry).points))
Tactic: rw [← s.closedInterior_map (AffineEquiv.injective _), ← convexHull_eq_closedInterior]
-- Lean 4 proof step from Mathlib.Analysis.Convex.TotallyBounded (goal)
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded.{u_1} (α := E) ((convexHull ℝ : (a : Set E) → Set E) s)
have rw : ∀ (U : Set E),
  Membership.mem (γ := Filter E) (nhds 0) U →
    ∃ (t : Set E),
      t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
Tactic: rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.TotallyBounded (goal)
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
⊢ ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
have obtain : ∀ (W : Set E) (hW₁ : Membership.mem (γ := Filter E) (nhds 0) W) (hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U),
  ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
Tactic: obtain ⟨W, hW₁, hW₂⟩ := exists_nhds_zero_half hU
-- Lean 4 proof step from Mathlib.Analysis.Convex.TotallyBounded (goal)
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
⊢ ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
have obtain : ∀ (V : Set E) (hV₁ : Membership.mem (γ := Filter E) (nhds 0) V) (hV₂ : Convex ℝ V) (hV₃ : V ⊆ W),
  ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
Tactic: obtain ⟨V, ⟨hV₁, hV₂, hV₃⟩⟩ := (locallyConvexSpace_iff_exists_convex_subset_zero ℝ E).mp lcs W hW₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.TotallyBounded (goal)
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
⊢ ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
have obtain : ∀ (t : Set E) (htf : t.Finite) (hts : s ⊆ ⋃ y ∈ t, y +ᵥ V),
  ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
Tactic: obtain ⟨t, ⟨htf, hts⟩⟩ := (totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp hs) _ hV₁