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 : 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]
ha' : head ∈ tail
cons :
  ((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
cons₁ :
  ∀ (head2 : P) (tail : List P),
    ((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), False
⊢ False

Tactic:
cases tail with
        | nil => simp at ha'
        | cons head2 tail =>
          rw [pairwise_cons] at hp
          rcases mem_cons.1 ha' with rfl | hat
          · cases tail with
            | nil => simp at ha
            | cons head3 tail => simpa using hp.1 head3
          · simpa using hp.1 head hat

Premises used: List.cons, List.pairwise_cons, Iff.mp, List.mem_cons, rfl, 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 a : P
h : (Pairwise (Sbtw R head) [a, a] ∧ Triplewise (Sbtw R) [a, a]) ∧ ∀ (a_1 : P), [head, a, a] ≠ [a_1, a_1]
hp : Pairwise (Sbtw R head) [a, a]
ht : Triplewise (Sbtw R) [a, a]
ha : ∀ (a_1 : P), [head, a, a] ≠ [a_1, a_1]
ht' : List.Wbtw R [a, a]
ih : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) [a, a] ↔ ∀ (a_1 : P), [a, a] ≠ [a_1, a_1]
⊢ False

Tactic:
simp at hp
-- 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
l : List P
nil :
  List.Wbtw.{u_1, u_2, u_4} R (P := P) [] ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) [] ↔
    Triplewise.{u_4} (α := P) (Sbtw R) [] ∧ ∀ (a : P), [] ≠ [a, a]
cons :
  ∀ (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]),
    List.Wbtw R (head :: tail) ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail) ↔
      Triplewise (Sbtw R) (head :: tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
⊢ List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l ↔ Triplewise (Sbtw R) l ∧ ∀ (a : P), l ≠ [a, a]

Tactic:
induction l with
  | nil => simp
  | cons head tail ih =>
    rw [wbtw_cons, triplewise_cons]
    refine ⟨fun h ↦ ?_,
            fun ⟨⟨hp, ht⟩, ha⟩ ↦ ⟨⟨hp.imp _root_.Sbtw.wbtw, ht.imp _root_.Sbtw.wbtw⟩, ?_⟩⟩
    · rcases h with ⟨⟨hp, ht⟩, hpne⟩
      refine ⟨⟨?_, ?_⟩, ?_⟩
      · clear ih
        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]
      · rw [pairwise_cons] at hpne
        exact (ih.1 ⟨ht, hpne.2⟩).1
      · grind
    · have ht' : tail.Wbtw R := ht.imp _root_.Sbtw.wbtw
      simp only [ht', true_and, ht] at ih
      rw [pairwise_cons, ih]
      refine ⟨fun a ha' ↦ ?_, fun a ↦ ?_⟩
      · rintro rfl
        cases tail with
        | nil => simp at ha'
        | cons head2 tail =>
          rw [pairwise_cons] at hp
          rcases mem_cons.1 ha' with rfl | hat
          · cases tail with
            | nil => simp at ha
            | cons head3 tail => simpa using hp.1 head3
          · simpa using hp.1 head hat
      · rintro rfl
        simp at hp

Premises used: List.head, List.triplewise_cons, List.pairwise_iff_forall_sublist, List.wbtw_cons, List.tail, List.cons, List.pairwise_cons, rfl, true_and, 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
p : P
l : List P
rw :
  ((Pairwise (Sbtw R p) l ∧ Triplewise (Sbtw R) l) ∧ ¬∃ (x : P), p :: l = [x, x]) ↔
    Pairwise (Sbtw R p) l ∧ List.Sbtw R l ∧ l ≠ [p]
⊢ List.Sbtw R (p :: l) ↔ Pairwise (Sbtw R p) l ∧ List.Sbtw R l ∧ l ≠ [p]

Tactic:
rw [sbtw_iff_triplewise_and_ne_pair, ← not_exists, triplewise_cons]

Premises used: List.triplewise_cons, not_exists, List.sbtw_iff_triplewise_and_ne_pair
-- 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
p : P
l : List P
simp : Pairwise (Sbtw R p) l → ¬l = [p] → (Triplewise (Sbtw R) l ↔ List.Sbtw R l)
⊢ ((Pairwise (Sbtw R p) l ∧ Triplewise (Sbtw R) l) ∧ ¬∃ (x : P), p :: l = [x, x]) ↔
    Pairwise (Sbtw R p) l ∧ List.Sbtw R l ∧ l ≠ [p]

Tactic:
simp only [cons.injEq, exists_eq_left', and_assoc, and_congr_right_iff, ne_eq, and_congr_left_iff]

Premises used: exists_eq_left', and_congr_right_iff, ne_eq, List.cons.injEq, and_congr_left_iff, and_assoc
-- 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
p : P
l : List P
hp : Pairwise (Sbtw R p) l
hne : ¬l = [p]
rw : Triplewise (Sbtw R) l → ¬∃ (x : P), l = [x, x]
⊢ Triplewise (Sbtw R) l ↔ List.Sbtw R l

Tactic:
rw [sbtw_iff_triplewise_and_ne_pair, iff_self_and, ← not_exists]

Premises used: not_exists, iff_self_and, List.sbtw_iff_triplewise_and_ne_pair
-- 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
p a : P
hp : Pairwise (Sbtw R p) [a, a]
hne : ¬[a, a] = [p]
hl : Triplewise (Sbtw R) [a, a]
⊢ False

Tactic:
simp at hp
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
l : List P
h : List.Wbtw R l
f : P →ᵃ[R] P'
⊢ List.Wbtw.{u_1, u_3, u_5} R (P := P') (map (⇑f : (a : P) → P') l)

Tactic:
Triplewise.map (fun h ↦ Wbtw.map h f) h

Premises used: Wbtw.map, List.Wbtw, List.Triplewise.map
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
l : List P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
⊢ List.Wbtw.{u_1, u_3, u_5} R (P := P') (map (⇑f : (a : P) → P') l) ↔ List.Wbtw R l

