[GOAL]
ι : Type u_1
c : ComplexShape ι
⊢ symm (symm c) = c
[PROOFSTEP]
ext
[GOAL]
case Rel.h.h.a
ι : Type u_1
c : ComplexShape ι
x✝¹ x✝ : ι
⊢ Rel (symm (symm c)) x✝¹ x✝ ↔ Rel c x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ : ι
w : Relation.Comp c₁.Rel c₂.Rel i✝ j✝
w' : Relation.Comp c₁.Rel c₂.Rel i✝ j'✝
⊢ j✝ = j'✝
[PROOFSTEP]
obtain ⟨k, w₁, w₂⟩ := w
[GOAL]
case intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ : ι
w' : Relation.Comp c₁.Rel c₂.Rel i✝ j'✝
k : ι
w₁ : Rel c₁ i✝ k
w₂ : Rel c₂ k j✝
⊢ j✝ = j'✝
[PROOFSTEP]
obtain ⟨k', w₁', w₂'⟩ := w'
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ k : ι
w₁ : Rel c₁ i✝ k
w₂ : Rel c₂ k j✝
k' : ι
w₁' : Rel c₁ i✝ k'
w₂' : Rel c₂ k' j'✝
⊢ j✝ = j'✝
[PROOFSTEP]
rw [c₁.next_eq w₁ w₁'] at w₂ 
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ k : ι
w₁ : Rel c₁ i✝ k
k' : ι
w₂ : Rel c₂ k' j✝
w₁' : Rel c₁ i✝ k'
w₂' : Rel c₂ k' j'✝
⊢ j✝ = j'✝
[PROOFSTEP]
exact c₂.next_eq w₂ w₂'
[GOAL]
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ : ι
w : Relation.Comp c₁.Rel c₂.Rel i✝ j✝
w' : Relation.Comp c₁.Rel c₂.Rel i'✝ j✝
⊢ i✝ = i'✝
[PROOFSTEP]
obtain ⟨k, w₁, w₂⟩ := w
[GOAL]
case intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ : ι
w' : Relation.Comp c₁.Rel c₂.Rel i'✝ j✝
k : ι
w₁ : Rel c₁ i✝ k
w₂ : Rel c₂ k j✝
⊢ i✝ = i'✝
[PROOFSTEP]
obtain ⟨k', w₁', w₂'⟩ := w'
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ k : ι
w₁ : Rel c₁ i✝ k
w₂ : Rel c₂ k j✝
k' : ι
w₁' : Rel c₁ i'✝ k'
w₂' : Rel c₂ k' j✝
⊢ i✝ = i'✝
[PROOFSTEP]
rw [c₂.prev_eq w₂ w₂'] at w₁ 
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ k : ι
w₂ : Rel c₂ k j✝
k' : ι
w₁ : Rel c₁ i✝ k'
w₁' : Rel c₁ i'✝ k'
w₂' : Rel c₂ k' j✝
⊢ i✝ = i'✝
[PROOFSTEP]
exact c₁.prev_eq w₁ w₁'
[GOAL]
ι : Type u_1
c : ComplexShape ι
i : ι
⊢ Subsingleton { j // Rel c i j }
[PROOFSTEP]
constructor
[GOAL]
case allEq
ι : Type u_1
c : ComplexShape ι
i : ι
⊢ ∀ (a b : { j // Rel c i j }), a = b
[PROOFSTEP]
rintro ⟨j, rij⟩ ⟨k, rik⟩
[GOAL]
case allEq.mk.mk
ι : Type u_1
c : ComplexShape ι
i j : ι
rij : Rel c i j
k : ι
rik : Rel c i k
⊢ { val := j, property := rij } = { val := k, property := rik }
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_val
ι : Type u_1
c : ComplexShape ι
i j : ι
rij : Rel c i j
k : ι
rik : Rel c i k
⊢ j = k
[PROOFSTEP]
exact c.next_eq rij rik
[GOAL]
ι : Type u_1
c : ComplexShape ι
j : ι
⊢ Subsingleton { i // Rel c i j }
[PROOFSTEP]
constructor
[GOAL]
case allEq
ι : Type u_1
c : ComplexShape ι
j : ι
⊢ ∀ (a b : { i // Rel c i j }), a = b
[PROOFSTEP]
rintro ⟨i, rik⟩ ⟨j, rjk⟩
[GOAL]
case allEq.mk.mk
ι : Type u_1
c : ComplexShape ι
j✝ i : ι
rik : Rel c i j✝
j : ι
rjk : Rel c j j✝
⊢ { val := i, property := rik } = { val := j, property := rjk }
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_val
ι : Type u_1
c : ComplexShape ι
j✝ i : ι
rik : Rel c i j✝
j : ι
rjk : Rel c j j✝
⊢ i = j
[PROOFSTEP]
exact c.prev_eq rik rjk
[GOAL]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ next c i = j
[PROOFSTEP]
apply c.next_eq _ h
[GOAL]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c i (next c i)
[PROOFSTEP]
rw [next]
[GOAL]
ι : 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)
[PROOFSTEP]
rw [dif_pos]
[GOAL]
ι : 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
[PROOFSTEP]
exact Exists.choose_spec ⟨j, h⟩
[GOAL]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ prev c j = i
[PROOFSTEP]
apply c.prev_eq _ h
[GOAL]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c (prev c j) j
[PROOFSTEP]
rw [prev, dif_pos]
[GOAL]
ι : 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
[PROOFSTEP]
exact Exists.choose_spec (⟨i, h⟩ : ∃ k, c.Rel k j)
