-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma prev_f_of_not_boundaryGE [e.IsRelIff] {i j : ι} (hij : c.prev j = i)
    (hj : ¬ e.BoundaryGE j) :
    c'.prev (e.f j) = e.f i

Proof state:
case neg.hj
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
⊢ False

Tactic:
simp only [BoundaryGE, not_and, not_forall, not_not] at hj

Result:
case neg.hj
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ x, c'.Rel (e.f x) (e.f j)
⊢ False

Proof state:
case neg.hj.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ x, c'.Rel (e.f x) (e.f j)
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ False

Tactic:
rw [e.rel_iff] at hi

Result:
case neg.hj.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ x, c'.Rel (e.f x) (e.f j)
i : ι
hi : c.Rel i j
⊢ False

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
⊢ c'.prev (e.f j) = e.f i

Tactic:
by_cases hij' : c.Rel i j

Result:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : c.Rel i j
⊢ c'.prev (e.f j) = e.f i

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ c'.prev (e.f j) = e.f i

Proof state:
case neg.hj.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ x, c'.Rel (e.f x) (e.f j)
i : ι
hij : i = j
hi : c.Rel i j
⊢ False

Tactic:
exact hij' (by simpa only [hij] using hi)

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ ¬c.Rel (c.prev j) j

Tactic:
simpa only [hij] using hij'

Result:
no goals

Proof state:
case neg.hj
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hij : c.prev j = j
hij' : ¬c.Rel j j
⊢ ¬c'.Rel (c'.prev (e.f j)) (e.f j)

Tactic:
intro hj'

Result:
case neg.hj
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
⊢ False

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ j = i

Tactic:
simpa only [c.prev_eq_self j (by simpa only [hij] using hij')] using hij

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : c.Rel i j
⊢ c'.Rel (e.f i) (e.f j)

Tactic:
simpa only [e.rel_iff] using hij'

Result:
no goals

Proof state:
case neg.hj.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ x, c'.Rel (e.f x) (e.f j)
i : ι
hi : c.Rel i j
⊢ False

Tactic:
rw [c.prev_eq' hi] at hij

Result:
case neg.hj.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ x, c'.Rel (e.f x) (e.f j)
i : ι
hij : i = j
hi : c.Rel i j
⊢ False

Proof state:
case neg.hj
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ x, c'.Rel (e.f x) (e.f j)
⊢ False

Tactic:
obtain ⟨i, hi⟩ := hj hj'

Result:
case neg.hj.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ x, c'.Rel (e.f x) (e.f j)
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ False

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : c.Rel i j
⊢ c'.prev (e.f j) = e.f i

Tactic:
exact c'.prev_eq' (by simpa only [e.rel_iff] using hij')

Result:
no goals

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hij : c.prev j = j
hij' : ¬c.Rel j j
⊢ c'.prev (e.f j) = e.f j

Tactic:
apply c'.prev_eq_self

Result:
case neg.hj
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hij : c.prev j = j
hij' : ¬c.Rel j j
⊢ ¬c'.Rel (c'.prev (e.f j)) (e.f j)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ x, c'.Rel (e.f x) (e.f j)
i : ι
hij : i = j
hi : c.Rel i j
⊢ c.Rel j j

Tactic:
simpa only [hij] using hi

Result:
no goals

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ c'.prev (e.f j) = e.f i

Tactic:
obtain rfl : j = i := by
  simpa only [c.prev_eq_self j (by simpa only [hij] using hij')] using hij

Result:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hij : c.prev j = j
hij' : ¬c.Rel j j
⊢ c'.prev (e.f j) = e.f j