Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: 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₁ x₂ : Fin (2 + 1)
hx : x₁ < x₂
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hxy : dist (t.points x₁) (t.points x₂) = dist (t.points y₁) (t.points y₂)
⊢ x₁ = y₁ ∧ x₂ = y₂

Tactic:
fin_cases x₁ <;> fin_cases x₂

Goal state after:
case «0».«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)
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩
hxy : dist (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = y₁ ∧ (fun i ↦ i) ⟨0, ⋯⟩ = y₂

case «0».«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)
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩
hxy : dist (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = y₁ ∧ (fun i ↦ i) ⟨1, ⋯⟩ = y₂

case «0».«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)
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩
hxy : dist (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points ((fun i ↦ i) ⟨2, ⋯⟩)) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = y₁ ∧ (fun i ↦ i) ⟨2, ⋯⟩ = y₂

case «1».«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)
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩
hxy : dist (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = y₁ ∧ (fun i ↦ i) ⟨0, ⋯⟩ = y₂

case «1».«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)
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩
hxy : dist (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = y₁ ∧ (fun i ↦ i) ⟨1, ⋯⟩ = y₂

case «1».«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)
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩
hxy : dist (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) (t.points ((fun i ↦ i) ⟨2, ⋯⟩)) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = y₁ ∧ (fun i ↦ i) ⟨2, ⋯⟩ = y₂

case «2».«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)
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩
hxy : dist (t.points ((fun i ↦ i) ⟨2, ⋯⟩)) (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨2, ⋯⟩ = y₁ ∧ (fun i ↦ i) ⟨0, ⋯⟩ = y₂

case «2».«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)
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩
hxy : dist (t.points ((fun i ↦ i) ⟨2, ⋯⟩)) (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨2, ⋯⟩ = y₁ ∧ (fun i ↦ i) ⟨1, ⋯⟩ = y₂

case «2».«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)
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hx : (fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩
hxy : dist (t.points ((fun i ↦ i) ⟨2, ⋯⟩)) (t.points ((fun i ↦ i) ⟨2, ⋯⟩)) = dist (t.points y₁) (t.points y₂)
⊢ (fun i ↦ i) ⟨2, ⋯⟩ = y₁ ∧ (fun i ↦ i) ⟨2, ⋯⟩ = y₂