awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Between
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 : 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:
simp [Set.range_comp, Set.image_insert_eq, hT.symm.collinear]

Premises used: Set.range_comp, Wbtw.collinear, Wbtw.symm, Set.image_insert_eq
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ LE.le.{u_1} (α := R) 0 2⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ LE.le.{u_1} (α := R) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Convex.Between
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
refine : (lineMap y ((pointReflection R x : (a : P) → P) y) : (a : R) → P) 2⁻¹ = x
⊢ Wbtw R y x ((pointReflection R x : (a : P) → P) y)

Tactic:
refine ⟨2⁻¹, ⟨by simp, by norm_num⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.Between
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
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
⊢ (lineMap y ((pointReflection R x : (a : P) → P) y) : (a : R) → P) 2⁻¹ = x

Tactic:
rw [lineMap_apply, pointReflection_apply, vadd_vsub_assoc, ← two_smul R (x -ᵥ y)]

Premises used: vadd_vsub_assoc, two_smul, VSub.vsub, AffineMap.lineMap_apply, AffineEquiv.pointReflection_apply
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ 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:
simp
-- Module: Mathlib.Analysis.Convex.Between
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)

Tactic:
⟨wbtw_pointReflection _ _ _, h, ?_⟩

Premises used: And.intro, wbtw_pointReflection, Sbtw
-- Module: Mathlib.Analysis.Convex.Between
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
refine : x ≠ (pointReflection R x : (a : P) → P) y
⊢ Sbtw R y x ((pointReflection R x : (a : P) → P) y)

Tactic:
refine ⟨wbtw_pointReflection _ _ _, h, ?_⟩
-- Module: Mathlib.Analysis.Convex.Between
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
nth_rw : Ne (α := P) ((pointReflection R x : (a : P) → P) x : P) ((pointReflection R x : (a : P) → P) y : P)
⊢ x ≠ (pointReflection R x : (a : P) → P) y

Tactic:
nth_rw 1 [← pointReflection_self R x]

Premises used: AffineEquiv.pointReflection_self
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ Ne (α := P) ((pointReflection R x : (a : P) → P) x : P) ((pointReflection R x : (a : P) → P) y : P)

Tactic:
(pointReflection_involutive R x).injective.ne h

Premises used: Function.Injective.ne, AffineEquiv.pointReflection_involutive, Function.Involutive.injective
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ Ne (α := P) ((pointReflection R x : (a : P) → P) x : P) ((pointReflection R x : (a : P) → P) y : P)

Tactic:
exact (pointReflection_involutive R x).injective.ne h

Premises used: Function.Injective.ne, AffineEquiv.pointReflection_involutive, Function.Involutive.injective
-- Module: Mathlib.Analysis.Convex.Between
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) ((pointReflection R (midpoint R x y) : (a : P) → P) x)

Tactic:
wbtw_pointReflection R (midpoint R x y) x

Premises used: midpoint, wbtw_pointReflection
-- Module: Mathlib.Analysis.Convex.Between
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 : y = (pointReflection R (midpoint R x y) : (a : P) → P) x
⊢ Wbtw R x (midpoint R x y) y

Tactic:
convert! wbtw_pointReflection R (midpoint R x y) x

Premises used: midpoint, wbtw_pointReflection
-- Module: Mathlib.Analysis.Convex.Between
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 h₁ : y = y
⊢ y = (pointReflection R (midpoint R x y) : (a : P) → P) x

Tactic:
rw [pointReflection_midpoint_left]

Premises used: AffineEquiv.pointReflection_midpoint_left
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ midpoint R x y ≠ x

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ midpoint R x y ≠ x

Tactic:
have h : midpoint R x y ≠ x := by simp [h]
-- Module: Mathlib.Analysis.Convex.Between
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) ((pointReflection R (midpoint R x y) : (a : P) → P) x)

Tactic:
sbtw_pointReflection_of_ne R h

Premises used: sbtw_pointReflection_of_ne
-- Module: Mathlib.Analysis.Convex.Between
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
h₁ : y = (pointReflection R (midpoint R x y) : (a : P) → P) x
⊢ Sbtw R x (midpoint R x y) y

Tactic:
convert! sbtw_pointReflection_of_ne R h

Premises used: sbtw_pointReflection_of_ne
-- Module: Mathlib.Analysis.Convex.Between
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
h₁ h₂ : y = y
⊢ y = (pointReflection R (midpoint R x y) : (a : P) → P) x

Tactic:
rw [pointReflection_midpoint_left]

Premises used: AffineEquiv.pointReflection_midpoint_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
p : P
l : List P
⊢ List.Wbtw R (p :: l) ↔ Pairwise (Wbtw R p) l ∧ List.Wbtw R l

Tactic:
triplewise_cons

Premises used: List.triplewise_cons, List.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
⊢ List.Wbtw.{u_1, u_2, u_4} R (P := P) []

Tactic:
simp [List.Wbtw]

Premises used: List.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
⊢ List.Sbtw.{u_1, u_2, u_4} R (P := P) []

Tactic:
simp [List.Sbtw]

Premises used: List.Sbtw
-- 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
p₁ : P
⊢ List.Wbtw R [p₁]

Tactic:
simp [List.Wbtw]

Premises used: List.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
p₁ : P
⊢ List.Sbtw R [p₁]

Tactic:
simp [List.Sbtw]

Premises used: List.Sbtw
-- 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
p₁ p₂ : P
⊢ List.Wbtw R [p₁, p₂]

Tactic:
simp [List.Wbtw]

Premises used: List.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
p₁ p₂ : P
⊢ List.Sbtw R [p₁, p₂] ↔ p₁ ≠ p₂

Tactic:
simp [List.Sbtw]

