awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
⊢ Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s

Tactic:
forall₂_congr fun _ _ => starConvex_iff_segment_subset

Premises used: starConvex_iff_segment_subset, forall₂_congr, Convex
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ [x -[𝕜] y] ⊆ s

Tactic:
convex_iff_segment_subset.1 h hx hy

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

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

Premises used: HasSubset.Subset.trans, openSegment_subset_segment, Convex.segment_subset
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
simp_rw :
  (∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
⊢ Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

Tactic:
simp_rw [convex_iff_segment_subset, segment_subset_iff]

Premises used: convex_iff_segment_subset, segment_subset_iff
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
hA : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
u : E
hu : 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 hu hv ha hb hab

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
hA : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
u : E
hu : 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 hu hv ha hb hab
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
⊢ Convex.{u_1, u_2} 𝕜 (E := E) ∅

Tactic:
fun _ => False.elim

Premises used: Set.Mem, False.elim, Convex
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
⊢ Convex.{u_1, u_2} 𝕜 (E := E) univ

Tactic:
fun _ _ => starConvex_univ _

Premises used: Convex, starConvex_univ
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s ∩ t)

Tactic:
fun _ hx => (hs hx.1).inter (ht hx.2)

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

Tactic:
fun _ hx =>
  starConvex_sInter fun _ hs => h _ hs <| hx _ hs

Premises used: starConvex_sInter, Convex
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
ι : Sort u_5
κ : ι → Sort u_6
s : (i : ι) → κ i → Set E
h : ∀ (i : ι) (j : κ i), Convex 𝕜 (s i j)
⊢ Convex.{u_1, u_2} 𝕜 (E := E) (⋂ (i : ι), ⋂ (j : κ i), s i j)

Tactic:
convex_iInter fun i => convex_iInter <| h i

Premises used: convex_iInter
-- Module: Mathlib.Analysis.Convex.Basic
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
s : Set E
t : Set F
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s ×ˢ t)

Tactic:
fun _ hx => (hs hx.1).prod (ht hx.2)

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

Tactic:
fun _ hx => starConvex_pi fun _ hi => ht hi <| hx _ hi

Premises used: Convex, starConvex_pi
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x : E
hx : Membership.mem (γ := Set E) (⋃ (i : ι), s i) x
y : E
hy : Membership.mem (γ := Set E) (⋃ (i : ι), s i) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw :
  ∀ (hx : ∃ (i : ι), x ∈ s i) ⦃y : E⦄ (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 hx hy ⊢

Premises used: Set.mem_iUnion
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x : E
hx : ∃ (i : ι), x ∈ s i
y : E
hy : ∃ (i : ι), y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
obtain : ∀ (i : ι) (hx : x ∈ s i), ∃ (i : ι), a • x + b • y ∈ s i
⊢ ∃ (i : ι), a • x + b • y ∈ s i

Tactic:
obtain ⟨i, hx⟩ := hx
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x y : E
hy : ∃ (i : ι), y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hx : x ∈ s i
obtain : ∀ (j : ι) (hy : y ∈ s j), ∃ (i : ι), a • x + b • y ∈ s i
⊢ ∃ (i : ι), a • x + b • y ∈ s i

Tactic:
obtain ⟨j, hy⟩ := hy
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
obtain : ∀ (k : ι) (hik : s i ⊆ s k) (hjk : s j ⊆ s k), ∃ (i : ι), a • x + b • y ∈ s i
⊢ ∃ (i : ι), a • x + b • y ∈ s i

Tactic:
obtain ⟨k, hik, hjk⟩ := hdir i j
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ ∃ (i : ι), a • x + b • y ∈ s i

Tactic:
⟨k, hc (hik hx) (hjk hy) ha hb hab⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ ∃ (i : ι), a • x + b • y ∈ s i

Tactic:
exact ⟨k, hc (hik hx) (hjk hy) ha hb hab⟩
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
c : Set (Set E)
hdir : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
rw : Convex.{u_1, u_2} 𝕜 (E := E) (⋃ (i : (↑c : Type u_2)), (↑i : Set E))
⊢ Convex 𝕜 (⋃₀ c)

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
c : Set (Set E)
hdir : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex.{u_1, u_2} 𝕜 (E := E) (⋃ (i : (↑c : Type u_2)), (↑i : Set E))

Tactic:
(directedOn_iff_directed.1 hdir).convex_iUnion fun A => hc A.2

Premises used: Directed.convex_iUnion, directedOn_iff_directed, Iff.mp, Subtype.property
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
c : Set (Set E)
hdir : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex.{u_1, u_2} 𝕜 (E := E) (⋃ (i : (↑c : Type u_2)), (↑i : Set E))

Tactic:
exact (directedOn_iff_directed.1 hdir).convex_iUnion fun A => hc A.2

Premises used: Directed.convex_iUnion, directedOn_iff_directed, Iff.mp, Subtype.property
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
P : Prop
hs : Convex 𝕜 s
pos : ∀ (hP : P), Convex.{u_1, u_2} 𝕜 (E := E) {x : E | P → x ∈ s}
neg : ∀ (hP : ¬P), Convex.{u_1, u_2} 𝕜 (E := E) {x : E | P → x ∈ s}
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | P → x ∈ s}

