awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∈ Ico x y
refine_1 :
  ∀ (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hz : a * x + b * y ∈ Ico 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 (Ico_subset_Icc_self hz)

Premises used: Set.Ico_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 ∈ Ico x y
refine_1 :
  ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1) (hz : 0 * x + b * y ∈ Ico x y),
    ∃ (a : 𝕜) (b_1 : 𝕜), 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y
refine_1₁ :
  ∀ (ha' : 0 < a), ∃ (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 | 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
hz : 0 * x + b * y ∈ Ico x y
⊢ 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 : 0 + b = 1
hz : 0 * x + b * y ∈ Ico x y
hab₁ : b = 1
⊢ 0 * x + b * y ∈ Ico x y

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
hz : 0 * x + b * y ∈ Ico x y
⊢ y ∈ Ico x y

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

Premises used: MulZeroClass.zero_mul, zero_add, one_mul
-- 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
hz : y ∈ Ico x y
⊢ ∃ (a : 𝕜) (b_1 : 𝕜), 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y

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

Premises used: False.elim, And.right, 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
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
hz : y ∈ Ico x y
⊢ ∃ (a : 𝕜) (b_1 : 𝕜), 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y

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

Premises used: False.elim, And.right, 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 ∈ Ico x y
ha' : 0 < a
⊢ ∃ (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 ∈ Ico x y
ha' : 0 < a
⊢ ∃ (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 : ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1), a * x + 0 * y ∈ Ico x y
refine_2₁ : ∀ (hb' : 0 < b), a * x + b * y ∈ Ico x y
⊢ a * x + b * y ∈ Ico x 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
⊢ 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 = 1
refine_2 : 1 * x + 0 * y ∈ Ico x y
refine_2₁ : x + 0 * y ∈ Ico x y
refine_2₂ : x + 0 ∈ Ico x y
refine_2₃ : x ∈ Ico x y
refine_2₄ refine_2₅ refine_2₆ refine_2₇ : x < y
⊢ a * x + 0 * y ∈ Ico x y

Tactic:
rwa [hab, one_mul, zero_mul, add_zero, left_mem_Ico]

Premises used: Set.left_mem_Ico, 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 b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
⊢ a * x + b * y ∈ Ico x y

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

Premises used: Iff.mpr, Convex.mem_Ioo, Set.Ioo_subset_Ico_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
hb' : 0 < b
⊢ a * x + b * y ∈ Ico x y

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

Premises used: Iff.mpr, Convex.mem_Ioo, Set.Ioo_subset_Ico_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 a : { t : 𝕜 // 0 ≤ t }
this : ∀ (hxa : x ≤ a) (hay : a ≤ y), a ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]
⊢ a ∈ Icc x y → a ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]

Tactic:
⟨hxa, hay⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
hxa : x ≤ a
hay : a ≤ y
⊢ (↑x : 𝕜) ≤ (↑a : 𝕜)

Tactic:
rw [← Subtype.coe_le_coe] at hxa hay

Premises used: Subtype.coe_le_coe
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
hxa : x ≤ a
hay : a ≤ y
hxa₁ : (↑x : 𝕜) ≤ (↑a : 𝕜)
⊢ (↑a : 𝕜) ≤ (↑y : 𝕜)

Tactic:
rw [← Subtype.coe_le_coe] at hxa hay

Premises used: Subtype.coe_le_coe
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
hxa : (↑x : 𝕜) ≤ (↑a : 𝕜)
hay : (↑a : 𝕜) ≤ (↑y : 𝕜)
rcases :
  ∀ (t₁ t₂ : 𝕜) (t₁_nonneg : 0 ≤ t₁) (t₂_nonneg : 0 ≤ t₂) (t_add : t₁ + t₂ = 1)
    (hta : t₁ • (↑x : 𝕜) + t₂ • (↑y : 𝕜) = (↑a : 𝕜)), a ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]
⊢ a ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]

