awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

Tactic:
exact h hy ha hb hab
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

Tactic:
h hy ⟨a, b, ha, hb, hab, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

Tactic:
exact h hy ⟨a, b, ha, hb, hab, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ [x -[𝕜] y] ⊆ s

Tactic:
starConvex_iff_segment_subset.1 h hy

Premises used: starConvex_iff_segment_subset, Iff.mp
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ openSegment 𝕜 x y ⊆ s

Tactic:
(openSegment_subset_segment 𝕜 x y).trans (h.segment_subset hy)

Premises used: HasSubset.Subset.trans, openSegment_subset_segment, StarConvex.segment_subset
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → HSMul.hSMul (β := Set E) a {x} + b • s ⊆ s

Tactic:
⟨?_, fun h y hy a b ha hb hab =>
      h ha hb hab (add_mem_add (smul_mem_smul_set <| mem_singleton _) ⟨_, hy, rfl⟩)⟩

Premises used: Set.mem_singleton, Set.add_mem_add, And.intro, Iff.intro, Exists.intro, rfl, Set.smul_mem_smul_set
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
fun : StarConvex 𝕜 x s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → HSMul.hSMul (β := Set E) a {x} + b • s ⊆ s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → HSMul.hSMul (β := Set E) a {x} + b • s ⊆ s

Tactic:
refine
    ⟨?_, fun h y hy a b ha hb hab =>
      h ha hb hab (add_mem_add (smul_mem_smul_set <| mem_singleton _) ⟨_, hy, rfl⟩)⟩
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
u : E
hA : StarConvex 𝕜 u s
v : E
hv : v ∈ s
⊢ (fun (x1 x2 : E) ↦ x1 + x2) ((fun (x : E) ↦ a • x) u) ((fun (x : E) ↦ b • x) v) ∈ s

Tactic:
hA hv ha hb hab

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
u : E
hA : StarConvex 𝕜 u s
v : E
hv : v ∈ s
⊢ (fun (x1 x2 : E) ↦ x1 + x2) ((fun (x : E) ↦ a • x) u) ((fun (x : E) ↦ b • x) v) ∈ s

Tactic:
exact hA hv ha hb hab
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
⊢ StarConvex 𝕜 x ∅

Tactic:
fun _ hy => hy.elim

Premises used: False.elim, StarConvex
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
⊢ StarConvex 𝕜 x univ

Tactic:
fun _ _ _ _ _ _ _ => trivial

Premises used: trivial, Set.Mem, Set.univ, setOf, StarConvex
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
⊢ StarConvex 𝕜 x (s ∩ t)

Tactic:
fun _ hy _ _ ha hb hab => ⟨hs hy.left ha hb hab, ht hy.right ha hb hab⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, And.intro, StarConvex
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
S : Set (Set E)
h : ∀ s ∈ S, StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋂₀ S)

Tactic:
fun _ hy _ _ ha hb hab s hs => h s hs (hy s hs) ha hb hab

Premises used: Set.Mem, setOf, Set.sInter, StarConvex
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
ι : Sort u_4
κ : ι → Sort u_5
s : (i : ι) → κ i → Set E
h : ∀ (i : ι) (j : κ i), StarConvex 𝕜 x (s i j)
⊢ StarConvex 𝕜 x (⋂ (i : ι), ⋂ (j : κ i), s i j)

Tactic:
starConvex_iInter fun i => starConvex_iInter (h i)

Premises used: starConvex_iInter
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t

Tactic:
Or.inl (hs hy ha hb hab)

Premises used: Set.union, Set.Mem, setOf, Or.inl
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t

Tactic:
exact Or.inl (hs hy ha hb hab)

Premises used: Or.inl
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t

Tactic:
Or.inr (ht hy ha hb hab)

Premises used: Set.union, Set.Mem, setOf, Or.inr
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t

Tactic:
exact Or.inr (ht hy ha hb hab)

Premises used: Or.inr
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : Membership.mem (γ := Set E) (⋃ (i : ι), s i) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw : ∀ (hy : ∃ (i : ι), y ∈ s i) ⦃a b : 𝕜⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∃ (i : ι), a • x + b • y ∈ s i
⊢ Membership.mem (γ := Set E) (⋃ (i : ι), s i) (a • x + b • y)

