ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c (prev c j) j
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ prev c j = i
apply c.prev_eq _ h
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c (Exists.choose ?hc) j

case hc
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ ∃ i, Rel c i j
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c (prev c j) j
rw [prev, dif_pos]
no goals
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c (Exists.choose ?hc) j

case hc
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ ∃ i, Rel c i j
exact Exists.choose_spec (⟨i, h⟩ : ∃ k, c.Rel k j)