awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2) : (a : R) → P) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw.{u_1, u_2, u_4} R (P := P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
ht : ¬Eq.{u_4 + 1} (α := List P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P) ([] : List P)
hl'' :
  Eq.{u_4 + 1} (α := List P)
    (map (⇑(lineMap ((lineMap head (tail.getLast ht2) : (a : R) → P) r) (tail.getLast ht2) : R →ᵃ[R] P) : (a : R) → P)
        l'' :
      List P)
    ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
neg : ∀ (a : R), Membership.mem (γ := List R) (0 :: map (fun (x : R) ↦ r + (1 - r) * x) l'') a → 0 ≤ a
neg₁ : SortedLE (α := R) (0 :: map (fun (x : R) ↦ r + (1 - r) * x) l'')
⊢ ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧
        map (⇑(lineMap head (tail.getLast ht2)) : (a : R) → P) l' =
          head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail
have neg₂ : map (α := R) (⇑(lineMap head (tail.getLast ht2)) : (a : R) → P) (0 :: map (fun (x : R) ↦ r + (1 - r) * x) l'') =
  head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail
Tactic: refine ⟨0 :: l''.map fun x ↦ r + (1 - r) * x, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2) : (a : R) → P) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw.{u_1, u_2, u_4} R (P := P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
ht : ¬Eq.{u_4 + 1} (α := List P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P) ([] : List P)
hl'' :
  Eq.{u_4 + 1} (α := List P)
    (map (⇑(lineMap ((lineMap head (tail.getLast ht2) : (a : R) → P) r) (tail.getLast ht2) : R →ᵃ[R] P) : (a : R) → P)
        l'' :
      List P)
    ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
⊢ ∀ (a : R), Membership.mem (γ := List R) (0 :: map (fun (x : R) ↦ r + (1 - r) * x) l'') a → 0 ≤ a
have neg : ∀ a ∈ l'', 0 ≤ r + (1 - r) * a
Tactic: simp only [mem_cons, mem_map, forall_eq_or_imp, le_refl, forall_exists_index,
                and_imp, forall_apply_eq_imp_iff₂, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2) : (a : R) → P) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw.{u_1, u_2, u_4} R (P := P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
ht : ¬Eq.{u_4 + 1} (α := List P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P) ([] : List P)
hl'' :
  Eq.{u_4 + 1} (α := List P)
    (map (⇑(lineMap ((lineMap head (tail.getLast ht2) : (a : R) → P) r) (tail.getLast ht2) : R →ᵃ[R] P) : (a : R) → P)
        l'' :
      List P)
    ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
a : R
ha : a ∈ l''
⊢ 0 ≤ r + (1 - r) * a
have this : 0 ≤ a
Tactic: have := hl''0 a ha
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2) : (a : R) → P) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw.{u_1, u_2, u_4} R (P := P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
ht : ¬Eq.{u_4 + 1} (α := List P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P) ([] : List P)
hl'' :
  Eq.{u_4 + 1} (α := List P)
    (map (⇑(lineMap ((lineMap head (tail.getLast ht2) : (a : R) → P) r) (tail.getLast ht2) : R →ᵃ[R] P) : (a : R) → P)
        l'' :
      List P)
    ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
a : R
ha : a ∈ l''
this : 0 ≤ a
⊢ 0 ≤ r + (1 - r) * a
have nlinarith : r + (1 - r) * a < 0 → 0 - r + (r + (1 - r) * a - 0) + (0 - (r - 1) * (0 - a)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2) : (a : R) → P) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw.{u_1, u_2, u_4} R (P := P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
ht : ¬Eq.{u_4 + 1} (α := List P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P) ([] : List P)
hl'' :
  Eq.{u_4 + 1} (α := List P)
    (map (⇑(lineMap ((lineMap head (tail.getLast ht2) : (a : R) → P) r) (tail.getLast ht2) : R →ᵃ[R] P) : (a : R) → P)
        l'' :
      List P)
    ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
⊢ SortedLE (α := R) (0 :: map (fun (x : R) ↦ r + (1 - r) * x) l'')
have neg : (∀ a ∈ l'', 0 ≤ r + (1 - r) * a) ∧ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) (map (fun (x : R) ↦ r + (1 - r) * x) l'')
Tactic: simp only [sortedLE_iff_pairwise, pairwise_cons, mem_map,
                forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2) : (a : R) → P) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw.{u_1, u_2, u_4} R (P := P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
ht : ¬Eq.{u_4 + 1} (α := List P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P) ([] : List P)
hl'' :
  Eq.{u_4 + 1} (α := List P)
    (map (⇑(lineMap ((lineMap head (tail.getLast ht2) : (a : R) → P) r) (tail.getLast ht2) : R →ᵃ[R] P) : (a : R) → P)
        l'' :
      List P)
    ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
⊢ (∀ a ∈ l'', 0 ≤ r + (1 - r) * a) ∧ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) (map (fun (x : R) ↦ r + (1 - r) * x) l'')
have neg : ∀ a ∈ l'', 0 ≤ r + (1 - r) * a
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2) : (a : R) → P) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw.{u_1, u_2, u_4} R (P := P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
ht : ¬Eq.{u_4 + 1} (α := List P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P) ([] : List P)
hl'' :
  Eq.{u_4 + 1} (α := List P)
    (map (⇑(lineMap ((lineMap head (tail.getLast ht2) : (a : R) → P) r) (tail.getLast ht2) : R →ᵃ[R] P) : (a : R) → P)
        l'' :
      List P)
    ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
neg : ∀ a ∈ l'', 0 ≤ r + (1 - r) * a
⊢ (∀ a ∈ l'', 0 ≤ r + (1 - r) * a) ∧ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) (map (fun (x : R) ↦ r + (1 - r) * x) l'')
have neg₁ : Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) (map (fun (x : R) ↦ r + (1 - r) * x) l'')
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2) : (a : R) → P) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw.{u_1, u_2, u_4} R (P := P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
ht : ¬Eq.{u_4 + 1} (α := List P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P) ([] : List P)
hl'' :
  Eq.{u_4 + 1} (α := List P)
    (map (⇑(lineMap ((lineMap head (tail.getLast ht2) : (a : R) → P) r) (tail.getLast ht2) : R →ᵃ[R] P) : (a : R) → P)
        l'' :
      List P)
    ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
⊢ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) (map (fun (x : R) ↦ r + (1 - r) * x) l'')
have neg : ∀ (a b : R) (hab : a ≤ b), r + (1 - r) * a ≤ r + (1 - r) * b
Tactic: refine hl''s.pairwise.map _ fun a b hab ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2) : (a : R) → P) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw.{u_1, u_2, u_4} R (P := P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
ht : ¬Eq.{u_4 + 1} (α := List P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P) ([] : List P)
hl'' :
  Eq.{u_4 + 1} (α := List P)
    (map (⇑(lineMap ((lineMap head (tail.getLast ht2) : (a : R) → P) r) (tail.getLast ht2) : R →ᵃ[R] P) : (a : R) → P)
        l'' :
      List P)
    ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
a b : R
hab : a ≤ b
⊢ r + (1 - r) * a ≤ r + (1 - r) * b
have neg : 0 ≤ 1 - r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2) : (a : R) → P) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw.{u_1, u_2, u_4} R (P := P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
ht : ¬Eq.{u_4 + 1} (α := List P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P) ([] : List P)
hl'' :
  Eq.{u_4 + 1} (α := List P)
    (map (⇑(lineMap ((lineMap head (tail.getLast ht2) : (a : R) → P) r) (tail.getLast ht2) : R →ᵃ[R] P) : (a : R) → P)
        l'' :
      List P)
    ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
⊢ map (α := R) (⇑(lineMap head (tail.getLast ht2)) : (a : R) → P) (0 :: map (fun (x : R) ↦ r + (1 - r) * x) l'') =
    head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail
have neg : ∀ a ∈ l'', head = tail.getLast ht2 ∨ r + (1 - r) * a = 1 - (1 - a) * (1 - r)
Tactic: simp only [map_cons, lineMap_apply_zero, map_map, ← hl'', cons.injEq,
                map_inj_left, Function.comp_apply, lineMap_lineMap_left, lineMap_eq_lineMap_iff,
                true_and]
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2) : (a : R) → P) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw.{u_1, u_2, u_4} R (P := P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
ht : ¬Eq.{u_4 + 1} (α := List P) ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P) ([] : List P)
hl'' :
  Eq.{u_4 + 1} (α := List P)
    (map (⇑(lineMap ((lineMap head (tail.getLast ht2) : (a : R) → P) r) (tail.getLast ht2) : R →ᵃ[R] P) : (a : R) → P)
        l'' :
      List P)
    ((lineMap head (tail.getLast ht2) : (a : R) → P) r :: tail : List P)