Tactic:
rcases Icc_subset_segment ⟨hxa, hay⟩ with ⟨t₁, t₂, t₁_nonneg, t₂_nonneg, t_add, hta⟩

Premises used: And.intro, Icc_subset_segment
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
hxa : (↑x : 𝕜) ≤ (↑a : 𝕜)
hay : (↑a : 𝕜) ≤ (↑y : 𝕜)
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • (↑x : 𝕜) + t₂ • (↑y : 𝕜) = (↑a : 𝕜)
⊢ a ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]

Tactic:
⟨⟨t₁, t₁_nonneg⟩, ⟨t₂, t₂_nonneg⟩, zero_le, zero_le, ?_, ?_⟩

Premises used: zero_le, Set.Mem, setOf, segment, Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
hxa : (↑x : 𝕜) ≤ (↑a : 𝕜)
hay : (↑a : 𝕜) ≤ (↑y : 𝕜)
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • (↑x : 𝕜) + t₂ • (↑y : 𝕜) = (↑a : 𝕜)
refine_1 : Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₁ t₁_nonneg + Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₂ t₂_nonneg = 1
refine_2 :
  Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₁ t₁_nonneg • x + Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₂ t₂_nonneg • y = a
⊢ a ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]

Tactic:
refine ⟨⟨t₁, t₁_nonneg⟩, ⟨t₂, t₂_nonneg⟩, zero_le, zero_le, ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
hxa : (↑x : 𝕜) ≤ (↑a : 𝕜)
hay : (↑a : 𝕜) ≤ (↑y : 𝕜)
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • (↑x : 𝕜) + t₂ • (↑y : 𝕜) = (↑a : 𝕜)
refine_1 :
  (↑(Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₁ t₁_nonneg + Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₂ t₂_nonneg) : 𝕜) =
    (↑1 : 𝕜)
⊢ Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₁ t₁_nonneg + Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₂ t₂_nonneg = 1

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
hxa : (↑x : 𝕜) ≤ (↑a : 𝕜)
hay : (↑a : 𝕜) ≤ (↑y : 𝕜)
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • (↑x : 𝕜) + t₂ • (↑y : 𝕜) = (↑a : 𝕜)
refine_2 :
  (↑(Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₁ t₁_nonneg • x + Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₂ t₂_nonneg • y) :
      𝕜) =
    (↑a : 𝕜)
