Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i j : Fin (2 + 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
h₂ : dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)

Tactic:
rcases hi with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩

Goal state after:
case refine_2.inl
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
i₃ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₁₃ : i ≠ i₃
h₂₃ : j ≠ i₃
h₁₂ : i ≠ j
h₁ : dist (t.points i) (t.points j) = dist (t.points i) (t.points i₃)
h₂ : dist (t.points i) (t.points j) = dist (t.points j) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points i) (t.points j)

case refine_2.inr.inl
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
i₃ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₂₃ : i ≠ i₃
h₁₃ : j ≠ i₃
h₁₂ : j ≠ i
h₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i₃)
h₂ : dist (t.points j) (t.points i) = dist (t.points i) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i)

case refine_2.inr.inr.inl
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
i₂ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₁₂ : i ≠ i₂
h₂₃ : i₂ ≠ j
h₁₃ : i ≠ j
h₁ : dist (t.points i) (t.points i₂) = dist (t.points i) (t.points j)
h₂ : dist (t.points i) (t.points i₂) = dist (t.points i₂) (t.points j)
⊢ dist (t.points i) (t.points j) = dist (t.points i) (t.points i₂)

case refine_2.inr.inr.inr.inl
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
i₂ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₂₃ : i₂ ≠ i
h₁₂ : j ≠ i₂
h₁₃ : j ≠ i
h₁ : dist (t.points j) (t.points i₂) = dist (t.points j) (t.points i)
h₂ : dist (t.points j) (t.points i₂) = dist (t.points i₂) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i₂)

case refine_2.inr.inr.inr.inr.inl
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
i₁ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₁₂ : i₁ ≠ i
h₁₃ : i₁ ≠ j
h₂₃ : i ≠ j
h₁ : dist (t.points i₁) (t.points i) = dist (t.points i₁) (t.points j)
h₂ : dist (t.points i₁) (t.points i) = dist (t.points i) (t.points j)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i)

case refine_2.inr.inr.inr.inr.inr
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
i₁ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₁₃ : i₁ ≠ i
h₁₂ : i₁ ≠ j
h₂₃ : j ≠ i
h₁ : dist (t.points i₁) (t.points j) = dist (t.points i₁) (t.points i)
h₂ : dist (t.points i₁) (t.points j) = dist (t.points j) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points j)