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 : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
ih' :
  ∀ (hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)) (hp : Pairwise (Wbtw R head) tail)
    (ht : List.Wbtw R tail), Pairwise (Sbtw R head) tail
hpne : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ (∀ a' ∈ tail, head2 ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail
hp : (∀ a' ∈ tail, Wbtw R head head2 a') ∧ Pairwise (Wbtw R head) tail
ht : List.Wbtw R (head2 :: tail)
a : P
ha : a ∈ tail
⊢ head2 ≠ head ∧ head2 ≠ a

Tactic:
⟨(hpne.1 head2 ?_).symm, hpne.2.1 a ha⟩

Premises used: Ne.symm, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
ih' :
  ∀ (hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)) (hp : Pairwise (Wbtw R head) tail)
    (ht : List.Wbtw R tail), Pairwise (Sbtw R head) tail
hpne : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ (∀ a' ∈ tail, head2 ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail
hp : (∀ a' ∈ tail, Wbtw R head head2 a') ∧ Pairwise (Wbtw R head) tail
ht : List.Wbtw R (head2 :: tail)
a : P
ha : a ∈ tail
cons : head2 ∈ head2 :: tail
⊢ head2 ≠ head ∧ head2 ≠ a

Tactic:
refine ⟨(hpne.1 head2 ?_).symm, hpne.2.1 a ha⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
ih' :
  ∀ (hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)) (hp : Pairwise (Wbtw R head) tail)
    (ht : List.Wbtw R tail), Pairwise (Sbtw R head) tail
hpne : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ (∀ a' ∈ tail, head2 ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail
hp : (∀ a' ∈ tail, Wbtw R head head2 a') ∧ Pairwise (Wbtw R head) tail
ht : List.Wbtw R (head2 :: tail)
a : P
ha : a ∈ tail
⊢ head2 ∈ head2 :: tail

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
ih' :
  ∀ (hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)) (hp : Pairwise (Wbtw R head) tail)
    (ht : List.Wbtw R tail), Pairwise (Sbtw R head) tail
hpne : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ (∀ a' ∈ tail, head2 ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail
hp : (∀ a' ∈ tail, Wbtw R head head2 a') ∧ Pairwise (Wbtw R head) tail
ht : List.Wbtw R (head2 :: tail)
⊢ Pairwise (Wbtw R head2) tail ∧ List.Wbtw R tail

Tactic:
rw [wbtw_cons] at ht

Premises used: List.wbtw_cons
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
ih' :
  ∀ (hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)) (hp : Pairwise (Wbtw R head) tail)
    (ht : List.Wbtw R tail), Pairwise (Sbtw R head) tail
hpne : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ (∀ a' ∈ tail, head2 ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail
hp : (∀ a' ∈ tail, Wbtw R head head2 a') ∧ Pairwise (Wbtw R head) tail
ht : Pairwise (Wbtw R head2) tail ∧ List.Wbtw R tail
⊢ Pairwise (Sbtw R head) tail

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 : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
cons :
  ∀ (hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) [head]) (hp : Pairwise (Wbtw R head) [])
    (ht : List.Wbtw.{u_1, u_2, u_4} R (P := P) []), Pairwise (Sbtw R head) []
cons₁ :
  ∀ (head2 : P) (tail : List P)
    (ih' :
      ∀ (hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)) (hp : Pairwise (Wbtw R head) tail)
        (ht : List.Wbtw R tail), Pairwise (Sbtw R head) tail)
    (hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: head2 :: tail)) (hp : Pairwise (Wbtw R head) (head2 :: tail))
    (ht : List.Wbtw R (head2 :: tail)), Pairwise (Sbtw R head) (head2 :: tail)
⊢ Pairwise (Sbtw R head) tail

Tactic:
induction tail with
        | nil => simp
        | cons head2 tail ih' =>
          rw [pairwise_cons] at hp hpne hpne ⊢
          refine ⟨fun a ha ↦ ⟨hp.1 a ha, ?_⟩, ?_⟩
          · refine ⟨(hpne.1 head2 ?_).symm, hpne.2.1 a ha⟩
            simp
          · rw [wbtw_cons] at ht
            grind [List.pairwise_iff_forall_sublist]