⊢ Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₁ t₁_nonneg • x + Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₂ t₂_nonneg • y = a

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
hxa : (↑x : 𝕜) ≤ (↑a : 𝕜)
hay : (↑a : 𝕜) ≤ (↑y : 𝕜)
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • (↑x : 𝕜) + t₂ • (↑y : 𝕜) = (↑a : 𝕜)
⊢ (↑(Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₁ t₁_nonneg + Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₂ t₂_nonneg) : 𝕜) =
    (↑1 : 𝕜)

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
hxa : (↑x : 𝕜) ≤ (↑a : 𝕜)
hay : (↑a : 𝕜) ≤ (↑y : 𝕜)
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • (↑x : 𝕜) + t₂ • (↑y : 𝕜) = (↑a : 𝕜)
⊢ (↑(Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₁ t₁_nonneg • x + Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₂ t₂_nonneg • y) :
      𝕜) =
    (↑a : 𝕜)

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : { t : 𝕜 // 0 ≤ t }
hxy : x ≤ y
⊢ [x -[{ t : 𝕜 // 0 ≤ t }] y] = Icc x y

Tactic:
subset_antisymm (segment_subset_Icc hxy) Nonneg.Icc_subset_segment

Premises used: subset_antisymm, segment_subset_Icc, Nonneg.Icc_subset_segment
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : { t : 𝕜 // 0 ≤ t }
hxy : x ≤ y
⊢ [x -[{ t : 𝕜 // 0 ≤ t }] y] = Icc x y

Tactic:
refine subset_antisymm (segment_subset_Icc hxy) Nonneg.Icc_subset_segment

Premises used: subset_antisymm, segment_subset_Icc, Nonneg.Icc_subset_segment
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : { t : 𝕜 // 0 ≤ t }
inl : ∀ (h : x ≤ y), [x -[{ t : 𝕜 // 0 ≤ t }] y] = uIcc x y
inr : ∀ (h : y ≤ x), [x -[{ t : 𝕜 // 0 ≤ t }] y] = uIcc x y
⊢ [x -[{ t : 𝕜 // 0 ≤ t }] 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
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : { t : 𝕜 // 0 ≤ t }
h : x ≤ y
⊢ [x -[{ t : 𝕜 // 0 ≤ t }] y] = uIcc x y

Tactic:
simp [h, Nonneg.segment_eq_Icc]

Premises used: Nonneg.segment_eq_Icc
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : { t : 𝕜 // 0 ≤ t }
h : y ≤ x
⊢ [x -[{ t : 𝕜 // 0 ≤ t }] y] = uIcc x y

Tactic:
simp [h, segment_symm _ x y, Nonneg.segment_eq_Icc]

Premises used: segment_symm, Nonneg.segment_eq_Icc
-- Module: Mathlib.Analysis.Convex.Segment
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
x y z : E × F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ [x.1 -[𝕜] y.1] ×ˢ [x.2 -[𝕜] y.2]

Tactic:
⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩

Premises used: Set.Mem, setOf, Set.prod, Prod.fst, congr_arg, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Analysis.Convex.Segment
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
x y z : E × F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ [x.1 -[𝕜] y.1] ×ˢ [x.2 -[𝕜] y.2]

Tactic:
exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩
-- Module: Mathlib.Analysis.Convex.Segment
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
x y z : E × F
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2

Tactic:
⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩

Premises used: Set.Mem, setOf, Set.prod, Prod.fst, congr_arg, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Analysis.Convex.Segment
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
x y z : E × F
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2

Tactic:
exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩
-- Module: Mathlib.Analysis.Convex.Segment
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
x₁ x₂ : E
y : F
rw :
  Eq (α := Set (E × F))
    ((fun (x : 𝕜 × 𝕜) ↦ (x.1 • x₁ + x.2 • x₂, y)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
⊢ (fun (x : E) ↦ (x, y)) '' [x₁ -[𝕜] x₂] = [(x₁, y) -[𝕜] (x₂, y)]

Tactic:
rw [segment_eq_image₂, segment_eq_image₂, image_image]

Premises used: Set.image_image, segment_eq_image₂
-- Module: Mathlib.Analysis.Convex.Segment
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
x₁ x₂ : E
y : F
⊢ Eq (α := Set (E × F))
    ((fun (x : 𝕜 × 𝕜) ↦ (x.1 • x₁ + x.2 • x₂, y)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})

Tactic:
EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
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
x₁ x₂ : E
y : F
refine :
  ∀ (a : 𝕜 × 𝕜) (ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} a),
    (a.1 • x₁ + a.2 • x₂, y) = a.1 • (x₁, y) + a.2 • (x₂, y)
⊢ Eq (α := Set (E × F))
    ((fun (x : 𝕜 × 𝕜) ↦ (x.1 • x₁ + x.2 • x₂, y)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
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
x₁ x₂ : E
y : F
a : 𝕜 × 𝕜
ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} a
⊢ (a.1 • x₁ + a.2 • x₂, y) = a.1 • (x₁, y) + a.2 • (x₂, y)

Tactic:
simp [Convex.combo_self ha.2.2]

Premises used: Convex.combo_self, And.right
-- Module: Mathlib.Analysis.Convex.Segment
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
x : E
y₁ y₂ : F
rw :
  Eq (α := Set (E × F))
    ((fun (x_1 : 𝕜 × 𝕜) ↦ (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
⊢ (fun (y : F) ↦ (x, y)) '' [y₁ -[𝕜] y₂] = [(x, y₁) -[𝕜] (x, y₂)]

Tactic:
rw [segment_eq_image₂, segment_eq_image₂, image_image]

Premises used: Set.image_image, segment_eq_image₂
-- Module: Mathlib.Analysis.Convex.Segment
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
x : E
y₁ y₂ : F
⊢ Eq (α := Set (E × F))
    ((fun (x_1 : 𝕜 × 𝕜) ↦ (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})

Tactic:
EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
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
x : E
y₁ y₂ : F
refine :
  ∀ (a : 𝕜 × 𝕜) (ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} a),
    (x, a.1 • y₁ + a.2 • y₂) = a.1 • (x, y₁) + a.2 • (x, y₂)
⊢ Eq (α := Set (E × F))
    ((fun (x_1 : 𝕜 × 𝕜) ↦ (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
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
x : E
y₁ y₂ : F
a : 𝕜 × 𝕜
ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} a
⊢ (x, a.1 • y₁ + a.2 • y₂) = a.1 • (x, y₁) + a.2 • (x, y₂)

Tactic:
simp [Convex.combo_self ha.2.2]

Premises used: Convex.combo_self, And.right
-- Module: Mathlib.Analysis.Convex.Segment
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
x₁ x₂ : E
y : F
rw :
  Eq (α := Set (E × F))
    ((fun (x : 𝕜 × 𝕜) ↦ (x.1 • x₁ + x.2 • x₂, y)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
⊢ (fun (x : E) ↦ (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)

Tactic:
rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]

Premises used: Set.image_image, openSegment_eq_image₂
-- Module: Mathlib.Analysis.Convex.Segment
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
x₁ x₂ : E
y : F
⊢ Eq (α := Set (E × F))
    ((fun (x : 𝕜 × 𝕜) ↦ (x.1 • x₁ + x.2 • x₂, y)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})

Tactic:
EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
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
x₁ x₂ : E
y : F
refine :
  ∀ (a : 𝕜 × 𝕜) (ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} a),
    (a.1 • x₁ + a.2 • x₂, y) = a.1 • (x₁, y) + a.2 • (x₂, y)
⊢ Eq (α := Set (E × F))
    ((fun (x : 𝕜 × 𝕜) ↦ (x.1 • x₁ + x.2 • x₂, y)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
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
x₁ x₂ : E
y : F
a : 𝕜 × 𝕜
ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} a
⊢ (a.1 • x₁ + a.2 • x₂, y) = a.1 • (x₁, y) + a.2 • (x₂, y)

Tactic:
simp [Convex.combo_self ha.2.2]

Premises used: Convex.combo_self, And.right
-- Module: Mathlib.Analysis.Convex.Segment
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
x : E
y₁ y₂ : F
rw :
  Eq (α := Set (E × F))
    ((fun (x_1 : 𝕜 × 𝕜) ↦ (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
⊢ (fun (y : F) ↦ (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)

Tactic:
rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]

Premises used: Set.image_image, openSegment_eq_image₂
-- Module: Mathlib.Analysis.Convex.Segment
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
x : E
y₁ y₂ : F
⊢ Eq (α := Set (E × F))
    ((fun (x_1 : 𝕜 × 𝕜) ↦ (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})

Tactic:
EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
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
x : E
y₁ y₂ : F
refine :
  ∀ (a : 𝕜 × 𝕜) (ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} a),
    (x, a.1 • y₁ + a.2 • y₂) = a.1 • (x, y₁) + a.2 • (x, y₂)
⊢ Eq (α := Set (E × F))
    ((fun (x_1 : 𝕜 × 𝕜) ↦ (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
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
x : E
y₁ y₂ : F
a : 𝕜 × 𝕜
ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} a
⊢ (x, a.1 • y₁ + a.2 • y₂) = a.1 • (x, y₁) + a.2 • (x, y₂)

Tactic:
simp [Convex.combo_self ha.2.2]

Premises used: Convex.combo_self, And.right