awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
mpr : a / (a + b) + b / (a + b) = 1
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ [y -[𝕜] z]

Tactic:
refine ⟨a / (a + b), b / (a + b), by positivity, by positivity, ?_, rfl⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
mpr : (a + b) / (a + b) = 1
mpr₁ mpr₂ : Eq.{u_1 + 1} (α := 𝕜) 1 1
⊢ a / (a + b) + b / (a + b) = 1

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

Premises used: LT.lt.ne', div_self, add_div
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y z : E
mp : x ∈ openSegment 𝕜 y z → ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
mpr : (∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ openSegment 𝕜 y z
⊢ x ∈ openSegment 𝕜 y z ↔ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
right : (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
⊢ ∃ (a_1 : 𝕜) (b_1 : 𝕜), 0 < a_1 ∧ 0 < b_1 ∧ (a_1 / (a_1 + b_1)) • y + (b_1 / (a_1 + b_1)) • z = a • y + b • z

Tactic:
use a, b, ha, hb
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
right : (a / 1) • y + (b / 1) • z = a • y + b • z
right₁ : a • y + (b / 1) • z = a • y + b • z
right₂ right₃ : a • y + b • z = a • y + b • z
⊢ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z

Tactic:
rw [hab, div_one, div_one]

Premises used: div_one
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ 0 < a + b

Tactic:
have hab : 0 < a + b := add_pos' ha hb
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ 0 < a / (a + b)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ 0 < b / (a + b)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
mpr : a / (a + b) + b / (a + b) = 1
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z

Tactic:
refine ⟨a / (a + b), b / (a + b), by positivity, by positivity, ?_, rfl⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
mpr : (a + b) / (a + b) = 1
mpr₁ mpr₂ : Eq.{u_1 + 1} (α := 𝕜) 1 1
⊢ a / (a + b) + b / (a + b) = 1

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

Premises used: LT.lt.ne', div_self, add_div
-- Module: Mathlib.Analysis.Convex.Segment
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 y z : E
⊢ x ∈ [y -[𝕜] z] ↔ SameRay 𝕜 (x - y) (z - x)

Tactic:
⟨sameRay_of_mem_segment, fun h => ?_⟩

Premises used: Iff.intro, sameRay_of_mem_segment
-- Module: Mathlib.Analysis.Convex.Segment
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 y z : E
refine : ∀ (h : SameRay 𝕜 (x - y) (z - x)), x ∈ [y -[𝕜] z]
⊢ x ∈ [y -[𝕜] z] ↔ SameRay 𝕜 (x - y) (z - x)

Tactic:
refine ⟨sameRay_of_mem_segment, fun h => ?_⟩
-- Module: Mathlib.Analysis.Convex.Segment
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 y z : E
h : SameRay 𝕜 (x - y) (z - x)
rcases :
  ∀ (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hxy : x - y = a • (x - y + (z - x)))
    (hzx : z - x = b • (x - y + (z - x))), x ∈ [y -[𝕜] z]
⊢ x ∈ [y -[𝕜] z]

Tactic:
rcases h.exists_eq_smul_add with ⟨a, b, ha, hb, hab, hxy, hzx⟩

Premises used: SameRay.exists_eq_smul_add
-- Module: Mathlib.Analysis.Convex.Segment
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 y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (x - y + (z - x))
hzx : z - x = b • (x - y + (z - x))
⊢ x - y = a • (z - y)

Tactic:
rw [add_comm, sub_add_sub_cancel] at hxy hzx

Premises used: sub_add_sub_cancel, add_comm
-- Module: Mathlib.Analysis.Convex.Segment
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 y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (x - y + (z - x))
hzx : z - x = b • (x - y + (z - x))
hxy₁ : x - y = a • (z - y)
⊢ z - x = b • (z - y)

Tactic:
rw [add_comm, sub_add_sub_cancel] at hxy hzx

Premises used: sub_add_sub_cancel, add_comm
-- Module: Mathlib.Analysis.Convex.Segment
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 y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
rw : 0 ∈ [-x + y -[𝕜] -x + z]
⊢ x ∈ [y -[𝕜] z]

Tactic:
rw [← mem_segment_translate _ (-x), neg_add_cancel]

Premises used: neg_add_cancel, mem_segment_translate, Neg.neg
-- Module: Mathlib.Analysis.Convex.Segment
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 y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
⊢ 0 ∈ [-x + y -[𝕜] -x + z]

Tactic:
⟨b, a, hb, ha, add_comm a b ▸ hab, ?_⟩

Premises used: Set.Mem, setOf, Eq.rec, segment, add_comm, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Segment
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 y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
refine : b • (-x + y) + a • (-x + z) = 0
⊢ 0 ∈ [-x + y -[𝕜] -x + z]

Tactic:
refine ⟨b, a, hb, ha, add_comm a b ▸ hab, ?_⟩
-- Module: Mathlib.Analysis.Convex.Segment
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 y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
rw : b • (y - x) + a • (-x + z) = 0
rw₁ : b • -(x - y) + a • (-x + z) = 0
rw₂ : b • -(a • (z - y)) + a • (-x + z) = 0
rw₃ : b • -(a • (z - y)) + a • (z - x) = 0
rw₄ : b • -(a • (z - y)) + a • b • (z - y) = 0
rw₅ : -(b • a • (z - y)) + a • b • (z - y) = 0
rw₆ : -(a • b • (z - y)) + a • b • (z - y) = 0
rw₇ rw₈ : Eq.{u_2 + 1} (α := E) 0 0
⊢ b • (-x + y) + a • (-x + z) = 0

Tactic:
rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_cancel]

Premises used: neg_sub, sub_eq_neg_add, smul_neg, neg_add_cancel, SMulCommClass.smul_comm
-- Module: Mathlib.Analysis.Convex.Segment
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 y z : E
hz : Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := 𝕜) (⇑(lineMap x y) : (a : 𝕜) → E)) z
rcases :
  ∀ (c : 𝕜),
    openSegment 𝕜 x y ⊆
      insert (α := E) ((lineMap x y : (a : 𝕜) → E) c : E)
        (openSegment 𝕜 x ((lineMap x y : (a : 𝕜) → E) c) ∪ openSegment 𝕜 ((lineMap x y : (a : 𝕜) → E) c) y)