Tactic:
rw [mem_iUnion] at hy ⊢

Premises used: Set.mem_iUnion
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : ∃ (i : ι), y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
obtain : ∀ (i : ι) (hy : y ∈ s i), ∃ (i : ι), a • x + b • y ∈ s i
⊢ ∃ (i : ι), a • x + b • y ∈ s i

Tactic:
obtain ⟨i, hy⟩ := hy
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hy : y ∈ s i
⊢ ∃ (i : ι), a • x + b • y ∈ s i

Tactic:
⟨i, hs i hy ha hb hab⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hy : y ∈ s i
⊢ ∃ (i : ι), a • x + b • y ∈ s i

Tactic:
exact ⟨i, hs i hy ha hb hab⟩
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
ι : Sort u_4
κ : ι → Sort u_5
s : (i : ι) → κ i → Set E
h : ∀ (i : ι) (j : κ i), StarConvex 𝕜 x (s i j)
⊢ StarConvex 𝕜 x (⋃ (i : ι), ⋃ (j : κ i), s i j)

Tactic:
starConvex_iUnion fun i => starConvex_iUnion (h i)

Premises used: starConvex_iUnion
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
S : Set (Set E)
hS : ∀ s ∈ S, StarConvex 𝕜 x s
rw : StarConvex 𝕜 x (⋃ (i : (↑S : Type u_2)), (↑i : Set E))
⊢ StarConvex 𝕜 x (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
S : Set (Set E)
hS : ∀ s ∈ S, StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃ (i : (↑S : Type u_2)), (↑i : Set E))

Tactic:
starConvex_iUnion fun s => hS _ s.2

Premises used: starConvex_iUnion, Subtype.val, Subtype.property
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
S : Set (Set E)
hS : ∀ s ∈ S, StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃ (i : (↑S : Type u_2)), (↑i : Set E))

Tactic:
exact starConvex_iUnion fun s => hS _ s.2

Premises used: starConvex_iUnion
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : SMul 𝕜 E
inst_5 : SMul 𝕜 F
x : E
y : F
s : Set E
t : Set F
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x, y) (s ×ˢ t)

Tactic:
fun _ hy _ _ ha hb hab =>
  ⟨hs hy.1 ha hb hab, ht hy.2 ha hb hab⟩

Premises used: Set.Mem, setOf, Set.prod, And.right, And.left, And.intro, StarConvex
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
ι : Type u_4
E : ι → Type u_5
inst_2 : (i : ι) → AddCommMonoid (E i)
inst_3 : (i : ι) → SMul.{u_1, u_5} 𝕜 (E i)
x : (i : ι) → E i
s : Set ι
t : (i : ι) → Set (E i)
ht : ∀ ⦃i : ι⦄, i ∈ s → StarConvex 𝕜 (x i) (t i)
⊢ StarConvex 𝕜 x (s.pi (α := E) t)

Tactic:
fun _ hy _ _ ha hb hab i hi => ht hi (hy i hi) ha hb hab

Premises used: Set.Mem, setOf, Set.pi, StarConvex
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
inst_4 : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
h : s.Nonempty
obtain : ∀ (y : E) (hy : y ∈ s), x ∈ s
⊢ x ∈ s

Tactic:
obtain ⟨y, hy⟩ := h
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
inst_4 : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s

Tactic:
hs hy zero_le_one le_rfl (add_zero 1)

Premises used: le_rfl, zero_le_one, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
inst_4 : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
h : x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
⊢ x ∈ s

Tactic:
convert! hs hy zero_le_one le_rfl (add_zero 1)

Premises used: le_rfl, zero_le_one, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
inst_4 : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
h : x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
h₁ : x = x + 0
h₂ h₃ : x = x
⊢ x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y

Tactic:
rw [one_smul, zero_smul, add_zero]

Premises used: one_smul, zero_smul, add_zero
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
⟨fun h y hy a b ha hb hab => h hy ha.le hb.le hab, ?_⟩

