awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
a : x + t • (y - x) ∈ [x -[𝕜] y]
⊢ x + t • (y - x) ∈ s

Tactic:
apply hs.segment_subset hy

Premises used: StarConvex.segment_subset
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
a : Membership.mem (γ := Set E) ((fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Icc 0 1) (x + t • (y - x))
⊢ x + t • (y - x) ∈ [x -[𝕜] y]

Tactic:
rw [segment_eq_image']

Premises used: segment_eq_image'
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ Membership.mem (γ := Set E) ((fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Icc 0 1) (x + t • (y - x))

Tactic:
mem_image_of_mem _ ⟨ht₀, ht₁⟩

Premises used: Set.mem_image_of_mem, And.intro
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ Membership.mem (γ := Set E) ((fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Icc 0 1) (x + t • (y - x))

Tactic:
exact mem_image_of_mem _ ⟨ht₀, ht₁⟩
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set F
hs : StarConvex 𝕜 ((f : (a : E) → F) x) s
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, Convex.combo_affine_apply hab]

Premises used: Set.mem_preimage, Convex.combo_affine_apply
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set F
hs : StarConvex 𝕜 ((f : (a : E) → F) x) s
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 hy ha hb hab
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set F
hs : StarConvex 𝕜 ((f : (a : E) → F) x) s
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 hy ha hb hab
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : (f : (a : E) → F) y' = y
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) + b • y)

Tactic:
⟨a • x + b • y', ⟨hs hy' ha hb hab, ?_⟩⟩

Premises used: Set.Mem, setOf, HAdd.hAdd, And.intro, Exists.intro, Set.image, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : (f : (a : E) → F) y' = y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine : (f : (a : E) → F) (a • x + b • y') = HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + b • y
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) (HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + b • y)

Tactic:
refine ⟨a • x + b • y', ⟨hs hy' ha hb hab, ?_⟩⟩
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : (f : (a : E) → F) y' = 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) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + b • y
rw₁ rw₂ :
  HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + b • y = HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + b • y
⊢ (f : (a : E) → F) (a • x + b • y') = HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + b • y

Tactic:
rw [Convex.combo_affine_apply hab, hy'f]

Premises used: Convex.combo_affine_apply
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
rw : StarConvex 𝕜 (-x) ((fun (x : E) ↦ -x) '' s)
⊢ StarConvex 𝕜 (-x) (-s)

Tactic:
rw [← image_neg_eq_neg]

Premises used: Set.image_neg_eq_neg
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
⊢ StarConvex 𝕜 (-x) ((fun (x : E) ↦ -x) '' s)

Tactic:
hs.is_linear_image IsLinearMap.isLinearMap_neg

Premises used: StarConvex.is_linear_image, IsLinearMap.isLinearMap_neg
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
⊢ StarConvex 𝕜 (-x) ((fun (x : E) ↦ -x) '' s)

Tactic:
exact hs.is_linear_image IsLinearMap.isLinearMap_neg

Premises used: StarConvex.is_linear_image, IsLinearMap.isLinearMap_neg
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
simp_rw : StarConvex 𝕜 (x + -y) (s + -t)
⊢ StarConvex 𝕜 (x - y) (s - t)

Tactic:
simp_rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + -y) (s + -t)

Tactic:
hs.add ht.neg

Premises used: StarConvex.add, StarConvex.neg
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + -y) (s + -t)

Tactic:
exact hs.add ht.neg

Premises used: StarConvex.add, StarConvex.neg
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
⊢ y ∈ (Iic x)ᶜ

Tactic:
simp [h.not_ge]

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
refine : ∀ (z : E) (hz : z ∈ (Iic x)ᶜ) (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), a • y + b • z ∈ (Iic x)ᶜ
⊢ StarConvex 𝕜 y (Iic x)ᶜ

Tactic:
refine (starConvex_iff_forall_pos <| by simp [h.not_ge]).mpr fun z hz a b ha hb hab ↦ ?_

Premises used: Iff.mpr, starConvex_iff_forall_pos
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
hz : z ∈ (Iic x)ᶜ
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
rw : ∀ (hz : ¬z ≤ x) (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), ¬a • y + b • z ≤ x
⊢ a • y + b • z ∈ (Iic x)ᶜ

Tactic:
rw [mem_compl_iff, mem_Iic] at hz ⊢

Premises used: Set.mem_Iic, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
hz : ¬z ≤ x
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
contrapose : ∀ (hz : a • y + b • z ≤ x), z ≤ x
⊢ ¬a • y + b • z ≤ x

Tactic:
contrapose hz
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ z ≤ x

Tactic:
(lt_of_smul_lt_smul_of_nonneg_left ?_ hb.le).le

Premises used: LT.lt.le, lt_of_smul_lt_smul_of_nonneg_left
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
refine : b • z < b • x
⊢ z ≤ x

Tactic:
refine (lt_of_smul_lt_smul_of_nonneg_left ?_ hb.le).le

