awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
inr₁ : Ioo 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) x
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)
inr₁ : Ioo y x = Ioo (min x y) (max x y)
inr₂ : Ioo y x = Ioo (min x y) x
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
have inr₃ : Ioo y x = Ioo y x
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 z : 𝕜
h : x < y
⊢ z ∈ Ioc x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
have refine_1 : ∀ (hz : z ∈ Ioc x y), ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
Tactic: refine ⟨fun hz => ?_, ?_⟩
-- 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 : 𝕜
h : x < y
refine_1 : ∀ (hz : z ∈ Ioc x y), ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
⊢ z ∈ Ioc x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
have refine_2 : (∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ioc x y
Tactic: refine ⟨fun hz => ?_, ?_⟩
-- 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 : 𝕜
h : x < y
hz : z ∈ Ioc x y
⊢ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
have refine_1 : ∀ (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hz : a * x + b * y ∈ Ioc x y),
  ∃ (a_1 : 𝕜) (b_1 : 𝕜), 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y
Tactic: obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ioc_subset_Icc_self hz)
Cleared hypotheses: z, hz
-- 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
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ioc x y
⊢ ∃ (a_1 : 𝕜) (b_1 : 𝕜), 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y
have refine_1 : ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1) (hz : a * x + 0 * y ∈ Ioc x y),
  ∃ (a_1 : 𝕜) (b : 𝕜), 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y
Tactic: obtain rfl | hb' := hb.eq_or_lt
Cleared hypotheses: b, hb, hab, hz
-- 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
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ioc x y
refine_1 :
  ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1) (hz : a * x + 0 * y ∈ Ioc x y),
    ∃ (a_1 : 𝕜) (b : 𝕜), 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y
