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₂ <;> simp +decide only at hx <;>
    fin_cases y₁

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

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

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

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

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

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

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

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

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