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
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:
⟨l.head hl, l.getLast hl, (exists_map_eq_of_sorted_nonempty_iff_wbtw hl).2 h⟩

Premises used: List.head, Iff.mpr, List.getLast, List.exists_map_eq_of_sorted_nonempty_iff_wbtw, 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
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 ⟨l.head hl, l.getLast hl, (exists_map_eq_of_sorted_nonempty_iff_wbtw hl).2 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
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

Tactic:
⟨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 ↦ ?_⟩

Premises used: _private.0.List.exists_map_eq_of_sorted_nonempty_iff_sbtw.match_1, List.SortedLT.pairwise, List.Sbtw, LT.lt.le, List.exists_map_eq_of_sorted_nonempty_iff_wbtw, And.intro, Iff.intro, Exists.intro, Iff.mp, List.Pairwise.sortedLE, List.Pairwise.imp
-- 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 ≠ []
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
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)
⊢ (∃ (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

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 ↦ ?_⟩
-- 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 :
  ∃ (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 : 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) l

Tactic:
rw [← 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
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')
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')
⊢ 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
-- 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 :
  ∃ (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
⊢ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')

Tactic:
grind [List.pairwise_iff_forall_sublist]

Premises used: List.pairwise_iff_forall_sublist
-- 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 :
  ∃ (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.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:
(hl's.pairwise.imp LT.lt.ne).map _ fun _ _ ↦ (lineMap_injective _ hla).ne

Premises used: List.SortedLT.pairwise, AffineMap.lineMap_injective, Function.Injective.ne, List.Pairwise.map, List.Pairwise.imp, LT.lt.ne
-- 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 :
  ∃ (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.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:
exact (hl's.pairwise.imp LT.lt.ne).map _ fun _ _ ↦ (lineMap_injective _ hla).ne

Premises used: AffineMap.lineMap_injective, Function.Injective.ne, 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
l : List P
hl : l ≠ []
h : List.Sbtw R l
⊢ (∃ (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

Premises used: List.Sbtw, List.exists_map_eq_of_sorted_nonempty_iff_wbtw
-- 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 :
  (∃ (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
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)
⊢ ∃ (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⟩
-- 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 ≠ []
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:
⟨l', ?_, hl'l, ?_⟩

Premises used: And.intro, 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 ≠ []
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
refine_2₁ : l.length = 1 ∨ l.head hl ≠ l.getLast hl
⊢ ∃ (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 ⟨l', ?_, 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
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
⊢ 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
-- 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 ≠ []
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
hp₁ : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')
⊢ l'.SortedLE

Tactic:
rw [← hl'l] at hp
-- 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 ≠ []
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
hp₁ : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')
hl's₁ : l'.SortedLE
⊢ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l

Tactic:
rw [← hl'l] at hp
-- 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 ≠ []
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
⊢ ∀ (a b : R),
    Ne.{u_4 + 1} (α := P) ((lineMap (l.head hl) (l.getLast hl) : (a : R) → P) a : P)
        ((lineMap (l.head hl) (l.getLast hl) : (a : R) → P) b : P) →
      a ≠ b

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
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
⊢ Pairwise (fun (x1 x2 : R) ↦ x1 ≠ x2) l'

Tactic:
have hp' : l'.Pairwise (· ≠ ·) := hp.of_map _ (by 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
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
hp' : Pairwise (fun (x1 x2 : R) ↦ x1 ≠ x2) l'
⊢ l'.SortedLT

Tactic:
((pairwise_and_iff.2 ⟨hl's.pairwise, hp'⟩).imp lt_iff_le_and_ne.2).sortedLT

Premises used: Iff.mpr, lt_iff_le_and_ne, List.SortedLE.pairwise, List.pairwise_and_iff, And.intro, List.Pairwise.sortedLT, List.Pairwise.imp
-- 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 ≠ []
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
hp' : Pairwise (fun (x1 x2 : R) ↦ x1 ≠ x2) l'
⊢ l'.SortedLT

Tactic:
exact ((pairwise_and_iff.2 ⟨hl's.pairwise, hp'⟩).imp lt_iff_le_and_ne.2).sortedLT

Premises used: Iff.mpr, lt_iff_le_and_ne, List.SortedLE.pairwise, List.pairwise_and_iff, And.intro, List.Pairwise.sortedLT, List.Pairwise.imp
-- 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 R
hl's : l'.SortedLE
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:
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
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 : tail = [] ∨ head ≠ (head :: tail).getLast hl
⊢ (head :: tail).length = 1 ∨ (head :: tail).head hl ≠ (head :: tail).getLast hl

Tactic:
simp only [length_cons, add_eq_right, length_eq_zero_iff, head_cons]

Premises used: List.length_cons, List.head_cons, add_eq_right, List.length_eq_zero_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
l' : List R
hl's : l'.SortedLE
head : P
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:
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
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
refine_2 : head ≠ (head :: head2 :: tail).getLast hl
⊢ head2 :: tail = [] ∨ head ≠ (head :: head2 :: tail).getLast hl

Tactic:
simp only [reduceCtorEq, false_or]

Premises used: reduceCtorEq, false_or
-- 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 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
⊢ (∀ a' ∈ head2 :: tail, head ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail)

Tactic:
rw [pairwise_cons] at hp

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
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
hp₁ : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail)
⊢ map (⇑(lineMap ((head :: head2 :: tail).head hl) ((head :: head2 :: tail).getLast hl)) : (a : R) → P) l' =
    head :: head2 :: tail

Tactic:
rw [pairwise_cons] at hp

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
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

Tactic:
hp.1 ((head :: head2 :: tail).getLast hl) ?_

Premises used: List.getLast, List.cons, And.left
-- 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 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
refine_2 : (head :: head2 :: tail).getLast hl ∈ head2 :: tail
⊢ head ≠ (head :: head2 :: tail).getLast hl

Tactic:
refine hp.1 ((head :: head2 :: tail).getLast hl) ?_

Premises used: List.getLast, List.cons, And.left
-- 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 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 :: head2 :: tail).getLast hl ∈ head2 :: tail

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
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
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
⊢ tail = [] ∨ head ≠ (head :: 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

Premises used: reduceCtorEq, false_or, List.cons, List.pairwise_cons, 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 ≠ []
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
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
⊢ l.length = 1 ∨ l.head hl ≠ l.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

Premises used: List.head, reduceCtorEq, List.length_cons, List.head_cons, false_or, List.tail, List.cons, List.pairwise_cons, add_eq_right, List.length_eq_zero_iff, 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
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

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

Premises used: List.Sbtw, _private.0.List.exists_map_eq_of_sorted_iff_sbtw.match_1, Iff.intro