Tactic:
⟨fun h ↦ h.of_map hf.wbtw_map_iff.1, fun h ↦ h.map f⟩

Premises used: List.Triplewise.of_map, List.Wbtw.map, Iff.intro, Function.Injective.wbtw_map_iff, Iff.mp
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
l : List P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
rw :
  List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P') ↦ x1 ≠ x2) (map (⇑f : (a : P) → P') l) ↔
    List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
⊢ List.Sbtw.{u_1, u_3, u_5} R (P := P') (map (⇑f : (a : P) → P') l) ↔ List.Sbtw R l

Tactic:
rw [List.Sbtw, List.Sbtw, hf.list_wbtw_map_iff]

Premises used: List.Sbtw, Function.Injective.list_wbtw_map_iff
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
l : List P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
⊢ List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P') ↦ x1 ≠ x2) (map (⇑f : (a : P) → P') l) ↔
    List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l

Tactic:
⟨fun ⟨hl, hp⟩ ↦ ⟨hl, hp.of_map _ ?_⟩, fun ⟨hl, hp⟩ ↦ ⟨hl, hp.map _ ?_⟩⟩

Premises used: List.Pairwise, _private.0.Function.Injective.list_sbtw_map_iff.match_2, List.map, List.Pairwise.of_map, Ne, And, _private.0.Function.Injective.list_sbtw_map_iff.match_1, And.intro, Iff.intro, List.Pairwise.map, List.Wbtw, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
l : List P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
refine_1 :
  List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P') ↦ x1 ≠ x2) (map (⇑f : (a : P) → P') l) →
    ∀ (hl : List.Wbtw R l) (hp : Pairwise (fun (x1 x2 : P') ↦ x1 ≠ x2) (map (⇑f : (a : P) → P') l)) (a b : P),
      Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') a : P') ((f : (a : P) → P') b : P') → a ≠ b
refine_2 :
  List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l →
    ∀ (hl : List.Wbtw R l) (hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l) (a b : P),
      a ≠ b → Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') a : P') ((f : (a : P) → P') b : P')
⊢ List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P') ↦ x1 ≠ x2) (map (⇑f : (a : P) → P') l) ↔
    List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l