⊢ openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)

Tactic:
rcases hz with ⟨c, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c : 𝕜
simp :
  MapsTo.{u_1, u_2} (α := 𝕜) (β := E) (⇑(lineMap x y) : (a : 𝕜) → E) (Ioo 0 1)
    (insert (α := E) ((lineMap x y : (a : 𝕜) → E) c : E)
      (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1) ∪
        image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1)))
⊢ openSegment 𝕜 x y ⊆
    insert (α := E) ((lineMap x y : (a : 𝕜) → E) c : E)
      (openSegment 𝕜 x ((lineMap x y : (a : 𝕜) → E) c) ∪ openSegment 𝕜 ((lineMap x y : (a : 𝕜) → E) c) y)

Tactic:
simp only [openSegment_eq_image_lineMap, ← mapsTo_iff_image_subset]

Premises used: Set.mapsTo_iff_image_subset, openSegment_eq_image_lineMap
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
inl :
  ∀ (hac : a < c),
    Membership.mem (α := E) (γ := Set E)
      (insert (α := E) ((lineMap x y : (a : 𝕜) → E) c : E)
        (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1) ∪
          image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1)))
      ((lineMap x y : (a : 𝕜) → E) a : E)
inr :
  Membership.mem (α := E) (γ := Set E)
    (insert (α := E) ((lineMap x y : (a : 𝕜) → E) a : E)
      (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) a)) : (a : 𝕜) → E) (Ioo 0 1) ∪
        image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) a) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1)))
    ((lineMap x y : (a : 𝕜) → E) a : E)