Premises used: List.Sbtw
-- 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
p₁ p₂ p₃ : P
⊢ List.Wbtw R [p₁, p₂, p₃] ↔ Wbtw R p₁ p₂ p₃

Tactic:
simp [List.Wbtw]

Premises used: List.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
p₁ p₂ p₃ : P
simp : Wbtw R p₁ p₂ p₃ ∧ (¬p₁ = p₂ ∧ ¬p₁ = p₃) ∧ ¬p₂ = p₃ ↔ Sbtw R p₁ p₂ p₃
⊢ List.Sbtw R [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]

Premises used: and_true, and_self, List.Sbtw, forall_eq, forall_eq_or_imp, ne_eq, List.pairwise_cons, List.Pairwise.nil, List.wbtw_triple, or_false, implies_true, List.mem_cons, List.not_mem_nil, IsEmpty.forall_iff
-- 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₂ p₃ : P
⊢ Wbtw R p₁ p₂ p₃ ∧ (¬p₁ = p₂ ∧ ¬p₁ = p₃) ∧ ¬p₂ = p₃ ↔ Sbtw R p₁ p₂ p₃

Tactic:
⟨fun ⟨hw, ⟨h₁₂, h₁₃⟩, h₂₃⟩ ↦ ⟨hw, Ne.symm h₁₂, h₂₃⟩,
         fun h ↦ ⟨h.1, ⟨h.2.1.symm, h.left_ne_right⟩, h.2.2⟩⟩

Premises used: _private.0.List.sbtw_triple.match_7, Ne.symm, Sbtw.left_ne_right, And.right, And.left, And.intro, Iff.intro, Sbtw
-- 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₂ p₃ : P
⊢ Wbtw R p₁ p₂ p₃ ∧ (¬p₁ = p₂ ∧ ¬p₁ = p₃) ∧ ¬p₂ = p₃ ↔ Sbtw R p₁ p₂ p₃

Tactic:
exact ⟨fun ⟨hw, ⟨h₁₂, h₁₃⟩, h₂₃⟩ ↦ ⟨hw, Ne.symm h₁₂, h₂₃⟩,
         fun h ↦ ⟨h.1, ⟨h.2.1.symm, h.left_ne_right⟩, h.2.2⟩⟩
-- 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
p₁ p₂ p₃ p₄ : P
⊢ List.Wbtw R [p₁, p₂, p₃, p₄] ↔ Wbtw R p₁ p₂ p₃ ∧ Wbtw R p₁ p₂ p₄ ∧ Wbtw R p₁ p₃ p₄ ∧ Wbtw R p₂ p₃ p₄

Tactic:
simp [List.Wbtw, triplewise_cons, and_assoc]

Premises used: List.triplewise_cons, and_assoc, List.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
p₁ p₂ p₃ p₄ : P
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₄
⊢ 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₄

Tactic:
simp [List.Sbtw, List.Wbtw, triplewise_cons, Sbtw]

Premises used: List.triplewise_cons, List.Sbtw, List.Wbtw, Sbtw
-- 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₂ p₃ p₄ : P
⊢ (((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:
aesop
-- 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
l : List P
h : List.Sbtw R l
⊢ List.Wbtw R l

Tactic:
h.1

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
l : List P
h : List.Sbtw R l
⊢ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) l

Tactic:
h.2

Premises used: And.right
-- 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
⊢ 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:
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 : 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 :
  (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]
⊢ 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:
rw [wbtw_cons, triplewise_cons]

Premises used: List.triplewise_cons, 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 : 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]

Tactic:
⟨fun h ↦ ?_,
            fun ⟨⟨hp, ht⟩, ha⟩ ↦ ⟨⟨hp.imp _root_.Sbtw.wbtw, ht.imp _root_.Sbtw.wbtw⟩, ?_⟩⟩

Premises used: List.Pairwise, Wbtw, Ne, _private.0.List.sbtw_iff_triplewise_and_ne_pair.match_1, List.cons, And, And.intro, Iff.intro, Sbtw.wbtw, List.Wbtw, List.Triplewise.imp, List.Pairwise.imp
-- 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]
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]
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)
⊢ (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⟩, ?_⟩⟩
-- 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 (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)
⊢ Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: tail)

Tactic:
rcases h with ⟨⟨hp, ht⟩, hpne⟩
-- 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 (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 (Wbtw R head) tail

Tactic:
rcases h with ⟨⟨hp, ht⟩, hpne⟩
-- 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 (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
⊢ List.Wbtw R tail

Tactic:
rcases h with ⟨⟨hp, ht⟩, hpne⟩
-- 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
⊢ (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]

Tactic:
⟨⟨?_, ?_⟩, ?_⟩

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
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
cons₂ : ∀ (a : P), head :: tail ≠ [a, a]
⊢ (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]

Tactic:
refine ⟨⟨?_, ?_⟩, ?_⟩
-- 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
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:
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 : Pairwise (fun (x1 x2 : P) ↦ x1 ≠ x2) (head :: head2 :: tail)
hp : Pairwise (Wbtw R head) (head2 :: tail)
ht : List.Wbtw R (head2 :: tail)
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
⊢ Pairwise (Sbtw R head) (head2 :: tail)

Tactic:
rw [pairwise_cons] at hp hpne 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 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

Tactic:
⟨fun a ha ↦ ⟨hp.1 a ha, ?_⟩, ?_⟩

Premises used: 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)
cons : ∀ (a : P) (ha : a ∈ tail), head2 ≠ head ∧ head2 ≠ a
cons₁ : Pairwise (Sbtw R head) tail
⊢ (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail

Tactic:
refine ⟨fun a ha ↦ ⟨hp.1 a ha, ?_⟩, ?_⟩