Tactic:
refine ⟨fun ⟨hl, hp⟩ ↦ ⟨hl, hp.of_map _ ?_⟩, fun ⟨hl, hp⟩ ↦ ⟨hl, hp.map _ ?_⟩⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
l : List P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
h : List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P') ↦ x1 ≠ x2) (map (⇑f : (a : P) → P') l)
hl : List.Wbtw R l
hp : Pairwise (fun (x1 x2 : P') ↦ x1 ≠ x2) (map (⇑f : (a : P) → P') l)
⊢ ∀ (a b : P), Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') a : P') ((f : (a : P) → P') b : P') → a ≠ b

Tactic:
simp [hf.ne_iff]

Premises used: Function.Injective.ne_iff
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
l : List P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
h : List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
hl : List.Wbtw R l
hp : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l
⊢ ∀ (a b : P), a ≠ b → Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') a : P') ((f : (a : P) → P') b : P')

Tactic:
simp [hf.ne_iff]

Premises used: Function.Injective.ne_iff
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
l : List P
f : P ≃ᵃ[R] P'
⊢ Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑(↑f : P →ᵃ[R] P') : (a : P) → P')

Tactic:
have hf : Function.Injective f.toAffineMap := f.injective
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
l : List P
f : P ≃ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑(↑f : P →ᵃ[R] P') : (a : P) → P')
⊢ List.Wbtw.{u_1, u_3, u_5} R (P := P') (map (⇑f : (a : P) → P') l) ↔ List.Wbtw R l

Tactic:
apply hf.list_wbtw_map_iff

Premises used: Function.Injective.list_wbtw_map_iff
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
l : List P
f : P ≃ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑(↑f : P →ᵃ[R] P') : (a : P) → P')
⊢ List.Sbtw.{u_1, u_3, u_5} R (P := P') (map (⇑f : (a : P) → P') l) ↔ List.Sbtw R l

Tactic:
apply hf.list_sbtw_map_iff

Premises used: Function.Injective.list_sbtw_map_iff
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
h : SortedLE.{u_1} (α := R) []
⊢ List.Wbtw R (P := R) []

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head : R
tail : List R
ih : ∀ (h : tail.SortedLE), List.Wbtw R tail
h : (head :: tail).SortedLE
cons : Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail
⊢ List.Wbtw R (head :: tail)

Tactic:
rw [wbtw_cons]

Premises used: List.wbtw_cons
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head : R
tail : List R
ih : ∀ (h : tail.SortedLE), List.Wbtw R tail
h : (head :: tail).SortedLE
⊢ Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail

Tactic:
⟨?_, ih h.pairwise.of_cons.sortedLE⟩

Premises used: List.SortedLE.pairwise, And.intro, List.Pairwise.sortedLE, List.Pairwise.of_cons
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head : R
tail : List R
ih : ∀ (h : tail.SortedLE), List.Wbtw R tail
h : (head :: tail).SortedLE
cons : Pairwise (Wbtw R head) tail
⊢ Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail

Tactic:
refine ⟨?_, ih h.pairwise.of_cons.sortedLE⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head : R
h : [head].SortedLE
⊢ Pairwise (Wbtw R head) []

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head head' : R
tail' : List R
ih : ∀ (h : (head :: tail').SortedLE), Pairwise (Wbtw R head) tail'
h : (head :: head' :: tail').SortedLE
cons : (∀ a' ∈ tail', Wbtw R head head' a') ∧ Pairwise (Wbtw R head) tail'
⊢ Pairwise (Wbtw R head) (head' :: tail')

Tactic:
rw [pairwise_cons]

Premises used: List.pairwise_cons
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head head' : R
tail' : List R
ih : ∀ (h : (head :: tail').SortedLE), Pairwise (Wbtw R head) tail'
h : (head :: head' :: tail').SortedLE
⊢ (∀ a' ∈ tail', Wbtw R head head' a') ∧ Pairwise (Wbtw R head) tail'

Tactic:
⟨?_, ih (h.pairwise.sublist ?_).sortedLE⟩

Premises used: List.SortedLE.pairwise, List.Pairwise.sublist, And.intro, List.Pairwise.sortedLE
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head head' : R
tail' : List R
ih : ∀ (h : (head :: tail').SortedLE), Pairwise (Wbtw R head) tail'
h : (head :: head' :: tail').SortedLE
cons : ∀ a' ∈ tail', Wbtw R head head' a'
cons₁ : head :: tail' <+ head :: head' :: tail'
⊢ (∀ a' ∈ tail', Wbtw R head head' a') ∧ Pairwise (Wbtw R head) tail'

Tactic:
refine ⟨?_, ih (h.pairwise.sublist ?_).sortedLE⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head head' : R
tail' : List R
ih : ∀ (h : (head :: tail').SortedLE), Pairwise (Wbtw R head) tail'
h : (head :: head' :: tail').SortedLE
⊢ head ≤ head' ∧
    ((∀ a' ∈ tail', head ≤ a') ∧ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) tail') ∧
      (∀ a' ∈ tail', head' ≤ a') ∧ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) tail'

Tactic:
simp_rw [sortedLE_iff_pairwise, pairwise_cons_cons, pairwise_cons] at h

Premises used: List.pairwise_cons_cons, List.sortedLE_iff_pairwise, List.pairwise_cons
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head head' : R
tail' : List R
ih : ∀ (h : (head :: tail').SortedLE), Pairwise (Wbtw R head) tail'
h :
  head ≤ head' ∧
    ((∀ a' ∈ tail', head ≤ a') ∧ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) tail') ∧
      (∀ a' ∈ tail', head' ≤ a') ∧ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) tail'
⊢ ∀ a' ∈ tail', Wbtw R head head' a'

Tactic:
fun a ha ↦ .of_le_of_le h.1 (h.2.2.1 a ha)

Premises used: Wbtw.of_le_of_le, And.right, And.left
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head head' : R
tail' : List R
ih : ∀ (h : (head :: tail').SortedLE), Pairwise (Wbtw R head) tail'
h :
  head ≤ head' ∧
    ((∀ a' ∈ tail', head ≤ a') ∧ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) tail') ∧
      (∀ a' ∈ tail', head' ≤ a') ∧ Pairwise (fun (x1 x2 : R) ↦ x1 ≤ x2) tail'
⊢ ∀ a' ∈ tail', Wbtw R head head' a'

Tactic:
exact fun a ha ↦ .of_le_of_le h.1 (h.2.2.1 a ha)
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head head' : R
tail' : List R
ih : ∀ (h : (head :: tail').SortedLE), Pairwise (Wbtw R head) tail'
h : (head :: head' :: tail').SortedLE
⊢ head :: tail' <+ head :: head' :: tail'

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.BetweenList
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) []
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')
⊢ Pairwise (Wbtw R 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

Premises used: List.pairwise_cons_cons, List.sortedLE_iff_pairwise, List.cons, List.pairwise_cons, List.nil
-- Module: Mathlib.Analysis.Convex.BetweenList
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) []
cons :
  ∀ (head : R) (tail : List R) (ih : ∀ (h : tail.SortedLE), List.Wbtw R tail) (h : (head :: tail).SortedLE),
    List.Wbtw R (head :: tail)
⊢ List.Wbtw R l

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

Premises used: List.head, List.pairwise_cons_cons, List.sortedLE_iff_pairwise, List.wbtw_cons, List.tail, List.cons, List.pairwise_cons, List.nil
-- Module: Mathlib.Analysis.Convex.BetweenList
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
l : List R
h : l.SortedLT
⊢ List.Sbtw R l

Tactic:
⟨h.sortedLE.wbtw, h.nodup⟩

Premises used: List.Sbtw, List.SortedLT.nodup, List.SortedLE.wbtw, And.intro, List.SortedLT.sortedLE
-- 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'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l) ↔ List.Wbtw R l

Tactic:
⟨fun ⟨l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩

Premises used: _private.0.List.exists_map_eq_of_sorted_nonempty_iff_wbtw.match_1, Iff.intro, List.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 ≠ []
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
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
⊢ (∃ (l' : List R), l'.SortedLE ∧ 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 ↦ ?_⟩
-- 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
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
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')
⊢ List.Wbtw R 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'.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.{u_1, u_2, u_4} R (P := P) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')

Tactic:
Wbtw.map hl's.wbtw _

Premises used: List.SortedLE.wbtw, List.Wbtw.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 : ∃ (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.{u_1, u_2, u_4} R (P := P) (map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l')

Tactic:
exact Wbtw.map hl's.wbtw _

Premises used: List.SortedLE.wbtw, List.Wbtw.map