inr₁ :
  ∀ (hca : c < a),
    Membership.mem (α := E) (γ := Set E)
      (insert (α := E) ((lineMap x y : (a : 𝕜) → E) c : E)
        (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1) ∪
          image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1)))
      ((lineMap x y : (a : 𝕜) → E) a : E)
⊢ Membership.mem (α := E) (γ := Set E)
    (insert (α := E) ((lineMap x y : (a : 𝕜) → E) c : E)
      (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1) ∪
        image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1)))
    ((lineMap x y : (a : 𝕜) → E) a : E)

Tactic:
rcases lt_trichotomy a c with (hac | rfl | hca)

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
inl :
  Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1) ∪
      image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1))
    ((lineMap x y : (a : 𝕜) → E) a : E)
⊢ Membership.mem (α := E) (γ := Set E)
    (insert (α := E) ((lineMap x y : (a : 𝕜) → E) c : E)
      (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1) ∪
        image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1)))
    ((lineMap x y : (a : 𝕜) → E) a : E)

Tactic:
right
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
inl :
  Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1))
    ((lineMap x y : (a : 𝕜) → E) a : E)
⊢ Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1) ∪
      image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1))
    ((lineMap x y : (a : 𝕜) → E) a : E)

Tactic:
left
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ 0 < c

Tactic:
have hc : 0 < c := h₀.trans hac
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
hc : 0 < c
⊢ Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1))
    ((lineMap x y : (a : 𝕜) → E) a : E)

Tactic:
⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, ?_⟩

Premises used: Iff.mpr, Set.Mem, setOf, HDiv.hDiv, div_lt_one, And.intro, Exists.intro, Set.image, div_pos
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
hc : 0 < c
inl :
  Eq.{u_2 + 1} (α := E) ((lineMap x ((lineMap x y : (a : 𝕜) → E) c) : (a : 𝕜) → E) (a / c) : E)
    ((lineMap x y : (a : 𝕜) → E) a : E)
⊢ Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1))
    ((lineMap x y : (a : 𝕜) → E) a : E)

Tactic:
refine ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
hc : 0 < c
⊢ Eq.{u_2 + 1} (α := E) ((lineMap x ((lineMap x y : (a : 𝕜) → E) c) : (a : 𝕜) → E) (a / c) : E)
    ((lineMap x y : (a : 𝕜) → E) a : E)

Tactic:
simp only [← homothety_eq_lineMap, ← homothety_mul_apply, div_mul_cancel₀ _ hc.ne']

Premises used: div_mul_cancel₀, LT.lt.ne', AffineMap.homothety_eq_lineMap, AffineMap.homothety_mul_apply
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
inr : Eq.{u_2 + 1} (α := E) ((lineMap x y : (a : 𝕜) → E) a : E) ((lineMap x y : (a : 𝕜) → E) a : E)
⊢ Membership.mem (α := E) (γ := Set E)
    (insert (α := E) ((lineMap x y : (a : 𝕜) → E) a : E)
      (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) a)) : (a : 𝕜) → E) (Ioo 0 1) ∪
        image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) a) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1)))
    ((lineMap x y : (a : 𝕜) → E) a : E)

Tactic:
left
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ Eq.{u_2 + 1} (α := E) ((lineMap x y : (a : 𝕜) → E) a : E) ((lineMap x y : (a : 𝕜) → E) a : E)

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
inr :
  Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1) ∪
      image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1))
    ((lineMap x y : (a : 𝕜) → E) a : E)
⊢ Membership.mem (α := E) (γ := Set E)
    (insert (α := E) ((lineMap x y : (a : 𝕜) → E) c : E)
      (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1) ∪
        image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1)))
    ((lineMap x y : (a : 𝕜) → E) a : E)

Tactic:
right
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
inr :
  Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1))
    ((lineMap x y : (a : 𝕜) → E) a : E)
