awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Topology
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 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h :
  (s \ interior s).Pairwise fun (x y : E) ↦
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∉ interior s
hy' : y ∉ interior s
c : 𝕜
hc : Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
⊢ openSegment 𝕜 ((lineMap x y : (a : 𝕜) → E) c) y ⊆ interior s

Tactic:
hs.openSegment_interior_self_subset_interior hc hy

Premises used: Convex.openSegment_interior_self_subset_interior
-- Module: Mathlib.Analysis.Convex.Topology
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 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h :
  (s \ interior s).Pairwise fun (x y : E) ↦
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∉ interior s
hy' : y ∉ interior s
c : 𝕜
hc : Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
⊢ openSegment 𝕜 x ((lineMap x y : (a : 𝕜) → E) c) ⊆ interior s

Tactic:
exacts [hs.openSegment_self_interior_subset_interior hx hc,
    hs.openSegment_interior_self_subset_interior hc hy]

Premises used: Convex.openSegment_self_interior_subset_interior, Convex.openSegment_interior_self_subset_interior
-- Module: Mathlib.Analysis.Convex.Topology
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 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun (x y : E) ↦ ([x -[𝕜] y] \ frontier s).Nonempty
⊢ StrictConvex 𝕜 s

Tactic:
hs.strictConvex' <| h.imp_on fun x hx y hy _ => ?_

Premises used: Set.Pairwise.imp_on, Convex.strictConvex'
-- Module: Mathlib.Analysis.Convex.Topology
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 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun (x y : E) ↦ ([x -[𝕜] y] \ frontier s).Nonempty
refine :
  ∀ (x : E) (hx : x ∈ s \ interior s) (y : E) (hy : y ∈ s \ interior s),
    x ≠ y →
      (fun ⦃a b : E⦄ ↦
          ([a -[𝕜] b] \ frontier s).Nonempty →
            ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap a b : (a : 𝕜) → E) c : E))
        (a := x) (b := y)
⊢ StrictConvex 𝕜 s

Tactic:
refine hs.strictConvex' <| h.imp_on fun x hx y hy _ => ?_

