awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h₂ : Wbtw R x y z
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
⊢ Wbtw R w x z
have rcases : ∀ (t₂ : R) (ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂) (hy : (lineMap x z : (a : R) → P) t₂ = y), Wbtw R w x z
Tactic: rcases h₂ with ⟨t₂, ht₂, hy⟩
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
⊢ Wbtw R w x z
have refine_1 : Membership.mem (γ := Set R) (Set.Icc 0 1) (t₁ * t₂ / (1 - t₁ + t₁ * t₂))
Tactic: refine ⟨t₁ * t₂ / (1 - t₁ + t₁ * t₂), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
refine_1 : Membership.mem (γ := Set R) (Set.Icc 0 1) (t₁ * t₂ / (1 - t₁ + t₁ * t₂))
⊢ Wbtw R w x z
have refine_2 : (lineMap w z : (a : R) → P) (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) = x
Tactic: refine ⟨t₁ * t₂ / (1 - t₁ + t₁ * t₂), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (t₁ * t₂ / (1 - t₁ + t₁ * t₂))
have refine_1 : 0 ≤ t₁ * t₂ / (1 - t₁ + t₁ * t₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
refine_1 : 0 ≤ t₁ * t₂ / (1 - t₁ + t₁ * t₂)
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (t₁ * t₂ / (1 - t₁ + t₁ * t₂))
have refine_1₁ : t₁ * t₂ / (1 - t₁ + t₁ * t₂) ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
⊢ 0 ≤ t₁ * t₂ / (1 - t₁ + t₁ * t₂)
have refine_1 : 0 ≤ 1 - t₁ + t₁ * t₂
Tactic: apply div_nonneg (mul_nonneg ht₁.1 ht₂.1)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
⊢ 0 ≤ 1 - t₁ + t₁ * t₂
have nlinarith : 1 - t₁ + t₁ * t₂ < 0 → 1 - t₁ + t₁ * t₂ - 0 + (t₁ - 1) + (0 - (0 - t₁) * (0 - t₂)) = 0
Tactic: nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
⊢ t₁ * t₂ / (1 - t₁ + t₁ * t₂) ≤ 1
have refine_1 : t₁ * t₂ ≤ 1 - t₁ + t₁ * t₂
Tactic: apply div_le_one_of_le₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
refine_1 : t₁ * t₂ ≤ 1 - t₁ + t₁ * t₂
⊢ t₁ * t₂ / (1 - t₁ + t₁ * t₂) ≤ 1
have refine_1₁ : 0 ≤ 1 - t₁ + t₁ * t₂
Tactic: apply div_le_one_of_le₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
⊢ 1 - t₁ + t₁ * t₂ ≠ 0
have contrapose : ∀ (h_ne : 1 - t₁ + t₁ * t₂ = 0), x = y
Tactic: contrapose h_ne
Cleared hypotheses: h_ne
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
⊢ t₁ = 1
have nlinarith : t₁ < 1 → 1 - t₁ + t₁ * t₂ - 0 + (t₁ - 1) + (0 - (0 - t₁) * (0 - t₂)) = 0
Tactic: nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
nlinarith : t₁ < 1 → 1 - t₁ + t₁ * t₂ - 0 + (t₁ - 1) + (0 - (0 - t₁) * (0 - t₂)) = 0
⊢ t₁ = 1
have nlinarith₁ : 1 < t₁ → 1 - t₁ + (t₁ - 1) = 0
Tactic: nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
⊢ x = y
have h1 : t₁ = 1
Tactic: have h1 : t₁ = 1 := by nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
h1 : t₁ = 1
⊢ x = y
have rw : (lineMap w y : (a : R) → P) t₁ = y
Tactic: rw [← hx, h1, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
h1 : t₁ = 1
rw : (lineMap w y : (a : R) → P) t₁ = y
⊢ x = y
have rw₁ : (lineMap w y : (a : R) → P) 1 = y
Tactic: rw [← hx, h1, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
h1 : t₁ = 1
rw : (lineMap w y : (a : R) → P) t₁ = y
rw₁ : (lineMap w y : (a : R) → P) 1 = y
⊢ x = y
have rw₂ : y = y
Tactic: rw [← hx, h1, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
⊢ (lineMap w z : (a : R) → P) (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) = x
have h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
Tactic: have h_denom : 1 - t₁ + t₁ * t₂ ≠ 0 := by
    contrapose h_ne
    have h1 : t₁ = 1 := by nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]
    rw [← hx, h1, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
hx : (lineMap w y : (a : R) → P) t₁ = x
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ (lineMap w z : (a : R) → P) (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) = x
have hx₁ : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
Tactic: rw [← hy, lineMap_apply, lineMap_apply, eq_comm, eq_vadd_iff_vsub_eq] at hx
Cleared hypotheses: hx, ht₂, hy, h_denom
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ (lineMap w z : (a : R) → P) (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) = x
have refine_2 : x -ᵥ w - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
Tactic: rw [lineMap_apply, eq_comm, eq_vadd_iff_vsub_eq, div_eq_mul_inv, mul_comm, mul_smul,
    eq_inv_smul_iff₀ h_denom, add_smul, sub_smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ x -ᵥ w - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
have refine_2 : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
Tactic: nth_rw 1 [hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
have refine_2 : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
Tactic: rw [← smul_sub, mul_smul, mul_smul, vsub_sub_vsub_cancel_right, vadd_vsub, ← smul_assoc,
    ← smul_assoc, ← smul_assoc, ← smul_add, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
refine_2 : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
have refine_2₁ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
Tactic: rw [← smul_sub, mul_smul, mul_smul, vsub_sub_vsub_cancel_right, vadd_vsub, ← smul_assoc,
    ← smul_assoc, ← smul_assoc, ← smul_add, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
refine_2 : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₁ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
have refine_2₂ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
Tactic: rw [← smul_sub, mul_smul, mul_smul, vsub_sub_vsub_cancel_right, vadd_vsub, ← smul_assoc,
    ← smul_assoc, ← smul_assoc, ← smul_add, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
refine_2 : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₁ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₂ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
have refine_2₃ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
Tactic: rw [← smul_sub, mul_smul, mul_smul, vsub_sub_vsub_cancel_right, vadd_vsub, ← smul_assoc,
    ← smul_assoc, ← smul_assoc, ← smul_add, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
refine_2 : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₁ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₂ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₃ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
have refine_2₄ : t₁ • t₂ • (z -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
Tactic: rw [← smul_sub, mul_smul, mul_smul, vsub_sub_vsub_cancel_right, vadd_vsub, ← smul_assoc,
    ← smul_assoc, ← smul_assoc, ← smul_add, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
refine_2 : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₁ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₂ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₃ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₄ : t₁ • t₂ • (z -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
have refine_2₅ : (t₁ • t₂) • (z -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
Tactic: rw [← smul_sub, mul_smul, mul_smul, vsub_sub_vsub_cancel_right, vadd_vsub, ← smul_assoc,
    ← smul_assoc, ← smul_assoc, ← smul_add, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
refine_2 : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₁ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₂ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₃ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₄ : t₁ • t₂ • (z -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₅ : (t₁ • t₂) • (z -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
have refine_2₆ : (t₁ • t₂) • (z -ᵥ x) + (t₁ • t₂) • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
Tactic: rw [← smul_sub, mul_smul, mul_smul, vsub_sub_vsub_cancel_right, vadd_vsub, ← smul_assoc,
    ← smul_assoc, ← smul_assoc, ← smul_add, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
refine_2 : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₁ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₂ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₃ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₄ : t₁ • t₂ • (z -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₅ : (t₁ • t₂) • (z -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₆ : (t₁ • t₂) • (z -ᵥ x) + (t₁ • t₂) • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
have refine_2₇ : (t₁ • t₂) • (z -ᵥ x) + (t₁ • t₂) • (x -ᵥ w) = (t₁ • t₂) • (z -ᵥ w)
Tactic: rw [← smul_sub, mul_smul, mul_smul, vsub_sub_vsub_cancel_right, vadd_vsub, ← smul_assoc,
    ← smul_assoc, ← smul_assoc, ← smul_add, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
hy : (lineMap x z : (a : R) → P) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
refine_2 : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₁ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
refine_2₂ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₃ : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₄ : t₁ • t₂ • (z -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₅ : (t₁ • t₂) • (z -ᵥ x) + t₁ • t₂ • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₆ : (t₁ • t₂) • (z -ᵥ x) + (t₁ • t₂) • (x -ᵥ w) = t₁ • t₂ • (z -ᵥ w)
refine_2₇ : (t₁ • t₂) • (z -ᵥ x) + (t₁ • t₂) • (x -ᵥ w) = (t₁ • t₂) • (z -ᵥ w)
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
have refine_2₈ : (t₁ • t₂) • (z -ᵥ x + (x -ᵥ w)) = (t₁ • t₂) • (z -ᵥ w)
Tactic: rw [← smul_sub, mul_smul, mul_smul, vsub_sub_vsub_cancel_right, vadd_vsub, ← smul_assoc,
    ← smul_assoc, ← smul_assoc, ← smul_add, vsub_add_vsub_cancel]