⊢ ∀ a ∈ l'', head = tail.getLast ht2 ∨ r + (1 - r) * a = 1 - (1 - a) * (1 - r)
have neg : ∀ a ∈ l'', head = tail.getLast ht2 ∨ True
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
tail : List P
hl : head :: tail ≠ []
h : Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail
ht : ¬tail = []
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
hl'' : map (⇑(lineMap (tail.head ht) (tail.getLast ht)) : (a : R) → P) l'' = tail
⊢ ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht)) : (a : R) → P) l' = head :: tail
have neg : ∀ (hl : [head] ≠ []) (h : Pairwise (Wbtw R head) [] ∧ List.Wbtw.{u_1, u_2, u_4} R (P := P) [])
  (ht : ¬Eq.{u_4 + 1} (α := List P) [] [])
  (hl'' : Eq.{u_4 + 1} (α := List P) (map (⇑(lineMap (List.head [] ht) (getLast [] ht)) : (a : R) → P) l'') []),
  ∃ (l' : List R), (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (getLast [] ht)) : (a : R) → P) l' = [head]
Tactic: cases tail with
        | nil => simp at ht
        | cons head2 tail =>
          by_cases ht2 : tail = []
          · exact ⟨[0, 1], by simp [ht2, sortedLE_iff_pairwise]⟩
          · simp only [head_cons, getLast_cons ht2] at hl'' ⊢
            rw [pairwise_cons] at h
            have hw := h.1.1 _ (getLast_mem ht2)
            rcases hw with ⟨r, ⟨hr0, hr1⟩, rfl⟩
            refine ⟨0 :: l''.map fun x ↦ r + (1 - r) * x, ?_, ?_, ?_⟩
            · simp only [mem_cons, mem_map, forall_eq_or_imp, le_refl, forall_exists_index,
                and_imp, forall_apply_eq_imp_iff₂, true_and]
              intro a ha
              have := hl''0 a ha
              nlinarith
            · simp only [sortedLE_iff_pairwise, pairwise_cons, mem_map,
                forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
              refine ⟨?_, ?_⟩
              · intro a ha
                have := hl''0 a ha
                nlinarith
              · refine hl''s.pairwise.map _ fun a b hab ↦ ?_
                gcongr
            · simp only [map_cons, lineMap_apply_zero, map_map, ← hl'', cons.injEq,
                map_inj_left, Function.comp_apply, lineMap_lineMap_left, lineMap_eq_lineMap_iff,
                true_and]
              ring_nf
              simp
Cleared hypotheses: tail, hl, h, ht, hl''
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
head : P
tail : List P
hl : head :: tail ≠ []
h : Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail
ht : ¬tail = []
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
hl'' : map (⇑(lineMap (tail.head ht) (tail.getLast ht)) : (a : R) → P) l'' = tail
neg :
  ∀ (hl : [head] ≠ []) (h : Pairwise (Wbtw R head) [] ∧ List.Wbtw.{u_1, u_2, u_4} R (P := P) [])
    (ht : ¬Eq.{u_4 + 1} (α := List P) [] [])
    (hl'' : Eq.{u_4 + 1} (α := List P) (map (⇑(lineMap (List.head [] ht) (getLast [] ht)) : (a : R) → P) l'') []),
    ∃ (l' : List R), (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (getLast [] ht)) : (a : R) → P) l' = [head]
⊢ ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht)) : (a : R) → P) l' = head :: tail
have neg₁ : ∀ (head2 : P) (tail : List P) (hl : head :: head2 :: tail ≠ [])
  (h : Pairwise (Wbtw R head) (head2 :: tail) ∧ List.Wbtw R (head2 :: tail)) (ht : ¬head2 :: tail = [])
  (hl'' : map (⇑(lineMap ((head2 :: tail).head ht) ((head2 :: tail).getLast ht)) : (a : R) → P) l'' = head2 :: tail),
  ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ map (⇑(lineMap head ((head2 :: tail).getLast ht)) : (a : R) → P) l' = head :: head2 :: tail
