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 : 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
⊢ (∀ a' ∈ tail, head ≠ a') ∧ ∀ (a : P), tail ≠ [a, a]
have cons₁ : ∀ (a : P), tail ≠ [a, a]
Tactic: refine ⟨fun a ha' ↦ ?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (hypothesis)
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
⊢ False
have hp₁ : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
Tactic: rw [pairwise_cons] at hp
Cleared hypotheses: hp, ht, ha, ht', ih, ha'
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
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
⊢ False
have 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
Tactic: rcases mem_cons.1 ha' with rfl | hat
Cleared hypotheses: head2, h, hp, ht, ha, ht', ih, ha'
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
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
⊢ False
have cons₁ : ∀ (hat : head ∈ tail), False
Tactic: rcases mem_cons.1 ha' with rfl | hat
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
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
⊢ False
have 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
Tactic: cases tail with
            | nil => simp at ha
            | cons head3 tail => simpa using hp.1 head3
Cleared hypotheses: tail, h, hp, ht, ha, ht', ih, ha'
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
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
⊢ False
have 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
Tactic: cases tail with
            | nil => simp at ha
            | cons head3 tail => simpa using hp.1 head3
Cleared hypotheses: tail, h, hp, ht, ha, ht', ih, ha'
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
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
⊢ False
have 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
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
Cleared hypotheses: tail, h, hp, ht, ha, ht', ih, ha'
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
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
⊢ False
have 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
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
Cleared hypotheses: tail, h, hp, ht, ha, ht', ih, ha'
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
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
⊢ List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l ↔ Triplewise (Sbtw R) l ∧ ∀ (a : P), l ≠ [a, a]
have 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]
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
Cleared hypotheses: 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 : 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]
⊢ List.Wbtw R l ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l ↔ Triplewise (Sbtw R) l ∧ ∀ (a : P), l ≠ [a, a]
have 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]
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
Cleared hypotheses: 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 : 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
⊢ List.Sbtw R (p :: l) ↔ Pairwise (Sbtw R p) l ∧ List.Sbtw R l ∧ l ≠ [p]
have 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]
Tactic: rw [sbtw_iff_triplewise_and_ne_pair, ← not_exists, triplewise_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 : 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
⊢ ((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]
have simp : Pairwise (Sbtw R p) l → ¬l = [p] → (Triplewise (Sbtw R) l ↔ List.Sbtw R l)
Tactic: simp only [cons.injEq, exists_eq_left', and_assoc, and_congr_right_iff, ne_eq, and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
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]
⊢ Triplewise (Sbtw R) l ↔ List.Sbtw R l
have rw : Triplewise (Sbtw R) l → ¬∃ (x : P), l = [x, x]
Tactic: rw [sbtw_iff_triplewise_and_ne_pair, iff_self_and, ← not_exists]
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
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.Sbtw.{u_1, u_3, u_5} R (P := P') (map (⇑f : (a : P) → P') l) ↔ List.Sbtw R l
have 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
Tactic: rw [List.Sbtw, List.Sbtw, hf.list_wbtw_map_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
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
have 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
Tactic: refine ⟨fun ⟨hl, hp⟩ ↦ ⟨hl, hp.of_map _ ?_⟩, fun ⟨hl, hp⟩ ↦ ⟨hl, hp.map _ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
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
⊢ 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
have 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')
Tactic: refine ⟨fun ⟨hl, hp⟩ ↦ ⟨hl, hp.of_map _ ?_⟩, fun ⟨hl, hp⟩ ↦ ⟨hl, hp.map _ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (hypothesis)
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'
⊢ List.Wbtw.{u_1, u_3, u_5} R (P := P') (map (⇑f : (a : P) → P') l) ↔ List.Wbtw R l
have hf : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (hypothesis)
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'
⊢ List.Sbtw.{u_1, u_3, u_5} R (P := P') (map (⇑f : (a : P) → P') l) ↔ List.Sbtw R l
have hf : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head : R
tail : List R
ih : ∀ (h : tail.SortedLE), List.Wbtw R tail
h : (head :: tail).SortedLE
⊢ List.Wbtw R (head :: tail)
have cons : Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail
Tactic: rw [wbtw_cons]
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head : R
tail : List R
ih : ∀ (h : tail.SortedLE), List.Wbtw R tail
h : (head :: tail).SortedLE
⊢ Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail
have cons : Pairwise (Wbtw R head) tail
Tactic: refine ⟨?_, ih h.pairwise.of_cons.sortedLE⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head 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')
have cons : (∀ a' ∈ tail', Wbtw R head head' a') ∧ Pairwise (Wbtw R head) tail'
Tactic: rw [pairwise_cons]
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head 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'
have cons : ∀ a' ∈ tail', Wbtw R head head' a'
Tactic: refine ⟨?_, ih (h.pairwise.sublist ?_).sortedLE⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head 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'
⊢ (∀ a' ∈ tail', Wbtw R head head' a') ∧ Pairwise (Wbtw R head) tail'
have cons₁ : head :: tail' <+ head :: head' :: tail'
Tactic: refine ⟨?_, ih (h.pairwise.sublist ?_).sortedLE⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (hypothesis)
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'
have 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'
Tactic: simp_rw [sortedLE_iff_pairwise, pairwise_cons_cons, pairwise_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
head : R
tail : List R
h : (head :: tail).SortedLE
⊢ Pairwise (Wbtw R head) tail
have cons : ∀ (h : [head].SortedLE), Pairwise (Wbtw R head) []
Tactic: induction tail with
    | nil => simp
    | cons head' tail' ih =>
      rw [pairwise_cons]
      refine ⟨?_, ih (h.pairwise.sublist ?_).sortedLE⟩
      · simp_rw [sortedLE_iff_pairwise, pairwise_cons_cons, pairwise_cons] at h
        exact fun a ha ↦ .of_le_of_le h.1 (h.2.2.1 a ha)
      · simp
Cleared hypotheses: tail, h