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
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y ((lineMap x y : (a : R) → P) r)
refine_1 :
  ∀ (hrlt : 1 < r),
    Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) r : P)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) r : P)
have refine_1₁ : ∀ (hr : LE.le.{u_1} (α := R) 1 1) (h : Sbtw R x y ((lineMap x y : (a : R) → P) 1)),
  Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) 1 : P)
Tactic: rcases hr.lt_or_eq with (hrlt | rfl)
Cleared hypotheses: r, hr, 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
x y z : P
h : x ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z
⊢ Sbtw R x y z
have refine_2 : ∀ (hne : x ≠ y) (r : R) (hr : Membership.mem (γ := Set R) (Set.Ioi 1) r), Sbtw R x y ((lineMap x y : (a : R) → P) r)
Tactic: rcases h with ⟨hne, r, hr, rfl⟩
Cleared hypotheses: z, h
-- 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
x y : P
hne : x ≠ y
r : R
hr : Membership.mem (γ := Set R) (Set.Ioi 1) r
⊢ Sbtw R x y ((lineMap x y : (a : R) → P) r)
have hr₁ : 1 < r
Tactic: rw [Set.mem_Ioi] at hr
Cleared hypotheses: hr
-- 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
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ Sbtw R x y ((lineMap x y : (a : R) → P) r)
have refine_2 : y ≠ (lineMap x y : (a : R) → P) r
Tactic: refine
      ⟨wbtw_iff_left_eq_or_right_mem_image_Ici.2
          (Or.inr (Set.mem_image_of_mem _ (Set.mem_of_mem_of_subset hr Set.Ioi_subset_Ici_self))),
        hne.symm, ?_⟩
-- 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
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ y ≠ (lineMap x y : (a : R) → P) r
have refine_2 : y -ᵥ x - r • (y -ᵥ x) ≠ 0
Tactic: rw [lineMap_apply, ← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub]
-- 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
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ y -ᵥ x - r • (y -ᵥ x) ≠ 0
have refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) - r • (y -ᵥ x) ≠ 0
Tactic: nth_rw 1 [← one_smul R (y -ᵥ x)]
-- 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
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) - r • (y -ᵥ x) ≠ 0
have refine_2 : 1 ≠ r ∧ y ≠ x
Tactic: rw [← sub_smul, smul_ne_zero_iff, vsub_ne_zero, sub_ne_zero]
-- 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
x y z : P
⊢ Wbtw R x y z ↔
    z = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ici 1)) x
have rw : Wbtw R z y x ↔
  z = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ici 1)) x
Tactic: rw [wbtw_comm, wbtw_iff_left_eq_or_right_mem_image_Ici]
-- 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
x y z : P
rw :
  Wbtw R z y x ↔
    z = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ici 1)) x
⊢ Wbtw R x y z ↔
    z = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ici 1)) x
have rw₁ : z = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ici 1)) x ↔
  z = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ici 1)) x
Tactic: rw [wbtw_comm, wbtw_iff_left_eq_or_right_mem_image_Ici]
-- 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
x y z : P
⊢ Sbtw R x y z ↔
    z ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ioi 1)) x
have rw : Sbtw R z y x ↔
  z ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ioi 1)) x
Tactic: rw [sbtw_comm, sbtw_iff_left_ne_and_right_mem_image_Ioi]
-- 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
x y z : P
rw :
  Sbtw R z y x ↔
    z ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ioi 1)) x
⊢ Sbtw R x y z ↔
    z ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ioi 1)) x
have rw₁ : z ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ioi 1)) x ↔
  z ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ioi 1)) x
Tactic: rw [sbtw_comm, sbtw_iff_left_ne_and_right_mem_image_Ioi]
-- 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 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : P
s : AffineSubspace R P
hxyz : Wbtw R x y z
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ z ∈ s
have obtain : ∀ (ε : R) (hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) ε : P))
  (hxy : x ≠ (lineMap x z : (a : R) → P) ε), z ∈ s