⊢ ∃ (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
have refine_1₁ : ∀ (hb' : 0 < b), ∃ (a_1 : 𝕜) (b_1 : 𝕜), 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y
Tactic: obtain rfl | hb' := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ ∃ (a_1 : 𝕜) (b : 𝕜), 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y
have hab₁ : a = 1
Tactic: rw [add_zero] at hab
Cleared hypotheses: hab, hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ ∃ (a_1 : 𝕜) (b : 𝕜), 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y
have hz₁ : x ∈ Ioc x y
Tactic: rw [hab, one_mul, zero_mul, add_zero] at hz
Cleared hypotheses: hz
-- 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
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a * x + b * y ∈ Ioc x y
have refine_2 : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1), 0 * x + b * y ∈ Ioc x y
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha, hab
-- 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
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
refine_2 : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1), 0 * x + b * y ∈ Ioc x y
⊢ a * x + b * y ∈ Ioc x y
have refine_2₁ : ∀ (ha' : 0 < a), a * x + b * y ∈ Ioc x y
Tactic: obtain rfl | ha' := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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
⊢ 0 * x + b * y ∈ Ioc x y
have hab₁ : b = 1
Tactic: rw [zero_add] at hab
Cleared hypotheses: hab
-- 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
b : 𝕜
hb : 0 < b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
⊢ 0 * x + b * y ∈ Ioc x y
have refine_2 : 0 * x + 1 * y ∈ Ioc x y
Tactic: rwa [hab, one_mul, zero_mul, zero_add, right_mem_Ioc]
-- 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
b : 𝕜
hb : 0 < b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
refine_2 : 0 * x + 1 * y ∈ Ioc x y
⊢ 0 * x + b * y ∈ Ioc x y
have refine_2₁ : 0 * x + y ∈ Ioc x y
Tactic: rwa [hab, one_mul, zero_mul, zero_add, right_mem_Ioc]
-- 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
b : 𝕜
hb : 0 < b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
refine_2 : 0 * x + 1 * y ∈ Ioc x y
refine_2₁ : 0 * x + y ∈ Ioc x y
⊢ 0 * x + b * y ∈ Ioc x y
have refine_2₂ : 0 + y ∈ Ioc x y
Tactic: rwa [hab, one_mul, zero_mul, zero_add, right_mem_Ioc]
-- 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
b : 𝕜
hb : 0 < b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
refine_2 : 0 * x + 1 * y ∈ Ioc x y
refine_2₁ : 0 * x + y ∈ Ioc x y
refine_2₂ : 0 + y ∈ Ioc x y
⊢ 0 * x + b * y ∈ Ioc x y
have refine_2₃ : y ∈ Ioc x y
Tactic: rwa [hab, one_mul, zero_mul, zero_add, right_mem_Ioc]
-- 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 : 𝕜
h : x < y
⊢ z ∈ Ico x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
have refine_1 : ∀ (hz : z ∈ Ico x y), ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
Tactic: refine ⟨fun hz => ?_, ?_⟩
-- 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 : 𝕜
h : x < y
refine_1 : ∀ (hz : z ∈ Ico x y), ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
⊢ z ∈ Ico x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
have refine_2 : (∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ico x y
Tactic: refine ⟨fun hz => ?_, ?_⟩
-- 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 : 𝕜
h : x < y
hz : z ∈ Ico x y
⊢ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
have 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
Tactic: obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ico_subset_Icc_self hz)
Cleared hypotheses: z, hz
-- 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
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
have 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
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha, hab, hz
-- 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
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
⊢ ∃ (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
have 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
Tactic: obtain rfl | ha' := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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
⊢ ∃ (a : 𝕜) (b_1 : 𝕜), 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y
have hab₁ : b = 1
Tactic: rw [zero_add] at hab
Cleared hypotheses: hab, hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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
⊢ ∃ (a : 𝕜) (b_1 : 𝕜), 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y
have hz₁ : y ∈ Ico x y
Tactic: rw [hab, one_mul, zero_mul, zero_add] at hz
Cleared hypotheses: hz
-- 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
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * x + b * y ∈ Ico x y
have refine_2 : ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1), a * x + 0 * y ∈ Ico x y
Tactic: obtain rfl | hb' := hb.eq_or_lt
Cleared hypotheses: b, hb, hab
-- 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
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
⊢ a * x + b * y ∈ Ico x y
have refine_2₁ : ∀ (hb' : 0 < b), a * x + b * y ∈ Ico x y
Tactic: obtain rfl | hb' := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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 * x + 0 * y ∈ Ico x y
have hab₁ : a = 1
Tactic: rw [add_zero] at hab
Cleared hypotheses: hab
-- 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
a : 𝕜
ha : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
⊢ a * x + 0 * y ∈ Ico x y
have refine_2 : 1 * x + 0 * y ∈ Ico x y
Tactic: rwa [hab, one_mul, zero_mul, add_zero, left_mem_Ico]
-- 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
a : 𝕜
ha : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
refine_2 : 1 * x + 0 * y ∈ Ico x y
⊢ a * x + 0 * y ∈ Ico x y
have refine_2₁ : x + 0 * y ∈ Ico x y
Tactic: rwa [hab, one_mul, zero_mul, add_zero, left_mem_Ico]
-- 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
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
⊢ a * x + 0 * y ∈ Ico x y
have refine_2₂ : x + 0 ∈ Ico x y
Tactic: rwa [hab, one_mul, zero_mul, add_zero, left_mem_Ico]
-- 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
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
⊢ a * x + 0 * y ∈ Ico x y
have refine_2₃ : x ∈ Ico x y
Tactic: rwa [hab, one_mul, zero_mul, add_zero, left_mem_Ico]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
⊢ a ∈ Icc x y → a ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]
have this : ∀ (hxa : x ≤ a) (hay : a ≤ y), a ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]
Tactic: ⟨hxa, hay⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
hxa : x ≤ a
hay : a ≤ y
⊢ a ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]
have hxa₁ : (↑x : 𝕜) ≤ (↑a : 𝕜)
Tactic: rw [← Subtype.coe_le_coe] at hxa hay
Cleared hypotheses: hxa, hay
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
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 ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]
have hay₁ : (↑a : 𝕜) ≤ (↑y : 𝕜)
Tactic: rw [← Subtype.coe_le_coe] at hxa hay
Cleared hypotheses: hxa, hay
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y a : { t : 𝕜 // 0 ≤ t }
hxa : (↑x : 𝕜) ≤ (↑a : 𝕜)
hay : (↑a : 𝕜) ≤ (↑y : 𝕜)
⊢ a ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]
have 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]
Tactic: rcases Icc_subset_segment ⟨hxa, hay⟩ with ⟨t₁, t₂, t₁_nonneg, t₂_nonneg, t_add, hta⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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]
have refine_1 : Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₁ t₁_nonneg + Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₂ t₂_nonneg = 1
Tactic: refine ⟨⟨t₁, t₁_nonneg⟩, ⟨t₂, t₂_nonneg⟩, zero_le, zero_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 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
⊢ a ∈ [x -[{ t : 𝕜 // 0 ≤ t }] y]
have 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
Tactic: refine ⟨⟨t₁, t₁_nonneg⟩, ⟨t₂, t₂_nonneg⟩, zero_le, zero_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 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
have refine_1 : (↑(Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₁ t₁_nonneg + Subtype.mk (p := fun (t : 𝕜) ↦ 0 ≤ t) t₂ t₂_nonneg) : 𝕜) =
  (↑1 : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
have 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 : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x y : { t : 𝕜 // 0 ≤ t }
⊢ [x -[{ t : 𝕜 // 0 ≤ t }] y] = uIcc x y
have inl : ∀ (h : x ≤ y), [x -[{ t : 𝕜 // 0 ≤ t }] 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
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
⊢ [x -[{ t : 𝕜 // 0 ≤ t }] y] = uIcc x y
have inr : ∀ (h : y ≤ x), [x -[{ t : 𝕜 // 0 ≤ t }] 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
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
⊢ (fun (x : E) ↦ (x, y)) '' [x₁ -[𝕜] x₂] = [(x₁, y) -[𝕜] (x₂, y)]
have 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})
Tactic: rw [segment_eq_image₂, segment_eq_image₂, image_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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})
have 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)
Tactic: refine EqOn.image_eq fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ (fun (y : F) ↦ (x, y)) '' [y₁ -[𝕜] y₂] = [(x, y₁) -[𝕜] (x, y₂)]
have 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})
Tactic: rw [segment_eq_image₂, segment_eq_image₂, image_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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})
have 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₂)
Tactic: refine EqOn.image_eq fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ (fun (x : E) ↦ (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)
have 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})
Tactic: rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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})
have 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)
Tactic: refine EqOn.image_eq fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ (fun (y : F) ↦ (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)
have 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})
Tactic: rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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})
have 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₂)
Tactic: refine EqOn.image_eq fun a ha ↦ ?_