Premises used: Set.Pairwise.imp_on, Convex.strictConvex'
-- Module: Mathlib.Analysis.Convex.Topology
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 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun (x y : E) ↦ ([x -[𝕜] y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
h_1 : x ≠ y
simp :
  (image.{u_2, u_3} (α := 𝕜) (⇑(lineMap x y) : (a : 𝕜) → E) (Icc 0 1) \ frontier s).Nonempty →
    ∃ (c : 𝕜), Membership.mem (α := E) (s \ frontier s) ((lineMap x y : (a : 𝕜) → E) c : E)
⊢ ([x -[𝕜] y] \ frontier s).Nonempty →
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)

Tactic:
simp only [segment_eq_image_lineMap, ← self_diff_frontier]

Premises used: self_diff_frontier, segment_eq_image_lineMap
-- Module: Mathlib.Analysis.Convex.Topology
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 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun (x y : E) ↦ ([x -[𝕜] y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
h_1 : x ≠ y
c : 𝕜
hc : Membership.mem (γ := Set 𝕜) (Icc 0 1) c
hcs : ((lineMap x y : (a : 𝕜) → E) c : E) ∉ frontier s
⊢ ∃ (c : 𝕜), Membership.mem (α := E) (s \ frontier s) ((lineMap x y : (a : 𝕜) → E) c : E)

Tactic:
⟨c, hs.segment_subset hx.1 hy.1 ?_, hcs⟩

Premises used: And.left, And.intro, Exists.intro, Convex.segment_subset
-- Module: Mathlib.Analysis.Convex.Topology
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 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun (x y : E) ↦ ([x -[𝕜] y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
h_1 : x ≠ y
c : 𝕜
hc : Membership.mem (γ := Set 𝕜) (Icc 0 1) c
hcs : ((lineMap x y : (a : 𝕜) → E) c : E) ∉ frontier s
refine : Membership.mem (α := E) [x -[𝕜] y] ((lineMap x y : (a : 𝕜) → E) c : E)
⊢ ∃ (c : 𝕜), Membership.mem (α := E) (s \ frontier s) ((lineMap x y : (a : 𝕜) → E) c : E)

Tactic:
refine ⟨c, hs.segment_subset hx.1 hy.1 ?_, hcs⟩
-- Module: Mathlib.Analysis.Convex.Topology
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 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun (x y : E) ↦ ([x -[𝕜] y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
h_1 : x ≠ y
c : 𝕜
hc : Membership.mem (γ := Set 𝕜) (Icc 0 1) c
hcs : ((lineMap x y : (a : 𝕜) → E) c : E) ∉ frontier s
⊢ Membership.mem (α := E) [x -[𝕜] y] ((lineMap x y : (a : 𝕜) → E) c : E)

Tactic:
lineMap_mem_segment 𝕜 x y hc

Premises used: Set.Mem, lineMap_mem_segment
-- Module: Mathlib.Analysis.Convex.Topology
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 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun (x y : E) ↦ ([x -[𝕜] y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
h_1 : x ≠ y
c : 𝕜
hc : Membership.mem (γ := Set 𝕜) (Icc 0 1) c
hcs : ((lineMap x y : (a : 𝕜) → E) c : E) ∉ frontier s
⊢ Membership.mem (α := E) [x -[𝕜] y] ((lineMap x y : (a : 𝕜) → E) c : E)

Tactic:
exact lineMap_mem_segment 𝕜 x y hc

Premises used: lineMap_mem_segment
-- Module: Mathlib.Analysis.Convex.Topology
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
hs' : (interior s).Nonempty
⊢ closure (interior s) = closure s

Tactic:
subset_antisymm (closure_mono interior_subset)
    fun _ h ↦ closure_mono (hs.openSegment_interior_closure_subset_interior hs'.choose_spec h)
      (segment_subset_closure_openSegment (right_mem_segment ..))

Premises used: Exists.choose_spec, interior_subset, subset_antisymm, closure_mono, right_mem_segment, Exists.choose, segment_subset_closure_openSegment, Convex.openSegment_interior_closure_subset_interior
-- Module: Mathlib.Analysis.Convex.Topology
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
hs' : (interior s).Nonempty
⊢ interior (closure s) = interior s

Tactic:
subset_antisymm ?_ (interior_mono subset_closure)

Premises used: interior_mono, subset_closure, subset_antisymm
-- Module: Mathlib.Analysis.Convex.Topology
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
hs' : (interior s).Nonempty
refine : interior (closure s) ⊆ interior s
⊢ interior (closure s) = interior s

Tactic:
refine subset_antisymm ?_ (interior_mono subset_closure)

Premises used: interior_mono, subset_closure, subset_antisymm
-- Module: Mathlib.Analysis.Convex.Topology
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
hs' : (interior s).Nonempty
y : E
hy : y ∈ interior (closure s)
rcases : ∀ (x : E) (hx : x ∈ interior s), y ∈ interior s
⊢ y ∈ interior s

Tactic:
rcases hs' with ⟨x, hx⟩
-- Module: Mathlib.Analysis.Convex.Topology
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
⊢ (AffineMap.lineMap x y : (a : 𝕜) → E) 1 = y

Tactic:
have h := AffineMap.lineMap_apply_one (k := 𝕜) x y
-- Module: Mathlib.Analysis.Convex.Topology
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
obtain :
  ∀ (t : 𝕜) (ht1 : 1 < t) (ht : Membership.mem (α := E) (closure s) ((AffineMap.lineMap x y : (a : 𝕜) → E) t : E)),
    y ∈ interior s
⊢ y ∈ interior s

Tactic:
obtain ⟨t, ht1, ht⟩ := AffineMap.lineMap_continuous.tendsto' _ _ h |>.eventually_mem
    (mem_interior_iff_mem_nhds.1 hy) |>.exists_gt

Premises used: mem_interior_iff_mem_nhds, AffineMap.lineMap_continuous, Filter.Tendsto.eventually_mem, Iff.mp, Continuous.tendsto', Filter.Eventually.exists_gt
-- Module: Mathlib.Analysis.Convex.Topology
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)
a : y ∈ openSegment 𝕜 x ((AffineMap.lineMap x y : (a : 𝕜) → E) t)
⊢ y ∈ interior s

Tactic:
apply hs.openSegment_interior_closure_subset_interior hx ht

Premises used: Convex.openSegment_interior_closure_subset_interior
-- Module: Mathlib.Analysis.Convex.Topology
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)
a : Membership.mem (γ := Set E) ((⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) '' openSegment 𝕜 0 t) y
⊢ y ∈ openSegment 𝕜 x ((AffineMap.lineMap x y : (a : 𝕜) → E) t)

Tactic:
nth_rw 1 [← AffineMap.lineMap_apply_zero (k := 𝕜) x y, ← image_openSegment]

Premises used: image_openSegment, AffineMap.lineMap_apply_zero
-- Module: Mathlib.Analysis.Convex.Topology
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)
⊢ Membership.mem (γ := Set E) ((⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) '' openSegment 𝕜 0 t) y

Tactic:
⟨1, Ioo_subset_openSegment ⟨zero_lt_one, ht1⟩, h⟩

Premises used: Set.Mem, setOf, zero_lt_one, Ioo_subset_openSegment, And.intro, Exists.intro, Set.image, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Topology
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)
⊢ Membership.mem (γ := Set E) ((⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) '' openSegment 𝕜 0 t) y

Tactic:
exact ⟨1, Ioo_subset_openSegment ⟨zero_lt_one, ht1⟩, h⟩
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
S : Set (Set E)
h : ∀ s ∈ S, Convex 𝕜 s ∧ IsClosed s
⊢ Convex 𝕜 (⋂₀ S) ∧ IsClosed (⋂₀ S)

Tactic:
⟨fun _ hx => starConvex_sInter fun _ hs => (h _ hs).1 <| hx _ hs,
    isClosed_sInter fun _ hs => (h _ hs).2⟩

Premises used: starConvex_sInter, And.right, And.left, And.intro, isClosed_sInter
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
s : Set E
⊢ Convex.{u_2, u_3} 𝕜 (E := E) ((closedConvexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
((closedConvexHull 𝕜).isClosed_closure s).1

Premises used: closedConvexHull, And.left, ClosureOperator.isClosed_closure
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
s : Set E
⊢ IsClosed.{u_3} (X := E) ((closedConvexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
((closedConvexHull 𝕜).isClosed_closure s).2

Premises used: closedConvexHull, And.right, ClosureOperator.isClosed_closure
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
s : Set E
⊢ s ⊆ (closedConvexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
(closedConvexHull 𝕜).le_closure s

Premises used: ClosureOperator.le_closure, closedConvexHull
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
s : Set E
⊢ closure s ⊆ (closedConvexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
closure_minimal subset_closedConvexHull isClosed_closedConvexHull

Premises used: subset_closedConvexHull, closure_minimal, isClosed_closedConvexHull
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
s t : Set E
hst : s ⊆ t
h_conv : Convex 𝕜 t
h_closed : IsClosed t
⊢ (closedConvexHull 𝕜 : (a : Set E) → Set E) s ⊆ t

Tactic:
(closedConvexHull 𝕜).closure_min hst ⟨h_conv, h_closed⟩

Premises used: ClosureOperator.closure_min, And.intro
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
s : Set E
⊢ Subset (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    ((closedConvexHull 𝕜 : (a : Set E) → Set E) s : Set E)

Tactic:
convexHull_min subset_closedConvexHull convex_closedConvexHull

Premises used: subset_closedConvexHull, convexHull_min, convex_closedConvexHull
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
s : Set E
⊢ Subset (α := Set E) ((closedConvexHull 𝕜 : (a : Set E) → Set E) (closure s) : Set E)
    ((closedConvexHull 𝕜 : (a : Set E) → Set E) s : Set E)

Tactic:
simpa using ((closedConvexHull 𝕜).monotone (closure_subset_closedConvexHull (𝕜 := 𝕜) (E := E)))

Premises used: closedConvexHull, ClosureOperator.monotone, closure_subset_closedConvexHull
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousConstSMul 𝕜 E
s : Set E
⊢ Eq (α := Set E) ((closedConvexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    (closure ((convexHull 𝕜 : (a : Set E) → Set E) s) : Set E)

Tactic:
subset_antisymm
  (closedConvexHull_min (subset_trans (subset_convexHull 𝕜 s) subset_closure)
    (Convex.closure (convex_convexHull 𝕜 s)) isClosed_closure)
  (closure_minimal convexHull_subset_closedConvexHull isClosed_closedConvexHull)

Premises used: closedConvexHull_min, subset_closure, closure_minimal, subset_convexHull, subset_trans, subset_antisymm, Convex.closure, convex_convexHull, isClosed_closure, isClosed_closedConvexHull, convexHull_subset_closedConvexHull
-- Module: Mathlib.Analysis.Convex.Topology
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
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)))
⊢ IsCompact.{u_3} (X := E) ((convexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
rw [hs.convexHull_eq_image]

Premises used: Set.Finite.convexHull_eq_image
-- Module: Mathlib.Analysis.Convex.Topology
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
this : Fintype (↑s : Type u_3) := hs.fintype (s := s)
⊢ 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:
(isCompact_stdSimplex 𝕜 s).image (LinearMap.continuous_on_pi _)

Premises used: isCompact_stdSimplex, Set.Elem, LinearMap.continuous_on_pi, IsCompact.image
-- Module: Mathlib.Analysis.Convex.Topology
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
this : Fintype (↑s : Type u_3) := hs.fintype (s := s)
⊢ 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:
exact (isCompact_stdSimplex 𝕜 s).image (LinearMap.continuous_on_pi _)

Premises used: isCompact_stdSimplex, Set.Elem, LinearMap.continuous_on_pi, IsCompact.image
-- Module: Mathlib.Analysis.Convex.Topology
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
inst_12 : T2Space E
s : Set E
hs : s.Finite
⊢ IsClosed.{u_3} (X := E) ((convexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
(hs.isCompact_convexHull 𝕜).isClosed

Premises used: Set.Finite.isCompact_convexHull, IsCompact.isClosed
-- Module: Mathlib.Analysis.Convex.Topology
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
⊢ t ≠ 0

Tactic:
have hne : t ≠ 0 := (one_pos.trans ht).ne'
-- Module: Mathlib.Analysis.Convex.Topology
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

Tactic:
⟨homothety x t⁻¹ y, hs.openSegment_interior_closure_subset_interior hx hy ?_,
      (AffineEquiv.homothetyUnitsMulHom x (Units.mk0 t hne)).apply_symm_apply y⟩

Premises used: Set.Mem, AffineMap.homothety, setOf, AffineEquiv.apply_symm_apply, AffineEquiv.homothetyUnitsMulHom, Units.mk0, Inv.inv, And.intro, Exists.intro, Set.image, DFunLike.coe, Convex.openSegment_interior_closure_subset_interior
-- Module: Mathlib.Analysis.Convex.Topology
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
x₁ : Membership.mem (α := E) (openSegment ℝ x y) ((homothety x t⁻¹ : (a : E) → E) y : E)
⊢ Membership.mem (γ := Set E) ((⇑(homothety x t) : (a : E) → E) '' interior s) y

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⟩