-- 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:
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₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
hle : affineSpan R {t.points i₂, t.points i₃} ≤ affineSpan R (Set.range t.points)
⊢ p₁ ∈ affineSpan R (Set.range t.points)

Tactic:
rw [AffineSubspace.le_def'] at hle

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₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
hle : ∀ p ∈ affineSpan R {t.points i₂, t.points i₃}, p ∈ affineSpan R (Set.range t.points)
⊢ p₁ ∈ affineSpan R (Set.range t.points)

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₃
h₂₃ : i₂ ≠ i₃
⊢ Sbtw R (t.points i₁) p p₁

Tactic:
have h3 : ∀ i : Fin 3, i = i₁ ∨ i = i₂ ∨ i = i₃ := by omega

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₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ 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₂
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
      {(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₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
⊢ ∀ (i : Fin 3), SignType.sign (w i) = SignType.sign (w i₃)

Tactic:
intro i

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₂
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
      {(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₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
i : Fin 3
⊢ SignType.sign (w i) = SignType.sign (w i₃)

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₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
hp : p ∈ affineSpan R (Set.range t.points)
h₁i : p₁ ∈ ⇑(lineMap (t.points i₂) (t.points i₃)) '' Set.Ioo 0 1
⊢ Sbtw R (t.points i₁) p p₁

Tactic:
have h₂i := h₂.mem_image_Ioo

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₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
hp : p ∈ affineSpan R (Set.range t.points)
h₁i : p₁ ∈ ⇑(lineMap (t.points i₂) (t.points i₃)) '' Set.Ioo 0 1
h₂i : p₂ ∈ ⇑(lineMap (t.points i₁) (t.points i₃)) '' Set.Ioo 0 1
⊢ Sbtw R (t.points i₁) p p₁