Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case «0»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨0, ⋯⟩ < x₂
hxy : dist (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points x₂) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = y₁ ∧ x₂ = y₂

pp: case «1»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨1, ⋯⟩ < x₂
hxy : dist (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) (t.points x₂) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = y₁ ∧ x₂ = y₂

pp: case «2»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨2, ⋯⟩ < x₂
hxy : dist (t.points ((fun i ↦ i) ⟨2, ⋯⟩)) (t.points x₂) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨2, ⋯⟩ = y₁ ∧ x₂ = y₂

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨0, ⋯⟩ < x₂
hxy : dist (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points x₂) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = y₁ ∧ x₂ = y₂

case «1»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨1, ⋯⟩ < x₂
hxy : dist (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) (t.points x₂) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = y₁ ∧ x₂ = y₂

case «2»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨2, ⋯⟩ < x₂
hxy : dist (t.points ((fun i ↦ i) ⟨2, ⋯⟩)) (t.points x₂) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨2, ⋯⟩ = y₁ ∧ x₂ = y₂