awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DenselyOrdered 𝕜
inst_4 : PseudoMetricSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : ProperSpace 𝕜
inst_7 : CompactIccSpace 𝕜
inst_8 : AddCommGroup E
inst_9 : TopologicalSpace E
inst_10 : T2Space E
inst_11 : ContinuousAdd E
inst_12 : Module 𝕜 E
inst_13 : ContinuousSMul 𝕜 E
x y : E
rw :
  Eq.{u_3 + 1} (α := Set E) (closure ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' Ioo 0 1))
    ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' closure (Ioo 0 1))
⊢ closure (openSegment 𝕜 x y) = [x -[𝕜] y]

Tactic:
rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]

Premises used: segment_eq_image, openSegment_eq_image, zero_ne_one', closure_Ioo
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DenselyOrdered 𝕜
inst_4 : PseudoMetricSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : ProperSpace 𝕜
inst_7 : CompactIccSpace 𝕜
inst_8 : AddCommGroup E
inst_9 : TopologicalSpace E
inst_10 : T2Space E
inst_11 : ContinuousAdd E
inst_12 : Module 𝕜 E
inst_13 : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous.{u_2, u_3} (Y := E) fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DenselyOrdered 𝕜
inst_4 : PseudoMetricSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : ProperSpace 𝕜
inst_7 : CompactIccSpace 𝕜
inst_8 : AddCommGroup E
inst_9 : TopologicalSpace E
inst_10 : T2Space E
inst_11 : ContinuousAdd E
inst_12 : Module 𝕜 E
inst_13 : ContinuousSMul 𝕜 E
x y : E
⊢ Eq.{u_3 + 1} (α := Set E) (closure ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' Ioo 0 1))
    ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' closure (Ioo 0 1))

Tactic:
exact (image_closure_of_isCompact (isBounded_Ioo _ _).isCompact_closure <|
    Continuous.continuousOn <| by fun_prop).symm

Premises used: Continuous.continuousOn, image_closure_of_isCompact, Metric.isBounded_Ioo, Bornology.IsBounded.isCompact_closure, Eq.symm
-- 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
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
rw rw₁ : interior (a • s) + b • s = interior (a • s) + b • s
⊢ interior (a • s) + closure (b • s) = interior (a • s) + b • s

Tactic:
rw [isOpen_interior.add_closure (b • s)]

Premises used: IsOpen.add_closure, isOpen_interior, HSMul.hSMul
-- 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
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • interior s + b • s ⊆ interior s

Tactic:
calc
    a • interior s + b • s ⊆ a • interior s + b • closure s :=
      add_subset_add Subset.rfl <| image_mono subset_closure
    _ ⊆ interior s := hs.combo_interior_closure_subset_interior ha hb hab

Premises used: Trans.trans, subset_closure, Convex.combo_interior_closure_subset_interior, Set.image_mono, Set.Subset.rfl, Set.add_subset_add
-- 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
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
rw : b • interior s + a • closure s ⊆ interior s
⊢ a • closure s + b • interior s ⊆ interior s

Tactic:
rw [add_comm]

Premises used: add_comm
-- 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
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • closure s ⊆ interior s

Tactic:
hs.combo_interior_closure_subset_interior hb ha (add_comm a b ▸ hab)

Premises used: Convex.combo_interior_closure_subset_interior, Eq.rec, add_comm
-- 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
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • closure s ⊆ interior s

Tactic:
exact hs.combo_interior_closure_subset_interior hb ha (add_comm a b ▸ hab)

Premises used: Convex.combo_interior_closure_subset_interior, Eq.rec, add_comm
-- 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
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
rw : b • interior s + a • s ⊆ interior s
⊢ a • s + b • interior s ⊆ interior s

Tactic:
rw [add_comm]

Premises used: add_comm
-- 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
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • s ⊆ interior s

Tactic:
hs.combo_interior_self_subset_interior hb ha (add_comm a b ▸ hab)

Premises used: Eq.rec, Convex.combo_interior_self_subset_interior, add_comm
-- 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
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • s ⊆ interior s

Tactic:
exact hs.combo_interior_self_subset_interior hb ha (add_comm a b ▸ hab)

Premises used: Eq.rec, Convex.combo_interior_self_subset_interior, add_comm
-- 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
hs : Convex 𝕜 s
x y : E
hx : x ∈ interior s
hy : y ∈ closure s
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
hs.combo_interior_closure_subset_interior ha hb hab <|
    add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)