Tactic:
by_cases hP : P
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
P : Prop
hs : Convex 𝕜 s
hP : P
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | P → x ∈ s}

Tactic:
simp [hP, hs, convex_univ]

Premises used: convex_univ
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
P : Prop
hs : Convex 𝕜 s
hP : ¬P
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | P → x ∈ s}

Tactic:
simp [hP, hs, convex_univ]

Premises used: convex_univ
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : ZeroLEOneClass 𝕜
⊢ Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → openSegment 𝕜 x y ⊆ s

Tactic:
forall₂_congr fun _ => starConvex_iff_openSegment_subset

Premises used: starConvex_iff_openSegment_subset, forall₂_congr, Convex
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
forall₂_congr fun _ => starConvex_iff_forall_pos

Premises used: forall₂_congr, Convex, starConvex_iff_forall_pos
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ Convex 𝕜 s ↔ s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
convex_iff_forall_pos.trans ⟨fun h x hx y hy _ => h hx hy, ?_⟩

Premises used: Iff.intro, Iff.trans, convex_iff_forall_pos
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
refine :
  (s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) →
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
⊢ Convex 𝕜 s ↔ s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
refine convex_iff_forall_pos.trans ⟨fun h x hx y hy _ => h hx hy, ?_⟩

Premises used: Iff.intro, Iff.trans, convex_iff_forall_pos
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inl : ∀ (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.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hy inl inl₁ inl₂ inl₃ : x ∈ s
⊢ a • x + b • x ∈ s

Tactic:
rwa [Convex.combo_self hab]

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

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

Tactic:
exact h hx hy hxy ha hb hab
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
inst_4 : ZeroLEOneClass 𝕜
hs : Convex 𝕜 s
h : s.Nonempty
⊢ StarConvex 𝕜 x s ↔ x ∈ s

Tactic:
⟨fun hxs => hxs.mem h, hs.starConvex⟩

Premises used: Iff.intro, Convex.starConvex, StarConvex.mem
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
h : s.Subsingleton
⊢ Convex 𝕜 s

Tactic:
convex_iff_pairwise_pos.mpr (h.pairwise _)

Premises used: Iff.mpr, convex_iff_pairwise_pos, Set.Subsingleton.pairwise
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
c : E
⊢ Convex 𝕜 (E := E) {c}

Tactic:
subsingleton_singleton.convex

Premises used: Set.Subsingleton.convex, Set.subsingleton_singleton
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
⊢ Convex.{u_1, u_2} 𝕜 (E := E) 0

Tactic:
convex_singleton _

Premises used: convex_singleton
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (ap • x + bp • y) + b • (aq • x + bq • y) ∈ [x -[𝕜] y]

Tactic:
⟨a * ap + b * aq, a * bp + b * bq, add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
      add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), ?_, ?_⟩

