awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.BetweenList
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
nlinarith : r + (1 - r) * a < 0 → 0 - r + (r + (1 - r) * a - 0) + (0 - (r - 1) * (0 - a)) = 0
⊢ 0 ≤ r + (1 - r) * a

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Convex.BetweenList
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) ∧ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) (map (fun (x : R) ↦ r + (1 - r) * x) l'')
⊢ SortedLE (α := R) (0 :: 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₂]

Premises used: and_imp, forall_exists_index, List.sortedLE_iff_pairwise, List.pairwise_cons, List.mem_map, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Analysis.Convex.BetweenList
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'')

Tactic:
⟨?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.Convex.BetweenList
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
neg₁ : Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) (map (fun (x : R) ↦ r + (1 - r) * x) l'')
⊢ (∀ a ∈ l'', 0 ≤ r + (1 - r) * a) ∧ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) (map (fun (x : R) ↦ r + (1 - r) * x) l'')

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
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'')

Tactic:
hl''s.pairwise.map _ fun a b hab ↦ ?_

Premises used: List.SortedLE.pairwise, List.Pairwise.map
-- Module: Mathlib.Analysis.Convex.BetweenList
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 b : R) (hab : a ≤ b), r + (1 - r) * a ≤ r + (1 - r) * b
⊢ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) (map (fun (x : R) ↦ r + (1 - r) * x) l'')

Tactic:
refine hl''s.pairwise.map _ fun a b hab ↦ ?_

Premises used: List.SortedLE.pairwise, List.Pairwise.map
-- Module: Mathlib.Analysis.Convex.BetweenList
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
neg : 0 ≤ 1 - r
⊢ r + (1 - r) * a ≤ r + (1 - r) * b

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.BetweenList
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'', head = tail.getLast ht2 ∨ r + (1 - r) * a = 1 - (1 - a) * (1 - r)
⊢ 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:
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]

Premises used: List.map_inj_left, List.map_cons, List.map_map, AffineMap.lineMap_eq_lineMap_iff, AffineMap.lineMap_apply_zero, List.cons.injEq, AffineMap.lineMap_lineMap_left, Function.comp_apply, true_and
-- Module: Mathlib.Analysis.Convex.BetweenList
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'', head = tail.getLast ht2 ∨ True
⊢ ∀ a ∈ l'', head = tail.getLast ht2 ∨ r + (1 - r) * a = 1 - (1 - a) * (1 - r)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Convex.BetweenList
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 ∨ True

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.BetweenList
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]
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
⊢ ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht)) : (a : R) → P) l' = head :: 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

Premises used: le_refl, List.map_inj_left, List.map_cons, and_imp, forall_exists_index, List.head_cons, List.SortedLE.pairwise, List.sortedLE_iff_pairwise, List.map_map, forall_eq_or_imp, AffineMap.lineMap_eq_lineMap_iff, AffineMap.lineMap_apply_zero, List.cons, List.cons.injEq, List.pairwise_cons, AffineMap.lineMap_lineMap_left, List.Pairwise.map, Function.comp_apply, List.mem_cons, List.mem_map, forall_apply_eq_imp_iff₂, rfl, true_and, List.nil
-- Module: Mathlib.Analysis.Convex.BetweenList
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
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') []
refine_2₁ :
  ∀ (head : P) (tail : List P)
    (ih :
      ∀ (hl : tail ≠ []) (h : List.Wbtw R tail),
        ∃ (l' : List R),
          (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head hl) (tail.getLast hl)) : (a : R) → P) l' = tail)
    (hl : head :: tail ≠ []) (h : List.Wbtw R (head :: tail)),
    ∃ (l' : List R),
      (∀ a ∈ l', 0 ≤ a) ∧
        l'.SortedLE ∧
          map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl)) : (a : R) → P) l' = head :: tail