Tactic: cases tail with
        | nil => simp at ht
        | cons head2 tail =>
          by_cases ht2 : tail = []
          · exact ⟨[0, 1], by simp [ht2, sortedLE_iff_pairwise]⟩
          · simp only [head_cons, getLast_cons ht2] at hl'' ⊢
            rw [pairwise_cons] at h
            have hw := h.1.1 _ (getLast_mem ht2)
            rcases hw with ⟨r, ⟨hr0, hr1⟩, rfl⟩
            refine ⟨0 :: l''.map fun x ↦ r + (1 - r) * x, ?_, ?_, ?_⟩
            · simp only [mem_cons, mem_map, forall_eq_or_imp, le_refl, forall_exists_index,
                and_imp, forall_apply_eq_imp_iff₂, true_and]
              intro a ha
              have := hl''0 a ha
              nlinarith
            · simp only [sortedLE_iff_pairwise, pairwise_cons, mem_map,
                forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
              refine ⟨?_, ?_⟩
              · intro a ha
                have := hl''0 a ha
                nlinarith
              · refine hl''s.pairwise.map _ fun a b hab ↦ ?_
                gcongr
            · simp only [map_cons, lineMap_apply_zero, map_map, ← hl'', cons.injEq,
                map_inj_left, Function.comp_apply, lineMap_lineMap_left, lineMap_eq_lineMap_iff,
                true_and]
              ring_nf
              simp
Cleared hypotheses: tail, hl, h, ht, hl''
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (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
l : List P
hl : l ≠ []
h : List.Wbtw R l
⊢ ∃ (l' : List R), (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
have refine_2 : ∀ (hl : Ne.{u_4 + 1} (α := List P) [] []) (h : List.Wbtw.{u_1, u_2, u_4} R (P := P) []),
  ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ Eq.{u_4 + 1} (α := List P) (map (⇑(lineMap (head [] hl) (getLast [] hl)) : (a : R) → P) l') []
Tactic: induction l with
    | nil => simp at hl
    | cons head tail ih =>
      by_cases ht : tail = []
      · refine ⟨[0], ?_⟩
        simp [ht, sortedLE_iff_pairwise]
      · rw [wbtw_cons] at h
        replace ih := ih ht h.2
        rcases ih with ⟨l'', hl''0, hl''s, hl''⟩
        simp only [head_cons, getLast_cons ht]
        cases tail with
        | nil => simp at ht
        | cons head2 tail =>
          by_cases ht2 : tail = []
          · exact ⟨[0, 1], by simp [ht2, sortedLE_iff_pairwise]⟩
          · simp only [head_cons, getLast_cons ht2] at hl'' ⊢
            rw [pairwise_cons] at h
            have hw := h.1.1 _ (getLast_mem ht2)
            rcases hw with ⟨r, ⟨hr0, hr1⟩, rfl⟩
            refine ⟨0 :: l''.map fun x ↦ r + (1 - r) * x, ?_, ?_, ?_⟩
            · simp only [mem_cons, mem_map, forall_eq_or_imp, le_refl, forall_exists_index,
                and_imp, forall_apply_eq_imp_iff₂, true_and]
              intro a ha
              have := hl''0 a ha
              nlinarith
            · simp only [sortedLE_iff_pairwise, pairwise_cons, mem_map,
                forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
              refine ⟨?_, ?_⟩
              · intro a ha
                have := hl''0 a ha
                nlinarith
              · refine hl''s.pairwise.map _ fun a b hab ↦ ?_
                gcongr
            · simp only [map_cons, lineMap_apply_zero, map_map, ← hl'', cons.injEq,
                map_inj_left, Function.comp_apply, lineMap_lineMap_left, lineMap_eq_lineMap_iff,
                true_and]
              ring_nf
              simp
Cleared hypotheses: l, hl, h