Premises used: mul_nonneg, HMul.hMul, Set.Mem, setOf, add_nonneg, segment, HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_1 : a * ap + b * aq + (a * bp + b * bq) = 1
refine_2 : (a * ap + b * aq) • x + (a * bp + b * bq) • y = a • (ap • x + bp • y) + b • (aq • x + bq • y)
⊢ a • (ap • x + bp • y) + b • (aq • x + bq • y) ∈ [x -[𝕜] y]

Tactic:
refine
    ⟨a * ap + b * aq, a * bp + b * bq, add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
      add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_1 : a * ap + a * bp + (b * aq + b * bq) = 1
refine_1₁ : a * (ap + bp) + (b * aq + b * bq) = 1
refine_1₂ : a * (ap + bp) + b * (aq + bq) = 1
refine_1₃ : a * 1 + b * (aq + bq) = 1
refine_1₄ : a * 1 + b * 1 = 1
refine_1₅ : a + b * 1 = 1
refine_1₆ : a + b = 1
refine_1₇ refine_1₈ : Eq.{u_1 + 1} (α := 𝕜) 1 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1

Tactic:
rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]

Premises used: mul_add, add_add_add_comm, mul_one
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
match_scalars : (a * ap + b * aq) * 1 = a * (ap * 1) + b * (aq * 1)
match_scalars₁ : (a * bp + b * bq) * 1 = a * (bp * 1) + b * (bq * 1)
⊢ (a * ap + b * aq) • x + (a * bp + b * bq) • y = a • (ap • x + bp • y) + b • (aq • x + bq • y)

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * ap + b * aq) * 1 = a * (ap * 1) + b * (aq * 1)

Tactic:
noncomm_ring
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * bp + b * bq) * 1 = a * (bp * 1) + b * (bq * 1)

Tactic:
noncomm_ring
-- Module: Mathlib.Analysis.Convex.Basic
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 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw :
  HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) (a • x) : F) ((f : (a : E) → F) (b • y) : F) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
rw₁ :
  HAdd.hAdd (β := F) (HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F)) ((f : (a : E) → F) (b • y) : F) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
rw₂ rw₃ :
  HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
⊢ (f : (a : E) → F) (a • x + b • y) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)

Tactic:
rw [f.map_add, f.map_smul, f.map_smul]

Premises used: LinearMap.map_add, LinearMap.map_smul
-- Module: Mathlib.Analysis.Convex.Basic
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 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s)
    (HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F))

Tactic:
exact ⟨a • x + b • y, hs hx hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩
-- Module: Mathlib.Analysis.Convex.Basic
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 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
f : E → F
hf : IsLinearMap 𝕜 f
⊢ Convex 𝕜 (f '' s)

Tactic:
hs.linear_image <| hf.mk' f

Premises used: Convex.linear_image, IsLinearMap.mk'
-- Module: Mathlib.Analysis.Convex.Basic
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 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw : HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F) ∈ s
⊢ Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) (a • x + b • y)

Tactic:
rw [mem_preimage, f.map_add, LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower]

Premises used: LinearMap.map_add, LinearMap.map_smul_of_tower, Set.mem_preimage
-- Module: Mathlib.Analysis.Convex.Basic
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 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F) ∈ s

Tactic:
hs hx hy ha hb hab

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Convex.Basic
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 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F) ∈ s

Tactic:
exact hs hx hy ha hb hab
-- Module: Mathlib.Analysis.Convex.Basic
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 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E → F
hf : IsLinearMap 𝕜 f
⊢ Convex 𝕜 (f ⁻¹' s)

Tactic:
hs.linear_preimage <| hf.mk' f

Premises used: IsLinearMap.mk', Convex.linear_preimage
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
rw : Convex 𝕜 (E := E) ((fun (x : E × E) ↦ x.1 + x.2) '' s ×ˢ t)
⊢ Convex 𝕜 (s + t)

Tactic:
rw [← add_image_prod]

Premises used: Set.add_image_prod
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (E := E) ((fun (x : E × E) ↦ x.1 + x.2) '' s ×ˢ t)

Tactic:
(hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

Premises used: Convex.prod, Convex.is_linear_image, IsLinearMap.isLinearMap_add