Premises used: LT.lt.le, Iff.intro
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
refine : (∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) → StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
refine ⟨fun h y hy a b ha hb hab => h hy ha.le hb.le hab, ?_⟩
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
inl : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
inr : ∀ (ha : 0 < a), a • x + b • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
obtain rfl | ha := ha.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
⊢ b = 1

Tactic:
rw [zero_add] at hab

Premises used: zero_add
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
inl : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y ∈ s
inl₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + y ∈ s
inl₂ : 0 + y ∈ s
inl₃ inl₄ inl₅ inl₆ : y ∈ s
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s

Tactic:
rwa [hab, one_smul, zero_smul, zero_add]

Premises used: zero_add, one_smul, zero_smul
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha_1 : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha : 0 < a
inr : ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1), a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
inr₁ : ∀ (hb : 0 < b), a • x + b • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
obtain rfl | hb := hb.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha_1 : 0 ≤ a
ha : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
⊢ a = 1

Tactic:
rw [add_zero] at hab

Premises used: add_zero
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha_1 : 0 ≤ a
ha : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
inr : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
inr₁ : x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
inr₂ : x + 0 ∈ s
inr₃ inr₄ inr₅ inr₆ : x ∈ s
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s

Tactic:
rwa [hab, one_smul, zero_smul, add_zero]

Premises used: one_smul, zero_smul, add_zero
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha_1 : 0 ≤ a
hb_1 : 0 ≤ b
hab : a + b = 1
ha : 0 < a
hb : 0 < b
⊢ a • x + b • y ∈ s

Tactic:
h hy ha hb hab
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha_1 : 0 ≤ a
hb_1 : 0 ≤ b
hab : a + b = 1
ha : 0 < a
hb : 0 < b
⊢ a • x + b • y ∈ s

Tactic:
exact h hy ha hb hab
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
⟨fun h y hy _ a b ha hb hab => h hy ha.le hb.le hab, ?_⟩

Premises used: LT.lt.le, Iff.intro
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
refine : (∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) → StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
refine ⟨fun h y hy _ a b ha hb hab => h hy ha.le hb.le hab, ?_⟩
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
inl : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
inr : ∀ (ha' : 0 < a), a • x + b • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
⊢ b = 1

Tactic:
rw [zero_add] at hab

Premises used: zero_add
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
inl : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y ∈ s
inl₁ : 0 + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y ∈ s
inl₂ : 0 + y ∈ s
inl₃ inl₄ inl₅ inl₆ : y ∈ s
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s

Tactic:
rwa [hab, zero_smul, one_smul, zero_add]

Premises used: zero_add, one_smul, zero_smul
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
inr : ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1), a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
inr₁ : ∀ (hb' : 0 < b), a • x + b • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
obtain rfl | hb' := hb.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha : 0 ≤ a
ha' : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
⊢ a = 1

Tactic:
rw [add_zero] at hab

Premises used: add_zero
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha : 0 ≤ a
ha' : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
inr : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
inr₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + 0 ∈ s
inr₂ : x + 0 ∈ s
inr₃ inr₄ inr₅ inr₆ : x ∈ s
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s

Tactic:
rwa [hab, zero_smul, one_smul, add_zero]

Premises used: one_smul, zero_smul, add_zero
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
hb' : 0 < b
inr : ∀ (hy : x ∈ s), a • x + b • x ∈ s
inr₁ : ∀ (hxy : x ≠ y), a • x + b • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
obtain rfl | hxy := eq_or_ne x y

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
hb' : 0 < b
hy inr inr₁ inr₂ inr₃ : x ∈ s
⊢ a • x + b • x ∈ s

Tactic:
rwa [Convex.combo_self hab]

Premises used: Convex.combo_self
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
hb' : 0 < b
hxy : x ≠ y
⊢ a • x + b • y ∈ s

Tactic:
h hy hxy ha' hb' hab
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
hb' : 0 < b
hxy : x ≠ y
⊢ a • x + b • y ∈ s

Tactic:
exact h hy hxy ha' hb' hab