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
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') []
⊢ ∃ (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₁ : ∀ (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
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
-- 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
⊢ (∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l) ↔ List.Wbtw R l
have 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
Tactic: refine ⟨fun ⟨p₁, p₂, 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
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
⊢ (∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l) ↔ List.Wbtw R l
have 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
Tactic: refine ⟨fun ⟨p₁, p₂, 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
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
⊢ List.Wbtw R l
have 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')
Tactic: subst hl'l
Cleared hypotheses: l, h, 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
h : List.Wbtw R l
⊢ ∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
have pos : ∀ (hl : l = []), ∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
Tactic: by_cases 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
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
⊢ ∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
have neg : ∀ (hl : ¬l = []), ∃ (p₁ : P) (p₂ : P) (l' : List R), l'.SortedLE ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
Tactic: by_cases 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 ≠ []
⊢ (∃ (l' : List R),
      l'.SortedLT ∧
        map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)) ↔
    List.Sbtw R l
have refine_1 : (∃ (l' : List R),
    l'.SortedLT ∧
      map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)) →
  ∀ (l' : List R) (hl's : l'.SortedLT) (hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l)
    (hla : l.length = 1 ∨ l.head hl ≠ l.getLast hl), Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
Tactic: refine ⟨fun ⟨l', hl's, hl'l, hla⟩ ↦
            ⟨(exists_map_eq_of_sorted_nonempty_iff_wbtw hl).1
            ⟨l', (hl's.pairwise.imp LT.lt.le).sortedLE, 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'.SortedLT ∧
        map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)) →
    ∀ (l' : List R) (hl's : l'.SortedLT) (hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l)
      (hla : l.length = 1 ∨ l.head hl ≠ l.getLast hl), Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
⊢ (∃ (l' : List R),
      l'.SortedLT ∧
        map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)) ↔
    List.Sbtw R l
have refine_2 : ∀ (h : List.Sbtw R l),
  ∃ (l' : List R),
    l'.SortedLT ∧
      map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
Tactic: refine ⟨fun ⟨l', hl's, hl'l, hla⟩ ↦
            ⟨(exists_map_eq_of_sorted_nonempty_iff_wbtw hl).1
            ⟨l', (hl's.pairwise.imp LT.lt.le).sortedLE, 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'.SortedLT ∧
      map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
hla : l.length = 1 ∨ l.head hl ≠ l.getLast hl
⊢ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
have refine_1 : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (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 :
  ∃ (l' : List R),
    l'.SortedLT ∧
      map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
hla : l.length = 1 ∨ l.head hl ≠ l.getLast hl
⊢ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')
have refine_1 : ∀ (hla : l.length = 1),
  Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')
Tactic: rcases hla with hla | hla
Cleared hypotheses: hla
-- 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'.SortedLT ∧
      map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
hla : l.length = 1 ∨ l.head hl ≠ l.getLast hl
refine_1 :
  ∀ (hla : l.length = 1),
    Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')
⊢ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')
have refine_1₁ : ∀ (hla : l.head hl ≠ l.getLast hl),
  Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')
Tactic: rcases hla with hla | hla
Cleared hypotheses: hla
-- 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
l : List P
hl : l ≠ []
h : List.Sbtw R l
⊢ ∃ (l' : List R),
    l'.SortedLT ∧
      map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
have h₁ : (∃ (l' : List R), l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l) ∧
  Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
Tactic: rw [List.Sbtw, ← exists_map_eq_of_sorted_nonempty_iff_wbtw hl] at h
Cleared hypotheses: 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) ∧
    Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
⊢ ∃ (l' : List R),
    l'.SortedLT ∧
      map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
have refine_2 : ∀ (hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l) (l' : List R) (hl's : l'.SortedLE)
  (hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l),
  ∃ (l' : List R),
    l'.SortedLT ∧
      map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
Tactic: rcases h with ⟨⟨l', hl's, hl'l⟩, hp⟩
Cleared hypotheses: 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 ≠ []
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
⊢ ∃ (l' : List R),
    l'.SortedLT ∧
      map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
have refine_2 : l'.SortedLT
Tactic: refine ⟨l', ?_, 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 ≠ []
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
refine_2 : l'.SortedLT
⊢ ∃ (l' : List R),
    l'.SortedLT ∧
      map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
have refine_2₁ : l.length = 1 ∨ l.head hl ≠ l.getLast hl
Tactic: refine ⟨l', ?_, hl'l, ?_⟩
-- 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
l : List P
hl : l ≠ []
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
⊢ l'.SortedLT
have hp₁ : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')
Tactic: rw [← hl'l] at hp
Cleared hypotheses: hp, hl's, hl'l
-- 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
l : List P
hl : l ≠ []
l' : List R
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
⊢ l'.SortedLT
have hp' : Pairwise (fun (x1 x2 : R) ↦ x1 ≠ x2) l'
Tactic: have hp' : l'.Pairwise (· ≠ ·) := hp.of_map _ (by simp)
-- 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 R
hl's : l'.SortedLE
head : P
tail : List P
hl : head :: tail ≠ []
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
hl'l : map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl)) : (a : R) → P) l' = head :: tail
⊢ (head :: tail).length = 1 ∨ (head :: tail).head hl ≠ (head :: tail).getLast hl
have refine_2 : tail = [] ∨ head ≠ (head :: tail).getLast hl
Tactic: simp only [length_cons, add_eq_right, length_eq_zero_iff, head_cons]
-- 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 R
hl's : l'.SortedLE
head head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: head2 :: tail)
hl'l :
  map (⇑(lineMap ((head :: head2 :: tail).head hl) ((head :: head2 :: tail).getLast hl)) : (a : R) → P) l' =
    head :: head2 :: tail
⊢ head2 :: tail = [] ∨ head ≠ (head :: head2 :: tail).getLast hl
have refine_2 : head ≠ (head :: head2 :: tail).getLast hl
Tactic: simp only [reduceCtorEq, false_or]
-- 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
l' : List R
hl's : l'.SortedLE
head head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: head2 :: tail)
hl'l :
  map (⇑(lineMap ((head :: head2 :: tail).head hl) ((head :: head2 :: tail).getLast hl)) : (a : R) → P) l' =
    head :: head2 :: tail
⊢ head ≠ (head :: head2 :: tail).getLast hl
have hp₁ : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail)
Tactic: rw [pairwise_cons] at hp
Cleared hypotheses: hp, 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 R
hl's : l'.SortedLE
head head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
hp : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail)
hl'l :
  map (⇑(lineMap ((head :: head2 :: tail).head hl) ((head :: head2 :: tail).getLast hl)) : (a : R) → P) l' =
    head :: head2 :: tail
⊢ head ≠ (head :: head2 :: tail).getLast hl
have refine_2 : (head :: head2 :: tail).getLast hl ∈ head2 :: tail
Tactic: refine hp.1 ((head :: head2 :: tail).getLast 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 R
hl's : l'.SortedLE
head : P
tail : List P
hl : head :: tail ≠ []
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
hl'l : map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl)) : (a : R) → P) l' = head :: tail
⊢ tail = [] ∨ head ≠ (head :: tail).getLast hl
have refine_2 : ∀ (hl : [head] ≠ []) (hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) [head])
  (hl'l : map (⇑(lineMap ([head].head hl) ([head].getLast hl)) : (a : R) → P) l' = [head]),
  Eq.{u_4 + 1} (α := List P) [] [] ∨ head ≠ [head].getLast hl
Tactic: cases tail with
        | nil => simp
        | cons head2 tail =>
          simp only [reduceCtorEq, false_or]
          rw [pairwise_cons] at hp
          refine hp.1 ((head :: head2 :: tail).getLast hl) ?_
          simp
Cleared hypotheses: tail, hl, hp, 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 R
hl's : l'.SortedLE
head : P
tail : List P
hl : head :: tail ≠ []
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
hl'l : map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl)) : (a : R) → P) l' = head :: tail
refine_2 :
  ∀ (hl : [head] ≠ []) (hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) [head])
    (hl'l : map (⇑(lineMap ([head].head hl) ([head].getLast hl)) : (a : R) → P) l' = [head]),
    Eq.{u_4 + 1} (α := List P) [] [] ∨ head ≠ [head].getLast hl
⊢ tail = [] ∨ head ≠ (head :: tail).getLast hl
have refine_2₁ : ∀ (head2 : P) (tail : List P) (hl : head :: head2 :: tail ≠ [])
  (hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: head2 :: tail))
  (hl'l :
    map (⇑(lineMap ((head :: head2 :: tail).head hl) ((head :: head2 :: tail).getLast hl)) : (a : R) → P) l' =
      head :: head2 :: tail),
  head2 :: tail = [] ∨ head ≠ (head :: head2 :: tail).getLast hl
Tactic: cases tail with
        | nil => simp
        | cons head2 tail =>
          simp only [reduceCtorEq, false_or]
          rw [pairwise_cons] at hp
          refine hp.1 ((head :: head2 :: tail).getLast hl) ?_
          simp
Cleared hypotheses: tail, hl, hp, 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 ≠ []
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
⊢ l.length = 1 ∨ l.head hl ≠ l.getLast hl
have refine_2 : ∀ (hl : Ne.{u_4 + 1} (α := List P) [] []) (hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) [])
  (hl'l : Eq.{u_4 + 1} (α := List P) (map (⇑(lineMap (head [] hl) (getLast [] hl)) : (a : R) → P) l') []),
  length.{u_4} (α := P) [] = 1 ∨ head [] hl ≠ getLast [] hl
Tactic: cases l with
      | nil => simp at hl
      | cons head tail =>
        simp only [length_cons, add_eq_right, length_eq_zero_iff, head_cons]
        cases tail with
        | nil => simp
        | cons head2 tail =>
          simp only [reduceCtorEq, false_or]
          rw [pairwise_cons] at hp
          refine hp.1 ((head :: head2 :: tail).getLast hl) ?_
          simp
Cleared hypotheses: l, hl, hp, 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 ≠ []
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
refine_2 :
  ∀ (hl : Ne.{u_4 + 1} (α := List P) [] []) (hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) [])
    (hl'l : Eq.{u_4 + 1} (α := List P) (map (⇑(lineMap (head [] hl) (getLast [] hl)) : (a : R) → P) l') []),
    length.{u_4} (α := P) [] = 1 ∨ head [] hl ≠ getLast [] hl
⊢ l.length = 1 ∨ l.head hl ≠ l.getLast hl
have refine_2₁ : ∀ (head : P) (tail : List P) (hl : head :: tail ≠ []) (hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail))
  (hl'l : map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl)) : (a : R) → P) l' = head :: tail),
  (head :: tail).length = 1 ∨ (head :: tail).head hl ≠ (head :: tail).getLast hl
Tactic: cases l with
      | nil => simp at hl
      | cons head tail =>
        simp only [length_cons, add_eq_right, length_eq_zero_iff, head_cons]
        cases tail with
        | nil => simp
        | cons head2 tail =>
          simp only [reduceCtorEq, false_or]
          rw [pairwise_cons] at hp
          refine hp.1 ((head :: head2 :: tail).getLast hl) ?_
          simp
Cleared hypotheses: l, hl, hp, 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
inst_6 : Nontrivial P
l : List P
⊢ (∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l) ↔
    List.Sbtw R l
have refine_1 : (∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l) →
  ∀ (p₁ p₂ : P) (hp₁p₂ : p₁ ≠ p₂) (l' : List R) (hl's : l'.SortedLT)
    (hl'l : map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l), List.Sbtw R l
Tactic: refine ⟨fun ⟨p₁, p₂, hp₁p₂, l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