-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair [NoZeroSMulDivisors 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₁' : p ∈ line[R, t.points i₁, p₁]) (h₂' : p ∈ line[R, t.points i₂, p₂]) :
    Sbtw R (t.points i₁) p p₁

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : LinearOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
this : DecidableRel fun x1 x2 => x1 < x2 := LinearOrderedRing.decidableLT
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i : Fin (2 + 1), w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    affineSpan R {t.points i₁, (lineMap (t.points i₂) (t.points i₃)) r₁}
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}
⊢ Sbtw R (t.points i₁) ((Finset.affineCombination R Finset.univ t.points) w) ((lineMap (t.points i₂) (t.points i₃)) r₁)

Tactic:
have h₁s :=
  sign_eq_of_affineCombination_mem_affineSpan_single_lineMap t.independent hw (Finset.mem_univ _)
    (Finset.mem_univ _) (Finset.mem_univ _) h₁₂ h₁₃ h₂₃ hr₁0 hr₁1 h₁'

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : LinearOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
this : DecidableRel fun x1 x2 => x1 < x2 := LinearOrderedRing.decidableLT
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i : Fin (2 + 1), w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    affineSpan R {t.points i₁, (lineMap (t.points i₂) (t.points i₃)) r₁}
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
⊢ Sbtw R (t.points i₁) ((Finset.affineCombination R Finset.univ t.points) w) ((lineMap (t.points i₂) (t.points i₃)) r₁)

Proof state:
case inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : LinearOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
t : Affine.Triangle R P
i₂ i₃ : Fin 3
this : DecidableRel fun x1 x2 => x1 < x2 := LinearOrderedRing.decidableLT
h₂₃ : i₂ ≠ i₃
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
w : Fin (2 + 1) → R
hw : ∑ i : Fin (2 + 1), w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
i : Fin 3
h₁₂ : i ≠ i₂
h₁₃ : i ≠ i₃
h3 : ∀ (i_1 : Fin 3), i_1 = i ∨ i_1 = i₂ ∨ i_1 = i₃
hu : Finset.univ = {i, i₂, i₃}
h₂ : Sbtw R (t.points i) ((lineMap (t.points i) (t.points i₃)) r₂) (t.points i₃)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    affineSpan R
      {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i),
        (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    affineSpan R {t.points i₂, (lineMap (t.points i) (t.points i₃)) r₂}
h₂s : SignType.sign (w i) = SignType.sign (w i₃)
⊢ SignType.sign (w i) = SignType.sign (w i₃)

Tactic:
exact h₂s

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : LinearOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors 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₁' : p ∈ affineSpan R {t.points i₁, p₁}
h₂' : p ∈ affineSpan R {t.points i₂, p₂}
this : DecidableRel fun x1 x2 => x1 < x2 := LinearOrderedRing.decidableLT
⊢ Sbtw R (t.points i₁) p p₁

Tactic:
have h₁₃ : i₁ ≠ i₃ := by
  rintro rfl
  simp at h₂

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : LinearOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors 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₁' : p ∈ affineSpan R {t.points i₁, p₁}
h₂' : p ∈ affineSpan R {t.points i₂, p₂}
this : DecidableRel fun x1 x2 => x1 < x2 := LinearOrderedRing.decidableLT
h₁₃ : i₁ ≠ i₃
⊢ Sbtw R (t.points i₁) p p₁

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : LinearOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors 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₁' : p ∈ affineSpan R {t.points i₁, p₁}
h₂' : p ∈ affineSpan R {t.points i₂, p₂}
this : DecidableRel fun x1 x2 => x1 < x2 := LinearOrderedRing.decidableLT
h₁₃ : i₁ ≠ i₃
⊢ Sbtw R (t.points i₁) p p₁

Tactic:
have h₂₃ : i₂ ≠ i₃ := by
  rintro rfl
  simp at h₁

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : LinearOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors 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₁' : p ∈ affineSpan R {t.points i₁, p₁}
h₂' : p ∈ affineSpan R {t.points i₂, p₂}
this : DecidableRel fun x1 x2 => x1 < x2 := LinearOrderedRing.decidableLT
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Sbtw R (t.points i₁) p p₁