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
l : List P
hl : l ≠ []
h : List.Wbtw R l
this :
  ∃ (l' : List R), (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
rcases :
  ∀ (l' : List R) (hl' : l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l),
    ∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
⊢ ∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l

Tactic:
rcases this with ⟨l', -, hl'⟩
-- 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
l' : List R
hl' : l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
⊢ ∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l

Tactic:
⟨l', hl'⟩

Premises used: Exists.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
l : List P
hl : l ≠ []
h : List.Wbtw R l
l' : List R
hl' : l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
⊢ ∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l

Tactic:
exact ⟨l', hl'⟩
-- 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 :
  ∃ (l' : List R), (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
⊢ ∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l

Tactic:
suffices ∃ l' : List R, (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧
        l'.map (lineMap (l.head hl) (l.getLast hl)) = l by
      rcases this with ⟨l', -, hl'⟩
      exact ⟨l', hl'⟩
-- 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
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:
simp at hl
-- 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
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)
pos :
  ∀ (ht : 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
neg :
  ∀ (ht : ¬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 ((head :: tail).head hl) ((head :: tail).getLast hl)) : (a : R) → P) l' = head :: tail

Tactic:
by_cases ht : tail = []
-- 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
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)
ht : 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

Tactic:
⟨[0], ?_⟩

Premises used: List.cons, Exists.intro, OfNat.ofNat, 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
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)
ht : tail = []
pos :
  (∀ (a : R), Membership.mem (γ := List R) [0] a → 0 ≤ a) ∧
    SortedLE.{u_1} (α := R) [0] ∧
      map.{u_1, u_4} (α := R) (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl)) : (a : R) → P) [0] =
        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

Tactic:
refine ⟨[0], ?_⟩
-- 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
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)
ht : tail = []
⊢ (∀ (a : R), Membership.mem (γ := List R) [0] a → 0 ≤ a) ∧
    SortedLE.{u_1} (α := R) [0] ∧
      map.{u_1, u_4} (α := R) (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl)) : (a : R) → P) [0] =
        head :: tail

Tactic:
simp [ht, 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
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)
ht : ¬tail = []
⊢ Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail

Tactic:
rw [wbtw_cons] at h

Premises used: List.wbtw_cons
-- 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
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)
ht : ¬tail = []
h₁ : Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail
⊢ ¬tail = []

Tactic:
rw [wbtw_cons] at h

Premises used: List.wbtw_cons
-- 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
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 : Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail
ht : ¬tail = []
⊢ ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head ht) (tail.getLast ht)) : (a : R) → P) l' = tail

Tactic:
replace ih := ih ht h.2
-- 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 = []
ih :
  ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head ht) (tail.getLast ht)) : (a : R) → P) l' = tail
neg :
  ∀ (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).head hl) ((head :: tail).getLast hl)) : (a : R) → P) l' = 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

Tactic:
rcases ih with ⟨l'', hl''0, hl''s, hl''⟩
-- 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 :
  ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht)) : (a : R) → P) l' = 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

Tactic:
simp only [head_cons, getLast_cons ht]

Premises used: List.head_cons, List.getLast_cons
-- 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
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:
simp at ht
-- 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
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
pos :
  ∀ (ht2 : tail = []),
    ∃ (l' : List R),
      (∀ a ∈ l', 0 ≤ a) ∧
        l'.SortedLE ∧ map (⇑(lineMap head ((head2 :: tail).getLast ht)) : (a : R) → P) l' = head :: head2 :: tail
neg :
  ∀ (ht2 : ¬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 ((head2 :: tail).getLast ht)) : (a : R) → P) l' = head :: head2 :: tail

Tactic:
by_cases ht2 : tail = []
-- 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
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
ht2 : tail = []
⊢ (∀ (a : R), Membership.mem (γ := List R) [0, 1] a → 0 ≤ a) ∧
    SortedLE.{u_1} (α := R) [0, 1] ∧
      map.{u_1, u_4} (α := R) (⇑(lineMap head ((head2 :: tail).getLast ht)) : (a : R) → P) [0, 1] =
        head :: head2 :: tail

Tactic:
simp [ht2, 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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
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
ht2 : 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:
exact ⟨[0, 1], by simp [ht2, 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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
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
ht2 : ¬tail = []
neg :
  ∀ (hl'' : map (⇑(lineMap head2 (tail.getLast ht2)) : (a : R) → P) l'' = head2 :: tail),
    ∃ (l' : List R),
      (∀ a ∈ l', 0 ≤ a) ∧
        l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht2)) : (a : R) → P) l' = head :: 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:
simp only [head_cons, getLast_cons ht2] at hl'' ⊢

Premises used: List.head_cons, List.getLast_cons
-- 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
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : Pairwise (Wbtw R head) (head2 :: tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
ht2 : ¬tail = []
hl'' : map (⇑(lineMap head2 (tail.getLast ht2)) : (a : R) → P) l'' = head2 :: tail
neg :
  ∀ (h : ((∀ a' ∈ tail, Wbtw R head head2 a') ∧ Pairwise (Wbtw R head) tail) ∧ List.Wbtw R (head2 :: tail))
    (ht : ¬head2 :: tail = []) (ht2 : ¬tail = [])
    (hl'' : map (⇑(lineMap head2 (tail.getLast ht2)) : (a : R) → P) l'' = head2 :: tail),
    ∃ (l' : List R),
      (∀ a ∈ l', 0 ≤ a) ∧
        l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht2)) : (a : R) → P) l' = head :: head2 :: tail
⊢ ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht2)) : (a : R) → P) l' = head :: head2 :: tail

Tactic:
rw [pairwise_cons] at h

Premises used: List.pairwise_cons
-- 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
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : ((∀ a' ∈ tail, Wbtw R head head2 a') ∧ Pairwise (Wbtw R head) tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
ht2 : ¬tail = []
hl'' : map (⇑(lineMap head2 (tail.getLast ht2)) : (a : R) → P) l'' = head2 :: tail
⊢ Wbtw R head head2 (tail.getLast ht2)

Tactic:
have hw := h.1.1 _ (getLast_mem ht2)
-- 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
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : ((∀ a' ∈ tail, Wbtw R head head2 a') ∧ Pairwise (Wbtw R head) tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
ht2 : ¬tail = []
hl'' : map (⇑(lineMap head2 (tail.getLast ht2)) : (a : R) → P) l'' = head2 :: tail
hw : Wbtw R head head2 (tail.getLast ht2)
neg :
  ∀ (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)),
    ∃ (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
⊢ ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht2)) : (a : R) → P) l' = head :: head2 :: tail

Tactic:
rcases hw with ⟨r, ⟨hr0, hr1⟩, rfl⟩

Premises used: rfl
-- 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)
⊢ ∃ (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

Tactic:
⟨0 :: l''.map fun x ↦ r + (1 - r) * x, ?_, ?_, ?_⟩

Premises used: HMul.hMul, List.map, HSub.hSub, List.cons, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- 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 : 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'')
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
⊢ ∃ (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

Tactic:
refine ⟨0 :: l''.map fun x ↦ r + (1 - r) * x, ?_, ?_, ?_⟩
-- 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
⊢ ∀ (a : R), Membership.mem (γ := List R) (0 :: map (fun (x : R) ↦ r + (1 - r) * x) l'') a → 0 ≤ 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]

Premises used: le_refl, and_imp, forall_exists_index, forall_eq_or_imp, List.mem_cons, List.mem_map, forall_apply_eq_imp_iff₂, 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)
a : R
ha : a ∈ l''
⊢ 0 ≤ a

Tactic:
have := hl''0 a ha