-- Mathlib/Order/RelSeries.lean
lemma smash_succ_natAdd {p q : RelSeries r} (h : p.last = q.head) (i : Fin q.length) :
    smash p q h (i.natAdd p.length).succ = q i.succ

Proof state:
case neg.e_a.e_val
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
H : ¬↑(Fin.natAdd p.length i).succ < p.length
⊢ ↑(Fin.natAdd p.length i).succ - p.length = ↑i + 1

Tactic:
simp only [Fin.val_succ, Fin.coe_natAdd]

Result:
case neg.e_a.e_val
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
H : ¬↑(Fin.natAdd p.length i).succ < p.length
⊢ p.length + ↑i + 1 - p.length = ↑i + 1

Proof state:
case neg.e_a.e_val
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
H : ¬↑(Fin.natAdd p.length i).succ < p.length
⊢ p.length + ↑i + 1 - p.length = ↑i + 1

Tactic:
rw [add_assoc, Nat.add_sub_cancel_left]

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ (if H : ↑(Fin.natAdd p.length i).succ < p.length then p.toFun ⟨↑(Fin.natAdd p.length i).succ, ⋯⟩
    else q.toFun ⟨↑(Fin.natAdd p.length i).succ - p.length, ⋯⟩) =
    q.toFun i.succ

Tactic:
split_ifs with H

Result:
case pos
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
H : ↑(Fin.natAdd p.length i).succ < p.length
⊢ p.toFun ⟨↑(Fin.natAdd p.length i).succ, ⋯⟩ = q.toFun i.succ

case neg
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
H : ¬↑(Fin.natAdd p.length i).succ < p.length
⊢ q.toFun ⟨↑(Fin.natAdd p.length i).succ - p.length, ⋯⟩ = q.toFun i.succ

Proof state:
case pos
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
H : ↑(Fin.natAdd p.length i).succ < p.length
⊢ p.toFun ⟨↑(Fin.natAdd p.length i).succ, ⋯⟩ = q.toFun i.succ

Tactic:
have H' : p.length < p.length + (i.1 + 1) := by omega

Result:
case pos
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
H : ↑(Fin.natAdd p.length i).succ < p.length
H' : p.length < p.length + (↑i + 1)
⊢ p.toFun ⟨↑(Fin.natAdd p.length i).succ, ⋯⟩ = q.toFun i.succ

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ (p.smash q h).toFun (Fin.natAdd p.length i).succ = q.toFun i.succ

Tactic:
rw [smash_toFun]

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ (if H : ↑(Fin.natAdd p.length i).succ < p.length then p.toFun ⟨↑(Fin.natAdd p.length i).succ, ⋯⟩
    else q.toFun ⟨↑(Fin.natAdd p.length i).succ - p.length, ⋯⟩) =
    q.toFun i.succ

Proof state:
case pos
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
H : ↑(Fin.natAdd p.length i).succ < p.length
H' : p.length < p.length + (↑i + 1)
⊢ p.toFun ⟨↑(Fin.natAdd p.length i).succ, ⋯⟩ = q.toFun i.succ

Tactic:
exact (lt_irrefl _ (H.trans H')).elim

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
H : ↑(Fin.natAdd p.length i).succ < p.length
⊢ p.length < p.length + (↑i + 1)

Tactic:
omega

Result:
no goals

Proof state:
case neg
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
H : ¬↑(Fin.natAdd p.length i).succ < p.length
⊢ q.toFun ⟨↑(Fin.natAdd p.length i).succ - p.length, ⋯⟩ = q.toFun i.succ

Tactic:
congr

Result:
case neg.e_a.e_val
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
H : ¬↑(Fin.natAdd p.length i).succ < p.length
⊢ ↑(Fin.natAdd p.length i).succ - p.length = ↑i + 1