awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
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.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedCancelAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
left : x < a • x + b • y
right : a • x + b • y < y
⊢ a • x + b • y ∈ Ioo x y

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedCancelAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ x = a • x + b • x

Tactic:
(Convex.combo_self hab _).symm

Premises used: Convex.combo_self, Eq.symm
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedCancelAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
bc : 0 < b
⊢ a • x + b • x < a • x + b • y

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedCancelAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
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.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedCancelAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
bc : 0 < a
⊢ a • x + b • y < a • y + b • y

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedCancelAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • y + b • y = y

Tactic:
Convex.combo_self hab _

Premises used: Convex.combo_self
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedCancelAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
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.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x y : E
inl : ∀ (h : x ≤ y), [x -[𝕜] y] ⊆ uIcc x y
inr : ∀ (h : y ≤ x), [x -[𝕜] y] ⊆ uIcc x y
⊢ [x -[𝕜] y] ⊆ uIcc x y

Tactic:
rcases le_total x y with h | h

Premises used: le_total
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x y : E
h : x ≤ y
inl : [x -[𝕜] y] ⊆ Icc x y
⊢ [x -[𝕜] y] ⊆ uIcc x y

Tactic:
rw [uIcc_of_le h]

Premises used: Set.uIcc_of_le
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x y : E
h : x ≤ y
⊢ [x -[𝕜] y] ⊆ Icc x y

Tactic:
segment_subset_Icc h

Premises used: segment_subset_Icc
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x y : E
h : x ≤ y
⊢ [x -[𝕜] y] ⊆ Icc x y

Tactic:
exact segment_subset_Icc h

Premises used: segment_subset_Icc
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x y : E
h : y ≤ x
inr : [y -[𝕜] x] ⊆ Icc y x
⊢ [x -[𝕜] y] ⊆ uIcc x y

Tactic:
rw [uIcc_of_ge h, segment_symm]

Premises used: Set.uIcc_of_ge, segment_symm
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x y : E
h : y ≤ x
⊢ [y -[𝕜] x] ⊆ Icc y x

Tactic:
segment_subset_Icc h

Premises used: segment_subset_Icc
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x y : E
h : y ≤ x
⊢ [y -[𝕜] x] ⊆ Icc y x

Tactic:
exact segment_subset_Icc h

Premises used: segment_subset_Icc
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
a b : 𝕜
x y : E
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ min x y ≤ a • x + b • y

Tactic:
(segment_subset_uIcc x y ⟨_, _, ha, hb, hab, rfl⟩).1

Premises used: And.left, And.intro, Exists.intro, segment_subset_uIcc, rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
a b : 𝕜
x y : E
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ≤ max x y

Tactic:
(segment_subset_uIcc x y ⟨_, _, ha, hb, hab, rfl⟩).2

Premises used: And.right, And.intro, Exists.intro, segment_subset_uIcc, rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
inl : ∀ (hyz : z ≤ x), z ∈ [x -[𝕜] x]
inr : ∀ (h : x < y), z ∈ [x -[𝕜] y]
⊢ z ∈ [x -[𝕜] y]

Tactic:
obtain rfl | h := (hxz.trans hyz).eq_or_lt

Premises used: LE.le.eq_or_lt, LE.le.trans, rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
inl : Membership.mem (γ := Set 𝕜) {x} z
⊢ z ∈ [x -[𝕜] x]

Tactic:
rw [segment_same]

Premises used: segment_same
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ Membership.mem (γ := Set 𝕜) {x} z

Tactic:
hyz.antisymm hxz

Premises used: Set.Mem, setOf, LE.le.antisymm, Set.singleton
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ Membership.mem (γ := Set 𝕜) {x} z

Tactic:
exact hyz.antisymm hxz

Premises used: LE.le.antisymm
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
⊢ 0 ≤ z - x

Tactic:
rw [← sub_nonneg] at hxz hyz

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
hxz₁ : 0 ≤ z - x
⊢ 0 ≤ y - z

Tactic:
rw [← sub_nonneg] at hxz hyz

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
hxz₁ : 0 ≤ z - x
hyz₁ : 0 ≤ y - z
⊢ x < y

Tactic:
rw [← sub_nonneg] at hxz hyz

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : x < y
⊢ 0 < y - x

Tactic:
rw [← sub_pos] at h

Premises used: sub_pos
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ z ∈ [x -[𝕜] y]

Tactic:
⟨(y - z) / (y - x), (z - x) / (y - x), div_nonneg hyz h.le, div_nonneg hxz h.le, ?_, ?_⟩

Premises used: Set.Mem, setOf, HSub.hSub, HDiv.hDiv, LT.lt.le, segment, And.intro, Exists.intro, div_nonneg
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
inr : (y - z) / (y - x) + (z - x) / (y - x) = 1
inr₁ : ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
⊢ z ∈ [x -[𝕜] y]

Tactic:
refine ⟨(y - z) / (y - x), (z - x) / (y - x), div_nonneg hyz h.le, div_nonneg hxz h.le, ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
inr : (y - z + (z - x)) / (y - x) = 1
inr₁ : (y - x) / (y - x) = 1
inr₂ inr₃ : Eq.{u_1 + 1} (α := 𝕜) 1 1
⊢ (y - z) / (y - x) + (z - x) / (y - x) = 1

