awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head : R
tail : List R
h : (head :: tail).SortedLE
cons : ∀ (h : [head].SortedLE), Pairwise (Wbtw R head) []
⊢ Pairwise (Wbtw R head) tail
have cons₁ : ∀ (head' : R) (tail' : List R) (ih : ∀ (h : (head :: tail').SortedLE), Pairwise (Wbtw R head) tail')
  (h : (head :: head' :: tail').SortedLE), Pairwise (Wbtw R head) (head' :: tail')
Tactic: induction tail with
    | nil => simp
    | cons head' tail' ih =>
      rw [pairwise_cons]
      refine ⟨?_, ih (h.pairwise.sublist ?_).sortedLE⟩
      · simp_rw [sortedLE_iff_pairwise, pairwise_cons_cons, pairwise_cons] at h
        exact fun a ha ↦ .of_le_of_le h.1 (h.2.2.1 a ha)
      · simp
Cleared hypotheses: tail, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
l : List R
h : l.SortedLE
⊢ List.Wbtw R l
have nil : ∀ (h : SortedLE.{u_1} (α := R) []), List.Wbtw R (P := R) []
Tactic: induction l with
  | nil => simp
  | cons head tail ih =>
    rw [wbtw_cons]
    refine ⟨?_, ih h.pairwise.of_cons.sortedLE⟩
    clear ih
    induction tail with
    | nil => simp
    | cons head' tail' ih =>
      rw [pairwise_cons]
      refine ⟨?_, ih (h.pairwise.sublist ?_).sortedLE⟩
      · simp_rw [sortedLE_iff_pairwise, pairwise_cons_cons, pairwise_cons] at h
        exact fun a ha ↦ .of_le_of_le h.1 (h.2.2.1 a ha)
      · simp
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
l : List R
h : l.SortedLE
nil : ∀ (h : SortedLE.{u_1} (α := R) []), List.Wbtw R (P := R) []
⊢ List.Wbtw R l
have cons : ∀ (head : R) (tail : List R) (ih : ∀ (h : tail.SortedLE), List.Wbtw R tail) (h : (head :: tail).SortedLE),
  List.Wbtw R (head :: tail)
Tactic: induction l with
  | nil => simp
  | cons head tail ih =>
    rw [wbtw_cons]
    refine ⟨?_, ih h.pairwise.of_cons.sortedLE⟩
    clear ih
    induction tail with
    | nil => simp
    | cons head' tail' ih =>
      rw [pairwise_cons]
      refine ⟨?_, ih (h.pairwise.sublist ?_).sortedLE⟩
      · simp_rw [sortedLE_iff_pairwise, pairwise_cons_cons, pairwise_cons] at h
        exact fun a ha ↦ .of_le_of_le h.1 (h.2.2.1 a ha)
      · simp
Cleared hypotheses: l, h
-- 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 ≠ []
⊢ (∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l) ↔ List.Wbtw R l
have refine_1 : (∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l) →
  ∀ (l' : List R) (hl's : l'.SortedLE) (hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l),
    List.Wbtw R l
Tactic: refine ⟨fun ⟨l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩
-- 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 ≠ []
refine_1 :
  (∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l) →
    ∀ (l' : List R) (hl's : l'.SortedLE) (hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l),
      List.Wbtw R l
⊢ (∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l) ↔ List.Wbtw R l
have refine_2 : ∀ (h : List.Wbtw R l), ∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
Tactic: refine ⟨fun ⟨l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩
-- 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 : ∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
⊢ List.Wbtw R l
have refine_1 : List.Wbtw.{u_1, u_2, u_4} R (P := P) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')
Tactic: rw [← hl'l]
-- 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
this :
  ∃ (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
have 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
Tactic: rcases this with ⟨l', -, hl'⟩
Cleared hypotheses: this
-- 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), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
have refine_2 : ∃ (l' : List R), (∀ a ∈ l', 0 ≤ a) ∧ 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'⟩
-- 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
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
have 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
Tactic: by_cases ht : tail = []
-- 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
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
⊢ ∃ (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
have 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
Tactic: by_cases ht : tail = []
-- 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
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
have 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
Tactic: refine ⟨[0], ?_⟩
-- 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
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
have h₁ : Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail
Tactic: rw [wbtw_cons] at h
Cleared hypotheses: h, ht
-- 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
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 ((head :: tail).head hl) ((head :: tail).getLast hl)) : (a : R) → P) l' = head :: tail
have ih₁ : ∃ (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
Cleared hypotheses: ih
-- 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 = []
ih :
  ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ 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
have 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
Tactic: rcases ih with ⟨l'', hl''0, hl''s, hl''⟩
Cleared hypotheses: ih
-- 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).head hl) ((head :: tail).getLast hl)) : (a : R) → P) l' = head :: tail
have neg : ∃ (l' : List R),
  (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht)) : (a : R) → P) l' = head :: tail
Tactic: simp only [head_cons, getLast_cons ht]
-- 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
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
have 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
Tactic: by_cases ht2 : tail = []
-- 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
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
⊢ ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ map (⇑(lineMap head ((head2 :: tail).getLast ht)) : (a : R) → P) l' = head :: head2 :: tail
have 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
Tactic: by_cases ht2 : tail = []
-- 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
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
have 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
Tactic: simp only [head_cons, getLast_cons ht2] at hl'' ⊢
Cleared hypotheses: 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
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
⊢ ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht2)) : (a : R) → P) l' = head :: head2 :: tail
have 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
Tactic: rw [pairwise_cons] at h
Cleared hypotheses: h, ht, ht2, hl''
-- 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
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
⊢ ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht2)) : (a : R) → P) l' = head :: head2 :: tail
have hw : Wbtw R head head2 (tail.getLast ht2)
Tactic: have hw := h.1.1 _ (getLast_mem ht2)
-- 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
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)
⊢ ∃ (l' : List R),
    (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht2)) : (a : R) → P) l' = head :: head2 :: tail
have 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
Tactic: rcases hw with ⟨r, ⟨hr0, hr1⟩, rfl⟩
Cleared hypotheses: head2, hl, h, ht, hl'', hw
-- 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)
⊢ ∃ (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 : ∀ (a : R), Membership.mem (γ := List R) (0 :: map (fun (x : R) ↦ r + (1 - r) * x) l'') a → 0 ≤ a
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)
neg : ∀ (a : R), Membership.mem (γ := List R) (0 :: map (fun (x : R) ↦ r + (1 - r) * x) l'') a → 0 ≤ a
⊢ ∃ (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₁ : SortedLE (α := R) (0 :: map (fun (x : R) ↦ r + (1 - r) * x) l'')
Tactic: refine ⟨0 :: l''.map fun x ↦ r + (1 - r) * x, ?_, ?_, ?_⟩