awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
ι : Type u_6
i j k : ι
h : Function.Injective ![i, j, k]
T : ι → P
hT :
  AffineIndependent R (ι := Fin (Nat.succ 0).succ.succ)
    (T ∘ (⇑{ toFun := ![i, j, k], inj' := h : Fin (Nat.succ 0).succ.succ ↪ ι } : (a : Fin (Nat.succ 0).succ.succ) → ι))
⊢ ¬Wbtw R (T i) (T j) (T k)
have hT₁ : ¬Collinear R
    (Set.range (ι := Fin 3)
      (T ∘
        (⇑{ toFun := ![i, j, k], inj' := h : Fin (Nat.succ 0).succ.succ ↪ ι } : (a : Fin (Nat.succ 0).succ.succ) → ι)))
Tactic: rw [affineIndependent_iff_not_collinear] at hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
ι : Type u_6
i j k : ι
h : Function.Injective ![i, j, k]
T : ι → P
hT :
  ¬Collinear R
      (Set.range (ι := Fin 3)
        (T ∘
          (⇑{ toFun := ![i, j, k], inj' := h : Fin (Nat.succ 0).succ.succ ↪ ι } :
            (a : Fin (Nat.succ 0).succ.succ) → ι)))
⊢ ¬Wbtw R (T i) (T j) (T k)
have contrapose : ∀ (hT : Wbtw R (T i) (T j) (T k)),
  Collinear R
    (Set.range (ι := Fin 3)
      (T ∘
        (⇑{ toFun := ![i, j, k], inj' := h : Fin (Nat.succ 0).succ.succ ↪ ι } : (a : Fin (Nat.succ 0).succ.succ) → ι)))
Tactic: contrapose hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
⊢ Wbtw R y x ((pointReflection R x : (a : P) → P) y)
have refine : (lineMap y ((pointReflection R x : (a : P) → P) y) : (a : R) → P) 2⁻¹ = x
Tactic: refine ⟨2⁻¹, ⟨by simp, by norm_num⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
⊢ (lineMap y ((pointReflection R x : (a : P) → P) y) : (a : R) → P) 2⁻¹ = x
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2⁻¹ (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 (x -ᵥ y)) +ᵥ y = x
Tactic: rw [lineMap_apply, pointReflection_apply, vadd_vsub_assoc, ← two_smul R (x -ᵥ y)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
h : x ≠ y
⊢ Sbtw R y x ((pointReflection R x : (a : P) → P) y)
have refine : x ≠ (pointReflection R x : (a : P) → P) y
Tactic: refine ⟨wbtw_pointReflection _ _ _, h, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
h : x ≠ y
⊢ x ≠ (pointReflection R x : (a : P) → P) y
have nth_rw : Ne (α := P) ((pointReflection R x : (a : P) → P) x : P) ((pointReflection R x : (a : P) → P) y : P)
Tactic: nth_rw 1 [← pointReflection_self R x]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
⊢ Wbtw R x (midpoint R x y) y
have h : y = (pointReflection R (midpoint R x y) : (a : P) → P) x
Tactic: convert! wbtw_pointReflection R (midpoint R x y) x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
⊢ y = (pointReflection R (midpoint R x y) : (a : P) → P) x
have h : y = y
Tactic: rw [pointReflection_midpoint_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
h : x ≠ y
⊢ Sbtw R x (midpoint R x y) y
have h₁ : midpoint R x y ≠ x
Tactic: have h : midpoint R x y ≠ x := by simp [h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
h_1 : x ≠ y
h : midpoint R x y ≠ x
⊢ Sbtw R x (midpoint R x y) y
have h₁ : y = (pointReflection R (midpoint R x y) : (a : P) → P) x
Tactic: convert! sbtw_pointReflection_of_ne R h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
h_1 : x ≠ y
h : midpoint R x y ≠ x
⊢ y = (pointReflection R (midpoint R x y) : (a : P) → P) x
have h₁ : y = y
Tactic: rw [pointReflection_midpoint_left]
-- 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₂ p₃ : P
⊢ List.Sbtw R [p₁, p₂, p₃] ↔ Sbtw R p₁ p₂ p₃
have simp : Wbtw R p₁ p₂ p₃ ∧ (¬p₁ = p₂ ∧ ¬p₁ = p₃) ∧ ¬p₂ = p₃ ↔ Sbtw R p₁ p₂ p₃
Tactic: simp only [List.Sbtw, wbtw_triple, ne_eq, pairwise_cons, mem_cons, not_mem_nil, or_false,
    forall_eq_or_imp, forall_eq, IsEmpty.forall_iff, implies_true, Pairwise.nil, and_self, and_true]
-- 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₂ p₃ p₄ : P
⊢ List.Sbtw R [p₁, p₂, p₃, p₄] ↔ Sbtw R p₁ p₂ p₃ ∧ Sbtw R p₁ p₂ p₄ ∧ Sbtw R p₁ p₃ p₄ ∧ Sbtw R p₂ p₃ p₄
have simp : (((Wbtw R p₁ p₂ p₃ ∧ Wbtw R p₁ p₂ p₄) ∧ Wbtw R p₁ p₃ p₄) ∧ Wbtw R p₂ p₃ p₄) ∧
    (¬p₁ = p₂ ∧ ¬p₁ = p₃ ∧ ¬p₁ = p₄) ∧ (¬p₂ = p₃ ∧ ¬p₂ = p₄) ∧ ¬p₃ = p₄ ↔
  (Wbtw R p₁ p₂ p₃ ∧ ¬p₂ = p₁ ∧ ¬p₂ = p₃) ∧
    (Wbtw R p₁ p₂ p₄ ∧ ¬p₂ = p₁ ∧ ¬p₂ = p₄) ∧
      (Wbtw R p₁ p₃ p₄ ∧ ¬p₃ = p₁ ∧ ¬p₃ = p₄) ∧ Wbtw R p₂ p₃ p₄ ∧ ¬p₃ = p₂ ∧ ¬p₃ = p₄
Tactic: simp [List.Sbtw, List.Wbtw, triplewise_cons, Sbtw]
-- 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
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]
have cons : (Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail) ↔
  (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
Tactic: rw [wbtw_cons, 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
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]
⊢ (Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail) ↔
    (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
have cons : ∀ (h : (Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)),
  (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
Tactic: refine ⟨fun h ↦ ?_,
            fun ⟨⟨hp, ht⟩, ha⟩ ↦ ⟨⟨hp.imp _root_.Sbtw.wbtw, ht.imp _root_.Sbtw.wbtw⟩, ?_⟩⟩
-- 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
ih : List.Wbtw R tail ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
cons :
  ∀ (h : (Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)),
    (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
⊢ (Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail) ↔
    (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
have cons₁ : ((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]),
    Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
Tactic: refine ⟨fun h ↦ ?_,
            fun ⟨⟨hp, ht⟩, ha⟩ ↦ ⟨⟨hp.imp _root_.Sbtw.wbtw, ht.imp _root_.Sbtw.wbtw⟩, ?_⟩⟩
-- 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 : 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 (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
⊢ (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
have hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
Tactic: rcases h with ⟨⟨hp, ht⟩, hpne⟩
Cleared hypotheses: h
-- 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 : 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 (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
⊢ (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
have hp : Pairwise (Wbtw R head) tail
Tactic: rcases h with ⟨⟨hp, ht⟩, hpne⟩
Cleared hypotheses: h
-- 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 : 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 (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
hpne : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
⊢ (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
have ht : List.Wbtw R tail
Tactic: rcases h with ⟨⟨hp, ht⟩, hpne⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : 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
⊢ (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
have cons : Pairwise (Sbtw R head) tail
Tactic: refine ⟨⟨?_, ?_⟩, ?_⟩
-- 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
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
cons : Pairwise (Sbtw R head) tail
⊢ (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
have cons₁ : Triplewise (Sbtw R) tail
Tactic: refine ⟨⟨?_, ?_⟩, ?_⟩
-- 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
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
cons : Pairwise (Sbtw R head) tail
cons₁ : Triplewise (Sbtw R) tail
⊢ (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
have cons₂ : ∀ (a : P), head :: tail ≠ [a, a]
Tactic: refine ⟨⟨?_, ?_⟩, ?_⟩
-- 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
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)
have cons : ∀ (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' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
Tactic: rw [pairwise_cons] at hp hpne hpne ⊢
Cleared hypotheses: hpne, hp, ht
-- 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
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' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
have cons : ∀ (a : P) (ha : a ∈ tail), head2 ≠ head ∧ head2 ≠ a
Tactic: refine ⟨fun a ha ↦ ⟨hp.1 a 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
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)
cons : ∀ (a : P) (ha : a ∈ tail), head2 ≠ head ∧ head2 ≠ a
⊢ (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
have cons₁ : Pairwise (Sbtw R head) tail
Tactic: refine ⟨fun a ha ↦ ⟨hp.1 a 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
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
have cons : head2 ∈ head2 :: tail
Tactic: refine ⟨(hpne.1 head2 ?_).symm, hpne.2.1 a ha⟩
-- 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
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 (Sbtw R head) tail
have ht₁ : Pairwise (Wbtw R head2) tail ∧ List.Wbtw R tail
Tactic: rw [wbtw_cons] at ht
Cleared hypotheses: ht
-- 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
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
have 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) []
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]
Cleared hypotheses: tail, hpne, hp, ht
-- 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
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) []
⊢ Pairwise (Sbtw R head) tail
have 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)
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]
Cleared hypotheses: tail, hpne, hp, ht
-- 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 : 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
⊢ Triplewise (Sbtw R) tail
have hpne₁ : (∀ a' ∈ tail, head ≠ a') ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail
Tactic: rw [pairwise_cons] at hpne
Cleared hypotheses: hpne, hp, ht
-- 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 : 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]
⊢ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
have ht' : List.Wbtw R tail
Tactic: have ht' : tail.Wbtw R := ht.imp _root_.Sbtw.wbtw
-- 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 : 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) (head :: tail)
have ih₁ : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
Tactic: simp only [ht', true_and, ht] at ih
Cleared hypotheses: ih
-- 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]
⊢ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
have cons : (∀ a' ∈ tail, head ≠ a') ∧ ∀ (a : P), tail ≠ [a, a]
Tactic: rw [pairwise_cons, ih]
-- 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]
⊢ (∀ a' ∈ tail, head ≠ a') ∧ ∀ (a : P), tail ≠ [a, a]
have cons : ∀ (a : P) (ha' : a ∈ tail), head ≠ a
Tactic: refine ⟨fun a ha' ↦ ?_, fun a ↦ ?_⟩