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 : 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
⊢ a • x + b • y ∈ Icc x y
have right : a • x + b • y ≤ y
Tactic: constructor
-- 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
⊢ x ≤ a • x + b • y
have x₁ : a • x + b • x ≤ a • x + b • y
Tactic: calc
      x = a • x + b • x := (Convex.combo_self hab _).symm
      _ ≤ a • x + b • y := by gcongr
-- 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 ≤ y
have a₁ : a • x + b • y ≤ a • y + b • y
Tactic: calc
      a • x + b • y ≤ a • y + b • y := by gcongr
      _ = y := Convex.combo_self hab _
-- 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 : 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 • x + b • y ∈ Ioo x y
have left : x < a • x + b • y
Tactic: constructor
-- 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 : 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
⊢ a • x + b • y ∈ Ioo x y
have right : a • x + b • y < y
Tactic: constructor
-- 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 : 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 • y
have x₁ : a • x + b • x < a • x + b • y
Tactic: calc
      x = a • x + b • x := (Convex.combo_self hab _).symm
      _ < a • x + b • y := by gcongr
-- 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 : 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 • x + b • y < y
have a₁ : a • x + b • y < a • y + b • y
Tactic: calc
      a • x + b • y < a • y + b • y := by gcongr
      _ = y := Convex.combo_self hab _
-- 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 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x y : E
⊢ [x -[𝕜] y] ⊆ uIcc x y
have inl : ∀ (h : x ≤ y), [x -[𝕜] y] ⊆ uIcc x y
Tactic: rcases le_total x y with h | 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 : 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
⊢ [x -[𝕜] y] ⊆ uIcc x y
have inr : ∀ (h : y ≤ x), [x -[𝕜] y] ⊆ uIcc x y
Tactic: rcases le_total x y with h | 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 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x y : E
h : x ≤ y
⊢ [x -[𝕜] y] ⊆ uIcc x y
have inl : [x -[𝕜] y] ⊆ Icc x y
Tactic: rw [uIcc_of_le 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 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x y : E
h : y ≤ x
⊢ [x -[𝕜] y] ⊆ uIcc x y
have inr : [y -[𝕜] x] ⊆ Icc y x
Tactic: rw [uIcc_of_ge h, segment_symm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
⊢ z ∈ [x -[𝕜] y]
have inl : ∀ (hyz : z ≤ x), z ∈ [x -[𝕜] x]
Tactic: obtain rfl | h := (hxz.trans hyz).eq_or_lt
Cleared hypotheses: y, hyz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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]
⊢ z ∈ [x -[𝕜] y]
have inr : ∀ (h : x < y), z ∈ [x -[𝕜] y]
Tactic: obtain rfl | h := (hxz.trans hyz).eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ [x -[𝕜] x]
have inl : Membership.mem (γ := Set 𝕜) {x} z
Tactic: rw [segment_same]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
⊢ z ∈ [x -[𝕜] y]
have hxz₁ : 0 ≤ z - x
Tactic: rw [← sub_nonneg] at hxz hyz
Cleared hypotheses: hxz, hyz, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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
⊢ z ∈ [x -[𝕜] y]
have hyz₁ : 0 ≤ y - z
Tactic: rw [← sub_nonneg] at hxz hyz
Cleared hypotheses: hxz, hyz, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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
⊢ z ∈ [x -[𝕜] y]
have h₁ : 0 < y - x
Tactic: rw [← sub_pos] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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]
have inr : (y - z) / (y - x) + (z - x) / (y - x) = 1
Tactic: refine ⟨(y - z) / (y - x), (z - x) / (y - x), div_nonneg hyz h.le, div_nonneg hxz h.le, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ z ∈ [x -[𝕜] y]
have inr₁ : ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
Tactic: refine ⟨(y - z) / (y - x), (z - x) / (y - x), div_nonneg hyz h.le, div_nonneg hxz h.le, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ (y - z) / (y - x) + (z - x) / (y - x) = 1
have inr : (y - z + (z - x)) / (y - x) = 1
Tactic: rw [← add_div, sub_add_sub_cancel, div_self h.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ (y - z) / (y - x) + (z - x) / (y - x) = 1
have inr₁ : (y - x) / (y - x) = 1
Tactic: rw [← add_div, sub_add_sub_cancel, div_self h.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ (y - z) / (y - x) + (z - x) / (y - x) = 1
have inr₂ : Eq.{u_1 + 1} (α := 𝕜) 1 1
Tactic: rw [← add_div, sub_add_sub_cancel, div_self h.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr : (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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr₁ : (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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr₂ : (y - z) * x / (y - 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr₃ : (y - z) * x / (y - x) + (z - x) * y / (y - x) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr₄ : ((y - z) * x + (z - x) * y) / (y - x) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr₅ : (y - z) * x + (z - x) * y = z * (y - x)
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr₆ : (z - x) * y + (y - z) * x = z * (y - x)
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr₇ : z * y - x * y + (y - z) * x = z * (y - x)
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr₈ : z * y - x * y + (y * x - z * x) = z * (y - x)
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr₉ : z * y - y * x + (y * x - z * x) = z * (y - x)
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr₁₀ : z * y - z * x = z * (y - x)
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
have inr₁₁ : z * y - z * x = z * y - z * x
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)
have inl : ∀ (h : x ≤ y), [x -[𝕜] y] = Icc (min x y) (max x y)
Tactic: rcases le_total x y with h | h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)
have inr : ∀ (h : y ≤ x), [x -[𝕜] y] = Icc (min x y) (max x y)
Tactic: rcases le_total x y with h | h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x ≤ y
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)
have inl : Icc x y = Icc (min x y) (max x y)
Tactic: rw [segment_eq_Icc h, max_eq_right h, min_eq_left h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)
have inl₁ : Icc x y = Icc (min x y) y
Tactic: rw [segment_eq_Icc h, max_eq_right h, min_eq_left h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)
have inl₂ : Icc x y = Icc x y
Tactic: rw [segment_eq_Icc h, max_eq_right h, min_eq_left h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : y ≤ x
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)
have inr : [y -[𝕜] x] = Icc (min x y) (max x y)
Tactic: rw [segment_symm, segment_eq_Icc h, max_eq_left h, min_eq_right h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)
have inr₁ : Icc y x = Icc (min x y) (max x y)
Tactic: rw [segment_symm, segment_eq_Icc h, max_eq_left h, min_eq_right h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)
have inr₂ : Icc y x = Icc (min x y) x
Tactic: rw [segment_symm, segment_eq_Icc h, max_eq_left h, min_eq_right h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)
have inr₃ : Icc y x = Icc y x
Tactic: rw [segment_symm, segment_eq_Icc h, max_eq_left h, min_eq_right h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
have inl : ∀ (h : x < y), openSegment 𝕜 x y = Ioo (min x y) (max x y)
Tactic: rcases hxy.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
have inr : ∀ (h : y < x), openSegment 𝕜 x y = Ioo (min x y) (max x y)
Tactic: rcases hxy.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : x < y
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
have inl : Ioo 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
have inl₁ : Ioo x y = Ioo (min x y) y
Tactic: rw [openSegment_eq_Ioo h, max_eq_right h.le, min_eq_left h.le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
have inl₂ : Ioo x y = Ioo x y
Tactic: rw [openSegment_eq_Ioo h, max_eq_right h.le, min_eq_left h.le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : y < x
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
have inr : openSegment 𝕜 y x = 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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)
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
have inr₁ : Ioo y x = 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]