Premises used: Convex.combo_interior_closure_subset_interior, Set.add_mem_add, Set.smul_mem_smul_set
-- 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
hs : Convex 𝕜 s
x y : E
hx : x ∈ interior s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
hs.combo_interior_closure_mem_interior hx (subset_closure hy) ha hb hab

Premises used: Convex.combo_interior_closure_mem_interior, subset_closure
-- 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
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
hs.combo_closure_interior_subset_interior ha hb hab <|
    add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)

Premises used: Set.add_mem_add, Convex.combo_closure_interior_subset_interior, Set.smul_mem_smul_set
-- 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
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ interior s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
hs.combo_closure_interior_mem_interior (subset_closure hx) hy ha hb hab

Premises used: subset_closure, Convex.combo_closure_interior_mem_interior
-- 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
hs : Convex 𝕜 s
x y : E
hx : x ∈ interior s
hy : y ∈ closure s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
hs.combo_interior_closure_mem_interior hx hy ha hb.le hab

Premises used: Convex.combo_interior_closure_mem_interior, LT.lt.le
-- 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
hs : Convex 𝕜 s
x y : E
hx : x ∈ interior s
hy : y ∈ closure s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
exact hs.combo_interior_closure_mem_interior hx hy ha hb.le hab

Premises used: Convex.combo_interior_closure_mem_interior, LT.lt.le
-- 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
hs : Convex 𝕜 s
x y : E
hx : x ∈ interior s
hy : y ∈ s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
hs.openSegment_interior_closure_subset_interior hx (subset_closure hy)

Premises used: subset_closure, Convex.openSegment_interior_closure_subset_interior
-- 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
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
hs.combo_closure_interior_mem_interior hx hy ha.le hb hab

Premises used: LT.lt.le, Convex.combo_closure_interior_mem_interior
-- 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
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
exact hs.combo_closure_interior_mem_interior hx hy ha.le hb hab

Premises used: LT.lt.le, Convex.combo_closure_interior_mem_interior
-- 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
inst_7 : AddRightMono 𝕜
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Ioc 0 1) t
⊢ x + t • (y - x) ∈ interior s

Tactic:
simpa only [sub_smul, smul_sub, one_smul, add_sub, add_comm] using
    hs.combo_interior_closure_mem_interior hy hx ht.1 (sub_nonneg.mpr ht.2)
      (add_sub_cancel _ _)

Premises used: Iff.mpr, Convex.combo_interior_closure_mem_interior, add_sub, sub_smul, add_comm, one_smul, smul_sub, And.right, add_sub_cancel, And.left, sub_nonneg
-- 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
inst_7 : AddRightMono 𝕜
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ interior s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Ioc 0 1) t
⊢ x + t • (y - x) ∈ interior s

Tactic:
hs.add_smul_sub_mem_interior' (subset_closure hx) hy ht

Premises used: subset_closure, Convex.add_smul_sub_mem_interior'
-- 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
inst_7 : AddRightMono 𝕜
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : x + y ∈ interior s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Ioc 0 1) t
⊢ x + t • y ∈ interior s

Tactic:
simpa only [add_sub_cancel_left] using hs.add_smul_sub_mem_interior' hx hy ht

Premises used: add_sub_cancel_left, Convex.add_smul_sub_mem_interior'
-- 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
inst_7 : AddRightMono 𝕜
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ interior s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Ioc 0 1) t
⊢ x + t • y ∈ interior s

Tactic:
hs.add_smul_mem_interior' (subset_closure hx) hy ht