Premises used: List.pairwise_iff_forall_sublist, List.wbtw_cons, 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 : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ (∀ a' ∈ tail, head ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail

Tactic:
rw [pairwise_cons] at hpne

Premises used: List.pairwise_cons
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
hpne₁ : (∀ a' ∈ tail, head ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail
⊢ Pairwise (Wbtw R head) tail

Tactic:
rw [pairwise_cons] at hpne

Premises used: List.pairwise_cons
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
hpne₁ : (∀ a' ∈ tail, head ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail
hp₁ : Pairwise (Wbtw R head) tail
⊢ List.Wbtw R tail

Tactic:
rw [pairwise_cons] at hpne

Premises used: List.pairwise_cons
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : (∀ a' ∈ tail, head ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ Triplewise (Sbtw R) tail

Tactic:
(ih.1 ⟨ht, hpne.2⟩).1

Premises used: And.right, And.left, And.intro, Iff.mp
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : (∀ a' ∈ tail, head ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ Triplewise (Sbtw R) tail

Tactic:
exact (ih.1 ⟨ht, hpne.2⟩).1

Premises used: And.right, And.left, And.intro, Iff.mp
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ ∀ (a : P), head :: tail ≠ [a, a]

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
h : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
⊢ List.Wbtw R tail

Tactic:
have ht' : tail.Wbtw R := ht.imp _root_.Sbtw.wbtw
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
h : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
⊢ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]

Tactic:
simp only [ht', true_and, ht] at ih

Premises used: true_and
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
h : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
cons : (∀ a' ∈ tail, head ≠ a') ∧ ∀ (a : P), tail ≠ [a, a]
⊢ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)

Tactic:
rw [pairwise_cons, ih]

Premises used: List.pairwise_cons
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
h : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
⊢ (∀ a' ∈ tail, head ≠ a') ∧ ∀ (a : P), tail ≠ [a, a]

Tactic:
⟨fun a ha' ↦ ?_, fun a ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
h : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
cons : ∀ (a : P) (ha' : a ∈ tail), head ≠ a
cons₁ : ∀ (a : P), tail ≠ [a, a]
⊢ (∀ a' ∈ tail, head ≠ a') ∧ ∀ (a : P), tail ≠ [a, a]

Tactic:
refine ⟨fun a ha' ↦ ?_, fun a ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
h : (Pairwise (Sbtw R head) [] ∧ Triplewise.{u_4} (α := P) (Sbtw R) []) ∧ ∀ (a : P), [head] ≠ [a, a]
hp : Pairwise (Sbtw R head) []
ht : Triplewise.{u_4} (α := P) (Sbtw R) []
ha : ∀ (a : P), [head] ≠ [a, a]
ht' : List.Wbtw.{u_1, u_2, u_4} R (P := P) []
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) [] ↔ ∀ (a : P), [] ≠ [a, a]
ha' : Membership.mem (γ := List P) [] head
⊢ False

Tactic:
simp at ha'
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
h :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) (head2 :: tail)
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
⊢ (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) 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 : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
h :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) (head2 :: tail)
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hp₁ : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
⊢ Triplewise (Sbtw R) (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 : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
h :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) (head2 :: tail)
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hp₁ : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht₁ : Triplewise (Sbtw R) (head2 :: tail)
⊢ ∀ (a : P), head :: head2 :: tail ≠ [a, a]

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 : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
h :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) (head2 :: tail)
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hp₁ : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht₁ : Triplewise (Sbtw R) (head2 :: tail)
ha₁ : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
⊢ List.Wbtw R (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 : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
h :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) (head2 :: tail)
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hp₁ : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht₁ : Triplewise (Sbtw R) (head2 :: tail)
ha₁ : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht'₁ : List.Wbtw R (head2 :: tail)
⊢ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]

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 : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
h :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) (head2 :: tail)
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hp₁ : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht₁ : Triplewise (Sbtw R) (head2 :: tail)
ha₁ : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht'₁ : List.Wbtw R (head2 :: tail)
ih₁ : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
⊢ 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 : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
h :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
cons :
  ((Pairwise (Sbtw R head) (head :: tail) ∧ Triplewise (Sbtw R) (head :: tail)) ∧
      ∀ (a : P), head :: head :: tail ≠ [a, a]) →
    ∀ (hp : (∀ a' ∈ tail, Sbtw R head head a') ∧ Pairwise (Sbtw R head) tail) (ht : Triplewise (Sbtw R) (head :: tail))
      (ha : ∀ (a : P), head :: head :: tail ≠ [a, a]) (ht' : List.Wbtw R (head :: tail))
      (ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail) ↔ ∀ (a : P), head :: tail ≠ [a, a])
      (ha' : head ∈ head :: tail), False
cons₁ : ∀ (hat : head ∈ tail), False
⊢ False

Tactic:
rcases mem_cons.1 ha' with rfl | hat

Premises used: Iff.mp, List.mem_cons, rfl
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
h : (Pairwise (Sbtw R head) [head] ∧ Triplewise (Sbtw R) [head]) ∧ ∀ (a : P), [head, head] ≠ [a, a]
hp : (∀ (a' : P), Membership.mem (γ := List P) [] a' → Sbtw R head head a') ∧ Pairwise (Sbtw R head) []
ht : Triplewise (Sbtw R) [head]
ha : ∀ (a : P), [head, head] ≠ [a, a]
ht' : List.Wbtw R [head]
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) [head] ↔ ∀ (a : P), [head] ≠ [a, a]
ha' : head ∈ [head]
⊢ False

Tactic:
simp at ha
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head3 : P
tail : List P
h :
  (Pairwise (Sbtw R head) (head :: head3 :: tail) ∧ Triplewise (Sbtw R) (head :: head3 :: tail)) ∧
    ∀ (a : P), head :: head :: head3 :: tail ≠ [a, a]
hp : (∀ a' ∈ head3 :: tail, Sbtw R head head a') ∧ Pairwise (Sbtw R head) (head3 :: tail)
ht : Triplewise (Sbtw R) (head :: head3 :: tail)
ha : ∀ (a : P), head :: head :: head3 :: tail ≠ [a, a]
ht' : List.Wbtw R (head :: head3 :: tail)
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: head3 :: tail) ↔ ∀ (a : P), head :: head3 :: tail ≠ [a, a]
ha' : head ∈ head :: head3 :: tail
⊢ False

Tactic:
simpa using hp.1 head3

Premises used: And.left
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head : P
tail : List P
h :
  (Pairwise (Sbtw R head) (head :: tail) ∧ Triplewise (Sbtw R) (head :: tail)) ∧
    ∀ (a : P), head :: head :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head :: tail)
