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 : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : w 0 + w 1 = 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)
⊢ w ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
    Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 (w 1)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [← hw]
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)
⊢ w = Finset.affineCombinationLineMapWeights 0 1 (w 1)

Tactic:
have h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1) := by
      rw [Fin.sum_univ_two] at hw
      ext i
      fin_cases i <;> simp [← hw]
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
h₁ :
  Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1))
    ((lineMap (s.points 0) (s.points 1) : (a : R) → P) (w 1) : P)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (1 + 1) → R) → P) w : P)

Tactic:
rw [h, Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _)]

Premises used: Finset.mem_univ, Finset.univ, Finset.affineCombination_affineCombinationLineMapWeights
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1))
    ((lineMap (s.points 0) (s.points 1) : (a : R) → P) (w 1) : P)

Tactic:
Set.mem_image_of_mem _ (h01 _)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i)
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1))
    ((lineMap (s.points 0) (s.points 1) : (a : R) → P) (w 1) : P)

Tactic:
exact Set.mem_image_of_mem _ (h01 _)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
h :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)),
    Membership.mem (γ := Set R) (Set.Ioo 0 1) (Finset.affineCombinationLineMapWeights 0 1 r i)
⊢ Membership.mem (α := P) s.interior ((lineMap (s.points 0) (s.points 1) : (a : R) → P) r : P)

Tactic:
rw [← Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _), affineCombination_mem_interior_iff
        (Finset.sum_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _) _)]

Premises used: Finset.mem_univ, Finset.univ, Affine.Simplex.affineCombination_mem_interior_iff, Finset.affineCombination_affineCombinationLineMapWeights, Finset.sum_affineCombinationLineMapWeights
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  Membership.mem (γ := Set R) (Set.Ioo 0 1)
    (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))
h₁ :
  Membership.mem (γ := Set R) (Set.Ioo 0 1)
    (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))
⊢ Membership.mem (γ := Set R) (Set.Ioo 0 1) (Finset.affineCombinationLineMapWeights 0 1 r i)

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
⊢ Membership.mem (γ := Set R) (Set.Ioo 0 1)
    (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))

Tactic:
simp [h0, h1]
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
⊢ Membership.mem (γ := Set R) (Set.Ioo 0 1)
    (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))

Tactic:
simp [h0, h1]
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
s : Simplex R P 1
p : P
rw :
  Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p ↔
    Membership.mem (γ := Set P)
        (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p ∧
      s.points 0 ≠ s.points 1
⊢ p ∈ s.interior ↔ Sbtw R (s.points 0) p (s.points 1)

Tactic:
rw [interior_eq_image_Ioo, sbtw_iff_mem_image_Ioo_and_ne]

Premises used: sbtw_iff_mem_image_Ioo_and_ne, Affine.Simplex.interior_eq_image_Ioo
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
s : Simplex R P 1
p : P
⊢ Ne (α := Fin 2) 0 1

Tactic:
decide
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
s : Simplex R P 1
p : P
⊢ Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p ↔
    Membership.mem (γ := Set P)
        (Set.image.{u_1, u_4} (α := R) (⇑(lineMap (s.points 0) (s.points 1)) : (a : R) → P) (Set.Ioo 0 1)) p ∧
      s.points 0 ≠ s.points 1

Tactic:
simp [s.independent.injective.ne (by decide : (0 : Fin 2) ≠ 1)]

Premises used: Function.Injective.ne, AffineIndependent.injective, Affine.Simplex.independent
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
inl : ∀ (hij : i < j), Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
inr : ∀ (hji : j < i), Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))

Tactic:
rcases h.lt_or_gt with hij | hji

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
hij : i < j
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))

Tactic:
simp [min_eq_left hij.le, max_eq_right hij.le]

Premises used: LT.lt.le, max_eq_right, min_eq_left
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
inr : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (max i j)) p (s.points (min i j))
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))

Tactic:
nth_rw 2 [sbtw_comm]

Premises used: sbtw_comm
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (max i j)) p (s.points (min i j))

Tactic:
simp [max_eq_left hji.le, min_eq_right hji.le]

Premises used: LT.lt.le, max_eq_left, min_eq_right
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))

Tactic:
have h' : Sbtw R (s.points i) p (s.points j) ↔
      Sbtw R (s.points (min i j)) p (s.points (max i j)) := by
    rcases h.lt_or_gt with hij | hji
    · simp [min_eq_left hij.le, max_eq_right hij.le]
    · nth_rw 2 [sbtw_comm]
      simp [max_eq_left hji.le, min_eq_right hji.le]
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
rw :
  Sbtw R (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0)) p
      (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1)) ↔
    Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ p ∈ (s.face (fs := {i, j}) ⋯).interior ↔ Sbtw R (s.points i) p (s.points j)