Premises used: LT.lt.le, lt_of_smul_lt_smul_of_nonneg_left
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
rwa : a • y + b • z ≤ (a + b) • x
rwa₁ : a • y + b • z ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x
rwa₂ rwa₃ rwa₄ rwa₅ : a • y + b • z ≤ x
⊢ b • z ≤ (a + b) • x - a • y

Tactic:
rwa [le_sub_iff_add_le', hab, one_smul]

Premises used: le_sub_iff_add_le', one_smul
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
rw : a • x + b • x < a • y + b • x
⊢ (a + b) • x - a • y < b • x

Tactic:
rw [add_smul, sub_lt_iff_lt_add']

Premises used: sub_lt_iff_lt_add', add_smul
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
bc : 0 < a
⊢ a • x + b • x < a • y + b • x

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
b₁ : b • z ≤ (a + b) • x - a • y
b₂ : (a + b) • x - a • y < b • x
⊢ b • z < b • x

Tactic:
calc
    b • z ≤ (a + b) • x - a • y := by rwa [le_sub_iff_add_le', hab, one_smul]
    _ < b • x := by
      rw [add_smul, sub_lt_iff_lt_add']
      gcongr

Premises used: HAdd.hAdd
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
⊢ StarConvex 𝕜 x (Ici y)ᶜ

Tactic:
starConvex_compl_Iic (E := Eᵒᵈ) h

Premises used: Set.Ici, Set.Mem, setOf, starConvex_compl_Iic, OrderDual
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
a₁ : 0 ≤ a / (a + b)
a₂ : 0 ≤ b / (a + b)
a₃ : a / (a + b) + b / (a + b) = 1
⊢ (a / (a + b)) • x + (b / (a + b)) • y ∈ s

Tactic:
apply h hy
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ 0 ≤ a / (a + b)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ 0 ≤ b / (a + b)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
a₁ : (a + b) / (a + b) = 1
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
rw [← add_div]

Premises used: add_div
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ (a + b) / (a + b) = 1

Tactic:
div_self hab.ne'

Premises used: LT.lt.ne', div_self
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ (a + b) / (a + b) = 1

Tactic:
exact div_self hab.ne'

Premises used: LT.lt.ne', div_self
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s

Tactic:
have h' := h hy ha hb
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h' : 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
⊢ LT.lt.{u_1} (α := 𝕜) 0 1 → a • x + b • y ∈ s

Tactic:
rw [hab, div_one, div_one] at h'

Premises used: div_one
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h' : LT.lt.{u_1} (α := 𝕜) 0 1 → a • x + b • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
h' zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h' : LT.lt.{u_1} (α := 𝕜) 0 1 → a • x + b • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
exact h' zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
rw : t⁻¹ • x ∈ s
⊢ x ∈ t • s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']

Premises used: LT.lt.ne', zero_lt_one, LT.lt.trans_le, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ 0 ≤ t⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ t⁻¹ • x ∈ s

Tactic:
exact hs.smul_mem hx (by positivity) (inv_le_one_of_one_le₀ ht)

Premises used: StarConvex.smul_mem, inv_le_one_of_one_le₀
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
inl : ∀ (hxy : x ≤ y), a • x + b • y ∈ s
inr : ∀ (hyx : y ≤ x), a • x + b • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
obtain hxy | hyx := h _ 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 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
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:
hs.out hx hy (mem_Icc.2 ⟨?_, ?_⟩)

Premises used: Iff.mpr, Set.OrdConnected.out, And.intro, Set.mem_Icc
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
inl : x ≤ a • x + b • y
inl₁ : a • x + b • y ≤ y
⊢ a • x + b • y ∈ s

Tactic:
refine hs.out hx hy (mem_Icc.2 ⟨?_, ?_⟩)

Premises used: Iff.mpr, Set.OrdConnected.out, And.intro, Set.mem_Icc
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ x = a • x + b • x

Tactic:
(Convex.combo_self hab _).symm

Premises used: Convex.combo_self, Eq.symm
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
bc : 0 ≤ b
⊢ a • x + b • x ≤ a • x + b • y

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
x₁ : a • x + b • x ≤ a • x + b • y
⊢ x ≤ a • x + b • y

Tactic:
calc
        x = a • x + b • x := (Convex.combo_self hab _).symm
        _ ≤ a • x + b • y := by gcongr

Premises used: Convex.combo_self, Eq.symm
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
bc : 0 ≤ a
⊢ a • x + b • y ≤ a • y + b • y

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ a • y + b • y = y

Tactic:
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 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
a₁ : a • x + b • y ≤ a • y + b • y
⊢ a • x + b • y ≤ y

Tactic:
calc
      a • x + b • y ≤ a • y + b • y := by gcongr
      _ = y := 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 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ a • x + b • y ∈ s

Tactic:
hs.out hy hx (mem_Icc.2 ⟨?_, ?_⟩)

Premises used: Iff.mpr, Set.OrdConnected.out, And.intro, Set.mem_Icc
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
inr : y ≤ a • x + b • y
inr₁ : a • x + b • y ≤ x
⊢ a • x + b • y ∈ s

Tactic:
refine hs.out hy hx (mem_Icc.2 ⟨?_, ?_⟩)

Premises used: Iff.mpr, Set.OrdConnected.out, And.intro, Set.mem_Icc