ha : ∀ (a : P), head :: head :: tail ≠ [a, a]
ht' : List.Wbtw R (head :: tail)
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail) ↔ ∀ (a : P), head :: tail ≠ [a, a]
ha' : head ∈ head :: tail
cons :
  ((Pairwise (Sbtw R head) [head] ∧ Triplewise (Sbtw R) [head]) ∧ ∀ (a : P), [head, head] ≠ [a, a]) →
    ∀ (hp : (∀ (a' : P), Membership.mem (γ := List P) [] a' → Sbtw R head head a') ∧ Pairwise (Sbtw R head) [])
      (ht : Triplewise (Sbtw R) [head]) (ha : ∀ (a : P), [head, head] ≠ [a, a]) (ht' : List.Wbtw R [head])
      (ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) [head] ↔ ∀ (a : P), [head] ≠ [a, a]) (ha' : head ∈ [head]), False
cons₁ :
  ∀ (head3 : P) (tail : List P),
    ((Pairwise (Sbtw R head) (head :: head3 :: tail) ∧ Triplewise (Sbtw R) (head :: head3 :: tail)) ∧
        ∀ (a : P), head :: head :: head3 :: tail ≠ [a, a]) →
      ∀ (hp : (∀ a' ∈ head3 :: tail, Sbtw R head head a') ∧ Pairwise (Sbtw R head) (head3 :: tail))
        (ht : Triplewise (Sbtw R) (head :: head3 :: tail)) (ha : ∀ (a : P), head :: head :: head3 :: tail ≠ [a, a])
        (ht' : List.Wbtw R (head :: head3 :: tail))
        (ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: head3 :: tail) ↔ ∀ (a : P), head :: head3 :: tail ≠ [a, a])
        (ha' : head ∈ head :: head3 :: tail), False
⊢ False

Tactic:
cases tail with
            | nil => simp at ha
            | cons head3 tail => simpa using hp.1 head3

Premises used: List.cons, List.nil
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
head head2 : P
tail : List P
h :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hat : head ∈ tail
⊢ False

Tactic:
simpa using hp.1 head hat

Premises used: And.left