Tactic:
rw [← add_div, sub_add_sub_cancel, div_self h.ne']

Premises used: sub_add_sub_cancel, LT.lt.ne', div_self, add_div
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
inr : (y - z) / (y - x) * x + ((z - x) / (y - x)) • y = z
inr₁ : (y - z) / (y - x) * x + (z - x) / (y - x) * y = z
inr₂ : (y - z) * x / (y - x) + (z - x) / (y - x) * y = z
inr₃ : (y - z) * x / (y - x) + (z - x) * y / (y - x) = z
inr₄ : ((y - z) * x + (z - x) * y) / (y - x) = z
inr₅ : (y - z) * x + (z - x) * y = z * (y - x)
inr₆ : (z - x) * y + (y - z) * x = z * (y - x)
inr₇ : z * y - x * y + (y - z) * x = z * (y - x)
inr₈ : z * y - x * y + (y * x - z * x) = z * (y - x)
inr₉ : z * y - y * x + (y * x - z * x) = z * (y - x)
inr₁₀ : z * y - z * x = z * (y - x)
inr₁₁ inr₁₂ : z * y - z * x = z * y - z * x
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z

Tactic:
rw [smul_eq_mul, smul_eq_mul, ← mul_div_right_comm, ← mul_div_right_comm, ← add_div,
      div_eq_iff h.ne', add_comm, sub_mul, sub_mul, mul_comm x, sub_add_sub_cancel, mul_sub]

Premises used: sub_add_sub_cancel, mul_sub, add_comm, mul_div_right_comm, LT.lt.ne', sub_mul, div_eq_iff, mul_comm, smul_eq_mul, add_div
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x ≤ y
⊢ [x -[𝕜] y] = Icc x y

Tactic:
(segment_subset_Icc h).antisymm Icc_subset_segment

Premises used: segment_subset_Icc, HasSubset.Subset.antisymm, Icc_subset_segment
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
⊢ Ioo x y ⊆ openSegment 𝕜 x y

Tactic:
fun _ hz =>
  mem_openSegment_of_ne_left_right hz.1.ne hz.2.ne' <| Icc_subset_segment <| Ioo_subset_Icc_self hz

Premises used: Set.Ioo_subset_Icc_self, Set.Mem, mem_openSegment_of_ne_left_right, Set.Subset, LT.lt.ne', And.right, And.left, LT.lt.ne, Icc_subset_segment
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
⊢ openSegment 𝕜 x y = Ioo x y

Tactic:
(openSegment_subset_Ioo h).antisymm Ioo_subset_openSegment

Premises used: Ioo_subset_openSegment, HasSubset.Subset.antisymm, openSegment_subset_Ioo
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
inl : ∀ (h : x ≤ y), [x -[𝕜] y] = Icc (min x y) (max x y)
inr : ∀ (h : y ≤ x), [x -[𝕜] y] = Icc (min x y) (max x y)
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)

Tactic:
rcases le_total x y with h | h

Premises used: le_total
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x ≤ y
inl : Icc x y = Icc (min x y) (max x y)
inl₁ : Icc x y = Icc (min x y) y
inl₂ inl₃ : Icc x y = Icc x y
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)

Tactic:
rw [segment_eq_Icc h, max_eq_right h, min_eq_left h]

Premises used: segment_eq_Icc, max_eq_right, min_eq_left
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : y ≤ x
inr : [y -[𝕜] x] = Icc (min x y) (max x y)
inr₁ : Icc y x = Icc (min x y) (max x y)
inr₂ : Icc y x = Icc (min x y) x
inr₃ inr₄ : Icc y x = Icc y x
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)

Tactic:
rw [segment_symm, segment_eq_Icc h, max_eq_left h, min_eq_right h]

Premises used: segment_symm, segment_eq_Icc, max_eq_left, min_eq_right
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
inl : ∀ (h : x < y), openSegment 𝕜 x y = Ioo (min x y) (max x y)
inr : ∀ (h : y < x), openSegment 𝕜 x y = Ioo (min x y) (max x y)
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)

Tactic:
rcases hxy.lt_or_gt with h | h

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : x < y
inl : Ioo x y = Ioo (min x y) (max x y)
inl₁ : Ioo x y = Ioo (min x y) y
inl₂ inl₃ : Ioo x y = Ioo x y
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)

Tactic:
rw [openSegment_eq_Ioo h, max_eq_right h.le, min_eq_left h.le]

Premises used: openSegment_eq_Ioo, LT.lt.le, max_eq_right, min_eq_left
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : y < x
inr : openSegment 𝕜 y x = Ioo (min x y) (max x y)
inr₁ : Ioo y x = Ioo (min x y) (max x y)
inr₂ : Ioo y x = Ioo (min x y) x
inr₃ inr₄ : Ioo y x = Ioo y x
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)

Tactic:
rw [openSegment_symm, openSegment_eq_Ioo h, max_eq_left h.le, min_eq_right h.le]

