awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
have right₂ : a • y + b • z = a • y + b • z
Tactic: rw [hab, div_one, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z
have hab : 0 < a + b
Tactic: have hab : 0 < a + b := add_pos' ha hb
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z
have mpr : a / (a + b) + b / (a + b) = 1
Tactic: refine ⟨a / (a + b), b / (a + b), by positivity, by positivity, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ a / (a + b) + b / (a + b) = 1
have mpr : (a + b) / (a + b) = 1
Tactic: rw [← add_div, div_self hab.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ a / (a + b) + b / (a + b) = 1
have mpr₁ : Eq.{u_1 + 1} (α := 𝕜) 1 1
Tactic: rw [← add_div, div_self hab.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
have refine : ∀ (h : SameRay 𝕜 (x - y) (z - x)), x ∈ [y -[𝕜] z]
Tactic: refine ⟨sameRay_of_mem_segment, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ x ∈ [y -[𝕜] z]
have 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]
Tactic: rcases h.exists_eq_smul_add with ⟨a, b, ha, hb, hab, hxy, hzx⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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 -[𝕜] z]
have hxy₁ : x - y = a • (z - y)
Tactic: rw [add_comm, sub_add_sub_cancel] at hxy hzx
Cleared hypotheses: hxy, hzx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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)
⊢ x ∈ [y -[𝕜] z]
have hzx₁ : z - x = b • (z - y)
Tactic: rw [add_comm, sub_add_sub_cancel] at hxy hzx
Cleared hypotheses: hxy, hzx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ x ∈ [y -[𝕜] z]
have rw : 0 ∈ [-x + y -[𝕜] -x + z]
Tactic: rw [← mem_segment_translate _ (-x), neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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]
have refine : b • (-x + y) + a • (-x + z) = 0
Tactic: refine ⟨b, a, hb, ha, add_comm a b ▸ hab, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ b • (-x + y) + a • (-x + z) = 0
have rw : b • (y - x) + 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ b • (-x + y) + a • (-x + z) = 0
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ b • (-x + y) + a • (-x + z) = 0
have rw₂ : b • -(a • (z - 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ b • (-x + y) + a • (-x + z) = 0
have rw₃ : b • -(a • (z - y)) + a • (z - x) = 0
Tactic: rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ b • (-x + y) + a • (-x + z) = 0
have rw₄ : b • -(a • (z - y)) + a • b • (z - y) = 0
Tactic: rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ b • (-x + y) + a • (-x + z) = 0
have rw₅ : -(b • a • (z - y)) + a • b • (z - y) = 0
Tactic: rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ b • (-x + y) + a • (-x + z) = 0
have rw₆ : -(a • b • (z - y)) + a • b • (z - y) = 0
Tactic: rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ b • (-x + y) + a • (-x + z) = 0
have rw₇ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)
have 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)
Tactic: rcases hz with ⟨c, rfl⟩
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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 : 𝕜
⊢ 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)
have 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)))
Tactic: simp only [openSegment_eq_image_lineMap, ← mapsTo_iff_image_subset]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ 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)
have 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)
Tactic: rcases lt_trichotomy a c with (hac | rfl | hca)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ 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)
have 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)
Tactic: rcases lt_trichotomy a c with (hac | rfl | hca)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ 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)
have 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)
Tactic: rcases lt_trichotomy a c with (hac | rfl | hca)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ 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)
have 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)
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ 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)
have 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)
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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
⊢ 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)
have hc : 0 < c
Tactic: have hc : 0 < c := h₀.trans hac
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
have 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)
Tactic: refine ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ 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)
have inr : Eq.{u_2 + 1} (α := E) ((lineMap x y : (a : 𝕜) → E) a : E) ((lineMap x y : (a : 𝕜) → E) a : E)
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ 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)
have 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)
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ 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)
have 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)
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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
⊢ 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)
have hc : 0 < 1 - c
Tactic: have hc : 0 < 1 - c := sub_pos.2 (hca.trans h₁)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
    (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)
have 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)
Tactic: simp only [← lineMap_apply_one_sub y]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
have 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)
Tactic: refine
      ⟨(a - c) / (1 - c), ⟨div_pos (sub_pos.2 hca) hc, (div_lt_one hc).2 <| sub_lt_sub_right h₁ _⟩,
        ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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 • x + b • y ∈ Icc x y
have left : x ≤ a • x + b • y
Tactic: constructor