Tactic: obtain ⟨ε, -, rfl⟩ := hxyz
Cleared hypotheses: y, hxyz, hy, hxy
-- 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 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
ε : R
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) ε : P)
hxy : x ≠ (lineMap x z : (a : R) → P) ε
⊢ z ∈ s
have hε : ε ≠ 0
Tactic: have hε : ε ≠ 0 := by rintro rfl; simp at hxy
-- 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
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)
have refine : (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x
Tactic: refine ⟨r₁ / r₂, ⟨div_nonneg hr₁ (hr₁.trans hr₂), div_le_one_of_le₀ hr₂ (hr₁.trans hr₂)⟩, ?_⟩
-- 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
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
⊢ (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x
have pos : ∀ (h : r₁ = 0), (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x
Tactic: by_cases h : r₁ = 0
-- 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
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
pos : ∀ (h : r₁ = 0), (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x
⊢ (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x
have neg : ∀ (h : ¬r₁ = 0), (lineMap x (r₂ • v +ᵥ x) : (a : R) → P) (r₁ / r₂) = r₁ • v +ᵥ x
Tactic: by_cases h : r₁ = 0
-- 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
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
have inl : ∀ (h : r₁ ≤ r₂), Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
Tactic: rcases le_total r₁ r₂ with (h | 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
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
inl : ∀ (h : r₁ ≤ r₂), Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
have inr : ∀ (h : r₂ ≤ r₁), Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
Tactic: rcases le_total r₁ r₂ with (h | 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
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)
have h : r₁ • v +ᵥ x = -r₁ • -v +ᵥ x
Tactic: convert!
    wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x (-v) (Left.nonneg_neg_iff.2 hr₁)
      (neg_le_neg_iff.2 hr₂) using
    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
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ r₁
h : r₁ • v +ᵥ x = -r₁ • -v +ᵥ x
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)
have h₁ : r₂ • v +ᵥ x = -r₂ • -v +ᵥ x
Tactic: convert!
    wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x (-v) (Left.nonneg_neg_iff.2 hr₁)
      (neg_le_neg_iff.2 hr₂) using
    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
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ r₁
⊢ r₁ • v +ᵥ x = -r₁ • -v +ᵥ x
have h : r₁ • v +ᵥ x = r₁ • v +ᵥ x
Tactic: rw [neg_smul_neg]
-- 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
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ r₁
⊢ r₂ • v +ᵥ x = -r₂ • -v +ᵥ x
have h : r₂ • v +ᵥ x = r₂ • v +ᵥ x
Tactic: rw [neg_smul_neg]
-- 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
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
have inl : ∀ (h : r₁ ≤ r₂), Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
Tactic: rcases le_total r₁ r₂ with (h | 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
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
inl : ∀ (h : r₁ ≤ r₂), Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
have inr : ∀ (h : r₂ ≤ r₁), Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
Tactic: rcases le_total r₁ r₂ with (h | 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
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : 0 ≤ r₂
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)
have h : x = -r₁ • v +ᵥ r₁ • v +ᵥ x
Tactic: convert!
    wbtw_smul_vadd_smul_vadd_of_nonneg_of_le (r₁ • v +ᵥ x) v (Left.nonneg_neg_iff.2 hr₁)
      (neg_le_sub_iff_le_add.2 ((le_add_iff_nonneg_left r₁).2 hr₂)) using
    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
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : 0 ≤ r₂
h : x = -r₁ • v +ᵥ r₁ • v +ᵥ x
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)
have h₁ : r₂ • v +ᵥ x = (r₂ - r₁) • v +ᵥ r₁ • v +ᵥ x
Tactic: convert!
    wbtw_smul_vadd_smul_vadd_of_nonneg_of_le (r₁ • v +ᵥ x) v (Left.nonneg_neg_iff.2 hr₁)
      (neg_le_sub_iff_le_add.2 ((le_add_iff_nonneg_left r₁).2 hr₂)) using
    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
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)
have rw : Wbtw R (r₂ • v +ᵥ x) x (r₁ • v +ᵥ x)
Tactic: rw [wbtw_comm]
-- 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 w y z
h₂ : Wbtw R w x y
⊢ Wbtw R x y z
have rcases : ∀ (t₁ : R) (ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁) (h₂ : Wbtw R w x ((lineMap w z : (a : R) → P) t₁)),
  Wbtw R x ((lineMap w z : (a : R) → P) t₁) z
Tactic: rcases h₁ with ⟨t₁, ht₁, rfl⟩
Cleared hypotheses: y, h₁, 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 z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
h₂ : Wbtw R w x ((lineMap w z : (a : R) → P) t₁)
⊢ Wbtw R x ((lineMap w z : (a : R) → P) t₁) z
have rcases : ∀ (t₂ : R) (ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂),
  Wbtw R ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) ((lineMap w z : (a : R) → P) t₁) z
Tactic: rcases h₂ with ⟨t₂, ht₂, rfl⟩
Cleared hypotheses: x, 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 z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
⊢ Wbtw R ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) ((lineMap w z : (a : R) → P) t₁) z
have t₃ : Eq.{u_4 + 1} (α := P)
  (((lineMap ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) z : R →ᵃ[R] P) : (a : R) → P)
      ((t₁ - t₂ * t₁) / (1 - t₂ * t₁)) :
    P)
  ((lineMap w z : (a : R) → P) t₁ : P)
Tactic: refine
    ⟨(t₁ - t₂ * t₁) / (1 - t₂ * t₁),
      ⟨div_nonneg (sub_nonneg.2 (mul_le_of_le_one_left ht₁.1 ht₂.2))
          (sub_nonneg.2 (mul_le_one₀ ht₂.2 ht₁.1 ht₁.2)), div_le_one_of_le₀
            (sub_le_sub_right ht₁.2 _) (sub_nonneg.2 (mul_le_one₀ 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 z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
⊢ Eq.{u_4 + 1} (α := P)
    (((lineMap ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) z : R →ᵃ[R] P) : (a : R) → P)
        ((t₁ - t₂ * t₁) / (1 - t₂ * t₁)) :
      P)
    ((lineMap w z : (a : R) → P) t₁ : P)
have simp : ((t₁ - t₂ * t₁ - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
Tactic: simp only [lineMap_apply, smul_smul, ← add_vadd, vsub_vadd_eq_vsub_sub, smul_sub, ← sub_smul,
    ← add_smul, vadd_vsub, vadd_right_cancel_iff, div_mul_eq_mul_div, div_sub_div_same]
-- 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 z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
⊢ ((t₁ - t₂ * t₁ - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
have nth_rw : (((t₁ - t₂ * t₁) * 1 - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
Tactic: nth_rw 1 [← mul_one (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 z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
⊢ (((t₁ - t₂ * t₁) * 1 - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
have rw : ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
Tactic: rw [← mul_sub, mul_div_assoc]
-- 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 z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
have pos : ∀ (h : 1 - t₂ * t₁ = 0), ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
Tactic: by_cases h : 1 - t₂ * t₁ = 0
-- 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 z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
pos : ∀ (h : 1 - t₂ * t₁ = 0), ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
have neg : ∀ (h : ¬1 - t₂ * t₁ = 0), ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
Tactic: by_cases h : 1 - t₂ * t₁ = 0
-- 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 z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
h : 1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
have h₁ : t₂ * t₁ = 1
Tactic: rw [sub_eq_zero, eq_comm] at h
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 z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
h : t₂ * t₁ = 1
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
have pos : ((t₁ - 1) * (HSub.hSub (α := R) 1 1 / HSub.hSub (α := R) 1 1) + 1) • (z -ᵥ w) = t₁ • (z -ᵥ w)
Tactic: rw [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 z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
h : t₂ * t₁ = 1
⊢ ((t₁ - 1) * (HSub.hSub (α := R) 1 1 / HSub.hSub (α := R) 1 1) + 1) • (z -ᵥ w) = t₁ • (z -ᵥ w)
have pos : t₁ = 1
Tactic: suffices t₁ = 1 by simp [this]
-- 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 z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
h : ¬1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
have neg : ((t₁ - t₂ * t₁) * 1 + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
Tactic: rw [div_self 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₁ : Wbtw R w x z
h₂ : Wbtw R x y z
⊢ Wbtw R w x y
have rw : ∀ (h₁ : Wbtw R z x w) (h₂ : Wbtw R z y x), Wbtw R y x w
Tactic: rw [wbtw_comm] at *
Cleared hypotheses: h₁, 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₁ : Wbtw R w x y
h₂ : Wbtw R x y z
h_ne : x ≠ y
⊢ Wbtw R w x z
have rcases : ∀ (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
Tactic: rcases h₁ with ⟨t₁, ht₁, hx⟩
Cleared hypotheses: h₁