Premises used: subset_closure, Convex.add_smul_mem_interior'
-- 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
inst_7 : ZeroLEOneClass 𝕜
s : Set E
hs : Convex 𝕜 s
⊢ Convex 𝕜 (interior s)

Tactic:
convex_iff_openSegment_subset.mpr fun _ hx _ hy =>
    hs.openSegment_closure_interior_subset_interior (interior_subset_closure hx) hy

Premises used: Iff.mpr, convex_iff_openSegment_subset, Convex.openSegment_closure_interior_subset_interior, interior_subset_closure
-- 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
hs : Convex 𝕜 s
⊢ Convex 𝕜 (closure s)

Tactic:
fun x hx y hy a b ha hb hab =>
  let f : E → E → E := fun x' y' => a • x' + b • y'
  have hf : Continuous (Function.uncurry f) :=
    (continuous_fst.const_smul _).add (continuous_snd.const_smul _)
  show f x y ∈ closure s from map_mem_closure₂ hf hx hy fun _ hx' _ hy' => hs hx' hy' ha hb hab

Premises used: map_mem_closure₂, Set.Mem, continuous_snd, continuous_fst, HAdd.hAdd, Convex, HSMul.hSMul, Continuous.add, Continuous.const_smul, StarConvex
-- 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)
⊢ StrictConvex 𝕜 s

Tactic:
strictConvex_iff_openSegment_subset.2 ?_

Premises used: Iff.mpr, strictConvex_iff_openSegment_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) ↦
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
refine : s.Pairwise fun (x y : E) ↦ openSegment 𝕜 x y ⊆ interior s
⊢ StrictConvex 𝕜 s

Tactic:
refine strictConvex_iff_openSegment_subset.2 ?_

Premises used: Iff.mpr, strictConvex_iff_openSegment_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) ↦
    ∃ (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
pos : ∀ (hx' : x ∈ interior s), openSegment 𝕜 x y ⊆ interior s
neg : ∀ (hx' : x ∉ interior s), openSegment 𝕜 x y ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
by_cases hx' : x ∈ interior s

Premises used: 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
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
hs.openSegment_interior_self_subset_interior hx' 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
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
exact hs.openSegment_interior_self_subset_interior hx' 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
pos : ∀ (hy' : y ∈ interior s), openSegment 𝕜 x y ⊆ interior s
neg : ∀ (hy' : y ∉ interior s), openSegment 𝕜 x y ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
by_cases hy' : y ∈ interior s

Premises used: 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
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
hs.openSegment_self_interior_subset_interior hx hy'

Premises used: Convex.openSegment_self_interior_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
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
exact hs.openSegment_self_interior_subset_interior hx hy'

Premises used: Convex.openSegment_self_interior_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
neg :
  ∀ (c : 𝕜) (hc : Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)),
    openSegment 𝕜 x y ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
rcases h ⟨hx, hx'⟩ ⟨hy, hy'⟩ hne with ⟨c, hc⟩

Premises used: And.intro
-- 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 y ⊆ interior s

Tactic:
(openSegment_subset_union x y ⟨c, rfl⟩).trans
    (insert_subset_iff.2 ⟨hc, union_subset ?_ ?_⟩)

Premises used: Iff.mpr, HasSubset.Subset.trans, Set.union_subset, Set.insert_subset_iff, And.intro, Exists.intro, openSegment_subset_union, rfl
-- 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)
neg : openSegment 𝕜 x ((lineMap x y : (a : 𝕜) → E) c) ⊆ interior s
neg₁ : openSegment 𝕜 ((lineMap x y : (a : 𝕜) → E) c) y ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
refine (openSegment_subset_union x y ⟨c, rfl⟩).trans
    (insert_subset_iff.2 ⟨hc, union_subset ?_ ?_⟩)

Premises used: Iff.mpr, HasSubset.Subset.trans, Set.union_subset, Set.insert_subset_iff, And.intro, Exists.intro, openSegment_subset_union, rfl
-- 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:
hs.openSegment_self_interior_subset_interior hx hc

Premises used: Convex.openSegment_self_interior_subset_interior