Tactic:
rw [h', mem_interior_iff_sbtw, face_points, face_points]

Premises used: Affine.Simplex.face_points, Affine.Simplex.mem_interior_iff_sbtw
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
a : (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = min i j
a₁ : (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1 = max i j
⊢ Sbtw R (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0)) p
      (s.points ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1)) ↔
    Sbtw R (s.points (min i j)) p (s.points (max i j))

Tactic:
congr! 4
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ Eq (α := Fin (n + 1))
    ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1))
        ⟨0, closedInterior_face_eq_affineSegment._proof_1⟩ :
      Fin (n + 1))
    (Finset.min' {i, j} ⋯ : Fin (n + 1))

Tactic:
Finset.orderEmbOfFin_zero _ _

Premises used: Finset.orderEmbOfFin_zero
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
h₁ : min i j = Finset.min' {i, j} ⋯
a : 0 < HAdd.hAdd (α := ℕ) 1 1
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = min i j

Tactic:
convert! Finset.orderEmbOfFin_zero _ _

Premises used: Finset.orderEmbOfFin_zero
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ min i j = Finset.min' {i, j} ⋯

Tactic:
(Finset.min'_pair i j).symm

Premises used: Finset.min'_pair, Eq.symm
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ min i j = Finset.min' {i, j} ⋯

Tactic:
exact (Finset.min'_pair i j).symm

Premises used: Finset.min'_pair, Eq.symm
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ 0 < HAdd.hAdd (α := ℕ) 1 1

Tactic:
lia
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ Eq (α := Fin (n + 1))
    ((Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) ⟨HAdd.hAdd (α := ℕ) 1 1 - 1, ⋯⟩ : Fin (n + 1))
    (Finset.max' {i, j} ⋯ : Fin (n + 1))

Tactic:
Finset.orderEmbOfFin_last _ _

Premises used: Finset.orderEmbOfFin_last
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
h₁ : max i j = Finset.max' {i, j} ⋯
a : 0 < HAdd.hAdd (α := ℕ) 1 1
⊢ (Finset.orderEmbOfFin {i, j} ⋯ : (a : Fin (1 + 1)) → Fin (n + 1)) 1 = max i j

Tactic:
convert! Finset.orderEmbOfFin_last _ _

Premises used: Finset.orderEmbOfFin_last
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ max i j = Finset.max' {i, j} ⋯

Tactic:
(Finset.max'_pair i j).symm

Premises used: Finset.max'_pair, Eq.symm
-- Module: Mathlib.Analysis.Convex.Between
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 : AffineSpace V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ max i j = Finset.max' {i, j} ⋯

Tactic:
exact (Finset.max'_pair i j).symm

Premises used: Finset.max'_pair, Eq.symm
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ SameRay R (y -ᵥ x) (z -ᵥ y)

Tactic:
simpa using sameRay_of_mem_segment ((mem_segment_iff_wbtw).2 (h.vsub_const x))

Premises used: Iff.mpr, mem_segment_iff_wbtw, sameRay_of_mem_segment, Wbtw.vsub_const
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Wbtw R x y z
rcases : ∀ (t : R) (ht0 : 0 ≤ t), t ≤ 1 → SameRay R ((lineMap x z : (a : R) → P) t -ᵥ x) (z -ᵥ x)
⊢ SameRay R (y -ᵥ x) (z -ᵥ x)

Tactic:
rcases h with ⟨t, ⟨ht0, _⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
right : t ≤ 1
⊢ SameRay R ((lineMap x z : (a : R) → P) t -ᵥ x) (z -ᵥ x)

Tactic:
simp [SameRay.sameRay_nonneg_smul_left (z -ᵥ x) ht0]

Premises used: SameRay.sameRay_nonneg_smul_left, VSub.vsub
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Wbtw R x y z
rcases : ∀ (t : R), 0 ≤ t → ∀ (ht1 : t ≤ 1), SameRay R (z -ᵥ x) (z -ᵥ (lineMap x z : (a : R) → P) t)
⊢ SameRay R (z -ᵥ x) (z -ᵥ y)

Tactic:
rcases h with ⟨t, ⟨_, ht1⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
t : R
left : 0 ≤ t
ht1 : t ≤ 1
⊢ SameRay R (z -ᵥ x) (z -ᵥ (lineMap x z : (a : R) → P) t)

Tactic:
simp [SameRay.sameRay_nonneg_smul_right (z -ᵥ x) (sub_nonneg.2 ht1)]

Premises used: Iff.mpr, VSub.vsub, SameRay.sameRay_nonneg_smul_right, sub_nonneg
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₁)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₁)
⊢ False

Tactic:
simp at h₂
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
⊢ i₁ ≠ i₃

Tactic:
have h₁₃ : i₁ ≠ i₃ := by
    rintro rfl
    simp at h₂
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₂)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₂)
h₁₃ : i₁ ≠ i₂
⊢ False

Tactic:
simp at h₁
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
⊢ i₂ ≠ i₃

Tactic:
have h₂₃ : i₂ ≠ i₃ := by
    rintro rfl
    simp at h₁
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₁, p₁}) p
h₂' : Membership.mem (γ := AffineSubspace R P) (affineSpan R {t.points i₂, p₂}) p
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃

Tactic:
lia