⊢ Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap x ((lineMap x y : (a : 𝕜) → E) c)) : (a : 𝕜) → E) (Ioo 0 1) ∪
      image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1))
    ((lineMap x y : (a : 𝕜) → E) a : E)

Tactic:
right
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ 0 < 1 - c

Tactic:
have hc : 0 < 1 - c := sub_pos.2 (hca.trans h₁)
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
inr :
  Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    ((fun (a : 𝕜) ↦ (lineMap y ((lineMap y x : (a : 𝕜) → E) (1 - c)) : (a : 𝕜) → E) (1 - a)) '' Ioo 0 1)
    ((lineMap y x : (a : 𝕜) → E) (1 - a) : E)
⊢ Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    (image.{u_1, u_2} (α := 𝕜) (⇑(lineMap ((lineMap x y : (a : 𝕜) → E) c) y : 𝕜 →ᵃ[𝕜] E) : (a : 𝕜) → E) (Ioo 0 1))
    ((lineMap x y : (a : 𝕜) → E) a : E)

Tactic:
simp only [← lineMap_apply_one_sub y]

Premises used: AffineMap.lineMap_apply_one_sub
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    ((fun (a : 𝕜) ↦ (lineMap y ((lineMap y x : (a : 𝕜) → E) (1 - c)) : (a : 𝕜) → E) (1 - a)) '' Ioo 0 1)
    ((lineMap y x : (a : 𝕜) → E) (1 - a) : E)

Tactic:
⟨(a - c) / (1 - c), ⟨div_pos (sub_pos.2 hca) hc, (div_lt_one hc).2 <| sub_lt_sub_right h₁ _⟩,
        ?_⟩

Premises used: Iff.mpr, sub_pos, Set.Mem, setOf, HSub.hSub, HDiv.hDiv, div_lt_one, And.intro, Exists.intro, Set.image, div_pos, OfNat.ofNat, sub_lt_sub_right
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
inr :
  Eq.{u_2 + 1} (α := E)
    ((fun (a : 𝕜) ↦ ((lineMap y ((lineMap y x : (a : 𝕜) → E) (1 - c)) : (a : 𝕜) → E) (1 - a) : E)) ((a - c) / (1 - c)) :
      E)
    ((lineMap y x : (a : 𝕜) → E) (1 - a) : E)
⊢ Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    ((fun (a : 𝕜) ↦ (lineMap y ((lineMap y x : (a : 𝕜) → E) (1 - c)) : (a : 𝕜) → E) (1 - a)) '' Ioo 0 1)
    ((lineMap y x : (a : 𝕜) → E) (1 - a) : E)

Tactic:
refine
      ⟨(a - c) / (1 - c), ⟨div_pos (sub_pos.2 hca) hc, (div_lt_one hc).2 <| sub_lt_sub_right h₁ _⟩,
        ?_⟩
-- Module: Mathlib.Analysis.Convex.Segment
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 y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ Eq.{u_2 + 1} (α := E)
    ((fun (a : 𝕜) ↦ ((lineMap y ((lineMap y x : (a : 𝕜) → E) (1 - c)) : (a : 𝕜) → E) (1 - a) : E)) ((a - c) / (1 - c)) :
      E)
    ((lineMap y x : (a : 𝕜) → E) (1 - a) : E)

Tactic:
simp only [← homothety_eq_lineMap, ← homothety_mul_apply, sub_mul, one_mul,
      div_mul_cancel₀ _ hc.ne', sub_sub_sub_cancel_right]

Premises used: sub_sub_sub_cancel_right, div_mul_cancel₀, LT.lt.ne', sub_mul, one_mul, AffineMap.homothety_eq_lineMap, AffineMap.homothety_mul_apply
-- 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
left : x ≤ a • x + b • y
right : a • x + b • y ≤ y
⊢ a • x + b • y ∈ Icc 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 : 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
⊢ 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 : 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
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 : 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
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 : 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
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 : 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 • y + b • y = y

Tactic:
Convex.combo_self hab _

Premises used: Convex.combo_self