Premises used: openSegment_eq_Ioo, LT.lt.le, max_eq_left, min_eq_right, openSegment_symm
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
⊢ [x -[𝕜] y] = uIcc x y

Tactic:
segment_eq_Icc' _ _

Premises used: segment_eq_Icc', Set.uIcc
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x ≤ y
⊢ z ∈ Icc x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
simp only [← segment_eq_Icc h, segment, mem_setOf_eq, smul_eq_mul, exists_and_left]

Premises used: exists_and_left, segment_eq_Icc, Set.mem_setOf_eq, segment, smul_eq_mul
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ioo x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
simp only [← openSegment_eq_Ioo h, openSegment, smul_eq_mul, exists_and_left, mem_setOf_eq]

Premises used: openSegment_eq_Ioo, exists_and_left, Set.mem_setOf_eq, openSegment, smul_eq_mul
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ioc x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
⟨fun hz => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
refine_1 : ∀ (hz : z ∈ Ioc x y), ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
refine_2 : (∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ioc x y
⊢ z ∈ Ioc x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
refine ⟨fun hz => ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
hz : z ∈ Ioc x y
refine_1 :
  ∀ (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hz : a * x + b * y ∈ Ioc x y),
    ∃ (a_1 : 𝕜) (b_1 : 𝕜), 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y
⊢ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ioc_subset_Icc_self hz)

Premises used: Set.Ioc_subset_Icc_self, LT.lt.le, Convex.mem_Icc, Iff.mp, rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ioc x y
refine_1 :
  ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1) (hz : a * x + 0 * y ∈ Ioc x y),
    ∃ (a_1 : 𝕜) (b : 𝕜), 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y
refine_1₁ :
  ∀ (hb' : 0 < b), ∃ (a_1 : 𝕜) (b_1 : 𝕜), 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y
⊢ ∃ (a_1 : 𝕜) (b_1 : 𝕜), 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y

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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ a = 1

Tactic:
rw [add_zero] at hab

Premises used: add_zero
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
hz : a * x + 0 * y ∈ Ioc x y
hab₁ : a = 1
⊢ a * x + 0 * y ∈ Ioc x y

Tactic:
rw [add_zero] at hab

Premises used: add_zero
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ x ∈ Ioc x y

Tactic:
rw [hab, one_mul, zero_mul, add_zero] at hz

Premises used: MulZeroClass.zero_mul, add_zero, one_mul
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
hz : x ∈ Ioc x y
⊢ ∃ (a_1 : 𝕜) (b : 𝕜), 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

Tactic:
(hz.1.ne rfl).elim

Premises used: False.elim, And.left, rfl, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
hz : x ∈ Ioc x y
⊢ ∃ (a_1 : 𝕜) (b : 𝕜), 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

Tactic:
exact (hz.1.ne rfl).elim

Premises used: False.elim, And.left, rfl, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ioc x y
hb' : 0 < b
⊢ ∃ (a_1 : 𝕜) (b_1 : 𝕜), 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y

Tactic:
⟨a, b, ha, hb', hab, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ioc x y
hb' : 0 < b
⊢ ∃ (a_1 : 𝕜) (b_1 : 𝕜), 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y

Tactic:
exact ⟨a, b, ha, hb', hab, rfl⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
refine_2 : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1), 0 * x + b * y ∈ Ioc x y
refine_2₁ : ∀ (ha' : 0 < a), a * x + b * y ∈ Ioc x y
⊢ a * x + b * y ∈ Ioc x y

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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
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.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
refine_2 : 0 * x + 1 * y ∈ Ioc x y
refine_2₁ : 0 * x + y ∈ Ioc x y
refine_2₂ : 0 + y ∈ Ioc x y
refine_2₃ : y ∈ Ioc x y
refine_2₄ refine_2₅ refine_2₆ refine_2₇ : x < y
⊢ 0 * x + b * y ∈ Ioc x y

Tactic:
rwa [hab, one_mul, zero_mul, zero_add, right_mem_Ioc]

Premises used: MulZeroClass.zero_mul, zero_add, Set.right_mem_Ioc, one_mul
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
ha' : 0 < a
⊢ a * x + b * y ∈ Ioc x y

Tactic:
Ioo_subset_Ioc_self ((Convex.mem_Ioo h).2 ⟨a, b, ha', hb, hab, rfl⟩)

Premises used: Iff.mpr, Convex.mem_Ioo, Set.Ioo_subset_Ioc_self, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
ha' : 0 < a
⊢ a * x + b * y ∈ Ioc x y

Tactic:
exact Ioo_subset_Ioc_self ((Convex.mem_Ioo h).2 ⟨a, b, ha', hb, hab, rfl⟩)

Premises used: Iff.mpr, Convex.mem_Ioo, Set.Ioo_subset_Ioc_self, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ico x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
⟨fun hz => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
refine_1 : ∀ (hz : z ∈ Ico x y), ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
refine_2 : (∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ico x y
⊢ z ∈ Ico x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
refine ⟨fun hz => ?_, ?_⟩