⊢ ∃ (l' : List R), (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = 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

Premises used: List.head, le_refl, List.map_inj_left, List.map_cons, and_imp, forall_exists_index, List.head_cons, List.sortedLE_iff_pairwise, List.map_map, forall_eq_or_imp, List.wbtw_cons, AffineMap.lineMap_eq_lineMap_iff, List.tail, AffineMap.lineMap_apply_zero, List.cons, List.cons.injEq, List.pairwise_cons, AffineMap.lineMap_lineMap_left, Function.comp_apply, List.mem_cons, List.mem_map, forall_apply_eq_imp_iff₂, rfl, true_and, List.nil
-- Module: Mathlib.Analysis.Convex.BetweenList
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
⊢ (∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l) ↔ List.Wbtw R l

Tactic:
⟨fun ⟨p₁, p₂, l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro, List.Wbtw, _private.0.List.exists_map_eq_of_sorted_iff_wbtw.match_1
-- Module: Mathlib.Analysis.Convex.BetweenList
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
refine_1 :
  (∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l) →
    ∀ (p₁ p₂ : P) (l' : List R) (hl's : l'.SortedLE) (hl'l : map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l), List.Wbtw R l
refine_2 :
  ∀ (h : List.Wbtw R l), ∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
⊢ (∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l) ↔ List.Wbtw R l

Tactic:
refine ⟨fun ⟨p₁, p₂, l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
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
h : ∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
p₁ p₂ : P
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
refine_1 :
  (∃ (p₁_1 : P) (p₂_1 : P) (l'_1 : List R),
      l'_1.SortedLE ∧
        Eq.{u_4 + 1} (α := List P) (map (⇑(lineMap p₁_1 p₂_1) : (a : R) → P) l'_1)
          (map (⇑(lineMap p₁ p₂) : (a : R) → P) l')) →
    List.Wbtw.{u_1, u_2, u_4} R (P := P) (map (⇑(lineMap p₁ p₂) : (a : R) → P) l')
⊢ List.Wbtw R l

Tactic:
subst hl'l
-- Module: Mathlib.Analysis.Convex.BetweenList
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
p₁ p₂ : P
l' : List R
hl's : l'.SortedLE
h :
  ∃ (p₁_1 : P) (p₂_1 : P) (l'_1 : List R),
    l'_1.SortedLE ∧
      Eq.{u_4 + 1} (α := List P) (map (⇑(lineMap p₁_1 p₂_1) : (a : R) → P) l'_1)
        (map (⇑(lineMap p₁ p₂) : (a : R) → P) l')
⊢ List.Wbtw.{u_1, u_2, u_4} R (P := P) (map (⇑(lineMap p₁ p₂) : (a : R) → P) l')

Tactic:
Wbtw.map hl's.wbtw _

Premises used: List.SortedLE.wbtw, List.Wbtw.map
-- Module: Mathlib.Analysis.Convex.BetweenList
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
p₁ p₂ : P
l' : List R
hl's : l'.SortedLE
h :
  ∃ (p₁_1 : P) (p₂_1 : P) (l'_1 : List R),
    l'_1.SortedLE ∧
      Eq.{u_4 + 1} (α := List P) (map (⇑(lineMap p₁_1 p₂_1) : (a : R) → P) l'_1)
        (map (⇑(lineMap p₁ p₂) : (a : R) → P) l')
⊢ List.Wbtw.{u_1, u_2, u_4} R (P := P) (map (⇑(lineMap p₁ p₂) : (a : R) → P) l')

Tactic:
exact Wbtw.map hl's.wbtw _

Premises used: List.SortedLE.wbtw, List.Wbtw.map
-- Module: Mathlib.Analysis.Convex.BetweenList
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
h : List.Wbtw R l
pos : ∀ (hl : l = []), ∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
neg : ∀ (hl : ¬l = []), ∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
⊢ ∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l

Tactic:
by_cases hl : l = []
-- Module: Mathlib.Analysis.Convex.BetweenList
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
h : List.Wbtw R l
hl : l = []
⊢ SortedLE.{u_1} (α := R) [] ∧
    map.{u_1, u_4} (α := R) (⇑(lineMap (Nonempty.some ⋯) (Nonempty.some ⋯)) : (a : R) → P) [] = l

Tactic:
simp [hl, sortedLE_iff_pairwise]

Premises used: List.sortedLE_iff_pairwise
-- Module: Mathlib.Analysis.Convex.BetweenList
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
h : List.Wbtw R l
hl : l = []
⊢ ∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l

Tactic:
exact ⟨AddTorsor.nonempty.some, AddTorsor.nonempty.some, [], by
        simp [hl, sortedLE_iff_pairwise]⟩