ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c i (next c i)
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ next c i = j
apply c.next_eq _ h
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c i (if h : ∃ j, Rel c i j then Exists.choose h else i)
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c i (next c i)
rw [next]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c i (Exists.choose ?hc)

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

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