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 : ZeroLEOneClass 𝕜
inst_4 : MulActionWithZero 𝕜 E
x y : E
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + 0 = x
Tactic: rw [zero_smul, one_smul, add_zero]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : MulActionWithZero 𝕜 E
x y : E
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + 0 = x
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
have rw₁ : x + 0 = x
Tactic: rw [zero_smul, one_smul, add_zero]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : MulActionWithZero 𝕜 E
x y : E
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + 0 = x
rw₁ : x + 0 = x
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
have rw₂ : x = x
Tactic: rw [zero_smul, one_smul, add_zero]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
⊢ insert x (insert y (openSegment 𝕜 x y)) = [x -[𝕜] y]
have simp : [x -[𝕜] y] ⊆ insert x (insert y (openSegment 𝕜 x y))
Tactic: simp only [subset_antisymm_iff, insert_subset_iff, left_mem_segment, right_mem_segment,
    openSegment_subset_segment, true_and]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ insert x (insert y (openSegment 𝕜 x y))
have refine_1 : 0 = b → a • x + b • y = x
Tactic: refine hb.eq_or_lt.imp ?_ fun hb' => ha.eq_or_lt.imp ?_ fun ha' => ?_
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_1 : 0 = b → a • x + b • y = x
⊢ a • x + b • y ∈ insert x (insert y (openSegment 𝕜 x y))
have refine_2 : ∀ (hb' : 0 < b), 0 = a → a • x + b • y = y
Tactic: refine hb.eq_or_lt.imp ?_ fun hb' => ha.eq_or_lt.imp ?_ fun ha' => ?_
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_1 : 0 = b → a • x + b • y = x
refine_2 : ∀ (hb' : 0 < b), 0 = a → a • x + b • y = y
⊢ a • x + b • y ∈ insert x (insert y (openSegment 𝕜 x y))
have refine_3 : ∀ (hb' : 0 < b) (ha' : 0 < a), a • x + b • y ∈ openSegment 𝕜 x y
Tactic: refine hb.eq_or_lt.imp ?_ fun hb' => ha.eq_or_lt.imp ?_ fun ha' => ?_
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
have refine_1 : (a + 0) • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
Tactic: rw [← add_zero a, hab, one_smul, zero_smul, add_zero]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
refine_1 : (a + 0) • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
have refine_1₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
Tactic: rw [← add_zero a, hab, one_smul, zero_smul, add_zero]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
refine_1 : (a + 0) • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
refine_1₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
have refine_1₂ : x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
Tactic: rw [← add_zero a, hab, one_smul, zero_smul, add_zero]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
refine_1 : (a + 0) • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
refine_1₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
refine_1₂ : x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
have refine_1₃ : x + 0 = x
Tactic: rw [← add_zero a, hab, one_smul, zero_smul, add_zero]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
refine_1 : (a + 0) • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
refine_1₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
refine_1₂ : x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
refine_1₃ : x + 0 = x
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
have refine_1₄ : x = x
Tactic: rw [← add_zero a, hab, one_smul, zero_smul, add_zero]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
b : 𝕜
hb : 0 ≤ b
hb' : 0 < b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y = y
have refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + (0 + b) • y = y
Tactic: rw [← zero_add b, hab, one_smul, zero_smul, zero_add]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
b : 𝕜
hb : 0 ≤ b
hb' : 0 < b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + (0 + b) • y = y
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y = y
have refine_2₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y = y
Tactic: rw [← zero_add b, hab, one_smul, zero_smul, zero_add]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
b : 𝕜
hb : 0 ≤ b
hb' : 0 < b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + (0 + b) • y = y
refine_2₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y = y
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y = y
have refine_2₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + y = y
Tactic: rw [← zero_add b, hab, one_smul, zero_smul, zero_add]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
b : 𝕜
hb : 0 ≤ b
hb' : 0 < b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + (0 + b) • y = y
refine_2₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y = y
refine_2₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + y = y
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y = y
have refine_2₃ : 0 + y = y
Tactic: rw [← zero_add b, hab, one_smul, zero_smul, zero_add]
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y : E
b : 𝕜
hb : 0 ≤ b
hb' : 0 < b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + (0 + b) • y = y
refine_2₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y = y
refine_2₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + y = y
refine_2₃ : 0 + y = y
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y = y
have refine_2₄ : y = y
Tactic: rw [← zero_add b, hab, one_smul, zero_smul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ [x -[𝕜] y]
⊢ z ∈ openSegment 𝕜 x y
have hz₁ : z ∈ insert x (insert y (openSegment 𝕜 x y))
Tactic: rw [← insert_endpoints_openSegment] at hz
Cleared hypotheses: hz
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_7
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
x y z : E
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ z ∈ [x -[𝕜] y]
have refine_1 : 0 ≤ HSMul.hSMul (β := 𝕜) a 1
Tactic: refine ⟨_, _, ?_, ?_, by simpa [add_smul] using congr($(hab) • (1 : 𝕜)), by simpa⟩
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_7
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
x y z : E
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : a • x + b • y = z
refine_1 : 0 ≤ HSMul.hSMul (β := 𝕜) a 1
⊢ z ∈ [x -[𝕜] y]
have refine_2 : 0 ≤ HSMul.hSMul (β := 𝕜) b 1
Tactic: refine ⟨_, _, ?_, ?_, by simpa [add_smul] using congr($(hab) • (1 : 𝕜)), by simpa⟩
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_7
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : Nontrivial 𝕜
inst_11 : SMulPosStrictMono R 𝕜
x y z : E
a b : R
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ z ∈ openSegment 𝕜 x y
have refine_1 : 0 < HSMul.hSMul (β := 𝕜) a 1
Tactic: refine ⟨_, _, ?_, ?_, by simpa [add_smul] using congr($(hab) • (1 : 𝕜)), by simpa⟩
-- 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 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_7
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : Nontrivial 𝕜
inst_11 : SMulPosStrictMono R 𝕜
x y z : E
a b : R
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : a • x + b • y = z
refine_1 : 0 < HSMul.hSMul (β := 𝕜) a 1
⊢ z ∈ openSegment 𝕜 x y
have refine_2 : 0 < HSMul.hSMul (β := 𝕜) b 1
Tactic: refine ⟨_, _, ?_, ?_, by simpa [add_smul] using congr($(hab) • (1 : 𝕜)), by simpa⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
x z : E
h : z = x
⊢ z ∈ openSegment 𝕜 x x
have obtain : ∀ (a : 𝕜) (ha₀ : 0 < a) (ha₁ : a < 1), z ∈ openSegment 𝕜 x x
Tactic: obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ z ∈ openSegment 𝕜 x x
have refine : a • x + (1 - a) • x = z
Tactic: refine ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ a • x + (1 - a) • x = z
have rw : (a + (1 - a)) • x = z
Tactic: rw [← add_smul, add_sub_cancel, one_smul, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
rw : (a + (1 - a)) • x = z
⊢ a • x + (1 - a) • x = z
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x = z
Tactic: rw [← add_smul, add_sub_cancel, one_smul, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
rw : (a + (1 - a)) • x = z
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x = z
⊢ a • x + (1 - a) • x = z
have rw₂ : x = z
Tactic: rw [← add_smul, add_sub_cancel, one_smul, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
rw : (a + (1 - a)) • x = z
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x = z
rw₂ : x = z
⊢ a • x + (1 - a) • x = z
have rw₃ : x = x
Tactic: rw [← add_smul, add_sub_cancel, one_smul, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
⊢ [x -[𝕜] y] = (fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Icc 0 1
have h : ∀ (a : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) a → x + a • (y - x) = (1 - a) • x + a • y
Tactic: convert! segment_eq_image 𝕜 x y using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
h : Membership.mem (γ := Set 𝕜) (Icc 0 1) a
⊢ x + a • (y - x) = (1 - a) • x + a • y
have h : x + (a • y - a • x) = x - a • x + a • y
Tactic: simp only [smul_sub, sub_smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
⊢ openSegment 𝕜 x y = (fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Ioo 0 1
have h : ∀ (a : 𝕜), Membership.mem (γ := Set 𝕜) (Ioo 0 1) a → x + a • (y - x) = (1 - a) • x + a • y
Tactic: convert! openSegment_eq_image 𝕜 x y using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
h : Membership.mem (γ := Set 𝕜) (Ioo 0 1) a
⊢ x + a • (y - x) = (1 - a) • x + a • y
have h : x + (a • y - a • x) = x - a • x + a • y
Tactic: simp only [smul_sub, sub_smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
⊢ [x -[𝕜] y] = image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) (Icc 0 1)
have h : ∀ (a : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) a → (AffineMap.lineMap x y : (a : 𝕜) → E) a = (1 - a) • x + a • y
Tactic: convert! segment_eq_image 𝕜 x y using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
⊢ openSegment 𝕜 x y = image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) (Ioo 0 1)
have h : ∀ (a : 𝕜), Membership.mem (γ := Set 𝕜) (Ioo 0 1) a → (AffineMap.lineMap x y : (a : 𝕜) → E) a = (1 - a) • x + a • y
Tactic: convert! openSegment_eq_image 𝕜 x y using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' [a -[𝕜] b]) x ↔
    Membership.mem (γ := Set F) ([(f : (a : E) → F) a -[𝕜] (f : (a : E) → F) b] : Set F) x
have simp_rw : Membership.mem (γ := Set F)
    (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F)
      (image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap a b) : (a : 𝕜) → E) (Icc 0 1)))
    x ↔
  Membership.mem (γ := Set F)
    (image.{u_1, u_3} (α := 𝕜)
      (⇑(AffineMap.lineMap ((f : (a : E) → F) a) ((f : (a : E) → F) b) : 𝕜 →ᵃ[𝕜] F) : (a : 𝕜) → F) (Icc 0 1))
    x
Tactic: simp_rw [segment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
simp_rw :
  Membership.mem (γ := Set F)
      (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F)
        (image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap a b) : (a : 𝕜) → E) (Icc 0 1)))
      x ↔
    Membership.mem (γ := Set F)
      (image.{u_1, u_3} (α := 𝕜)
        (⇑(AffineMap.lineMap ((f : (a : E) → F) a) ((f : (a : E) → F) b) : 𝕜 →ᵃ[𝕜] F) : (a : 𝕜) → F) (Icc 0 1))
      x
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' [a -[𝕜] b]) x ↔
    Membership.mem (γ := Set F) ([(f : (a : E) → F) a -[𝕜] (f : (a : E) → F) b] : Set F) x
have simp_rw₁ : (∃ (x_1 : E),
    (∃ (x : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x ∧ (AffineMap.lineMap a b : (a : 𝕜) → E) x = x_1) ∧
      (f : (a : E) → F) x_1 = x) ↔
  ∃ (x_1 : 𝕜),
    Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧
      ((AffineMap.lineMap ((f : (a : E) → F) a) ((f : (a : E) → F) b) : 𝕜 →ᵃ[𝕜] F) : (a : 𝕜) → F) x_1 = x
Tactic: simp_rw [segment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
simp_rw :
  Membership.mem (γ := Set F)
      (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F)
        (image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap a b) : (a : 𝕜) → E) (Icc 0 1)))
      x ↔
    Membership.mem (γ := Set F)
      (image.{u_1, u_3} (α := 𝕜)
        (⇑(AffineMap.lineMap ((f : (a : E) → F) a) ((f : (a : E) → F) b) : 𝕜 →ᵃ[𝕜] F) : (a : 𝕜) → F) (Icc 0 1))
      x
simp_rw₁ :
  (∃ (x_1 : E),
      (∃ (x : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x ∧ (AffineMap.lineMap a b : (a : 𝕜) → E) x = x_1) ∧
        (f : (a : E) → F) x_1 = x) ↔
    ∃ (x_1 : 𝕜),
      Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧
        ((AffineMap.lineMap ((f : (a : E) → F) a) ((f : (a : E) → F) b) : 𝕜 →ᵃ[𝕜] F) : (a : 𝕜) → F) x_1 = x
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' [a -[𝕜] b]) x ↔
    Membership.mem (γ := Set F) ([(f : (a : E) → F) a -[𝕜] (f : (a : E) → F) b] : Set F) x
have simp_rw₂ : (∃ (a_1 : 𝕜),
    Membership.mem (γ := Set 𝕜) (Icc 0 1) a_1 ∧ (f : (a : E) → F) ((AffineMap.lineMap a b : (a : 𝕜) → E) a_1 : E) = x) ↔
  ∃ (x_1 : 𝕜),
    Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧
      ((AffineMap.lineMap ((f : (a : E) → F) a) ((f : (a : E) → F) b) : 𝕜 →ᵃ[𝕜] F) : (a : 𝕜) → F) x_1 = x
Tactic: simp_rw [segment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a x b c : E
⊢ a + x ∈ [a + b -[𝕜] a + c] ↔ x ∈ [b -[𝕜] c]
have simp_rw : a +ᵥ x ∈ [a +ᵥ b -[𝕜] a +ᵥ c] ↔ x ∈ [b -[𝕜] c]
Tactic: simp_rw [← vadd_eq_add, ← vadd_segment, vadd_mem_vadd_set_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a x b c : E
simp_rw : a +ᵥ x ∈ [a +ᵥ b -[𝕜] a +ᵥ c] ↔ x ∈ [b -[𝕜] c]
⊢ a + x ∈ [a + b -[𝕜] a + c] ↔ x ∈ [b -[𝕜] c]
have simp_rw₁ : a +ᵥ x ∈ a +ᵥ [b -[𝕜] c] ↔ x ∈ [b -[𝕜] c]
Tactic: simp_rw [← vadd_eq_add, ← vadd_segment, vadd_mem_vadd_set_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a x b c : E
⊢ a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c
have simp_rw : a +ᵥ x ∈ openSegment 𝕜 (a +ᵥ b) (a +ᵥ c) ↔ x ∈ openSegment 𝕜 b c
Tactic: simp_rw [← vadd_eq_add, ← vadd_openSegment, vadd_mem_vadd_set_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a x b c : E
simp_rw : a +ᵥ x ∈ openSegment 𝕜 (a +ᵥ b) (a +ᵥ c) ↔ x ∈ openSegment 𝕜 b c
⊢ a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c
have simp_rw₁ : a +ᵥ x ∈ a +ᵥ openSegment 𝕜 b c ↔ x ∈ openSegment 𝕜 b c
Tactic: simp_rw [← vadd_eq_add, ← vadd_openSegment, vadd_mem_vadd_set_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
⊢ z ∈ [c -[𝕜] x] ∩ [c -[𝕜] y] → Membership.mem (γ := Set E) {c} z
have this : ∀ (hzt : z ∈ [c -[𝕜] x]) (hzs : z ∈ [c -[𝕜] y]), Membership.mem (γ := Set E) {c} z
Tactic: ⟨hzt, hzs⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
hzt : z ∈ [c -[𝕜] x]
hzs : z ∈ [c -[𝕜] y]
⊢ Membership.mem (γ := Set E) {c} z
have hzt₁ : ∃ (x_1 : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧ (1 - x_1) • c + x_1 • x = z
Tactic: rw [segment_eq_image, mem_image] at hzt hzs
Cleared hypotheses: hzt, hzs