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

Proof state:
case h.e'_3.e_a
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin p.length
H : ¬↑i + 1 < p.length
⊢ i.succ = Fin.last p.length

Tactic:
ext

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

Proof state:
case h.e'_3
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin p.length
H : ¬↑i + 1 < p.length
⊢ p.toFun i.succ = p.last

Tactic:
congr

Result:
case h.e'_3.e_a
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin p.length
H : ¬↑i + 1 < p.length
⊢ i.succ = Fin.last p.length

Proof state:
case h.e'_3.e_a.h
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin p.length
H : ¬↑i + 1 < p.length
⊢ ↑i + 1 = p.length

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 p.length
H : ¬↑(Fin.castAdd q.length i).succ < p.length
⊢ q.toFun ⟨↑(Fin.castAdd q.length i).succ - p.length, ⋯⟩ = p.toFun i.succ

Tactic:
simp only [Fin.val_succ, Fin.coe_castAdd] at H

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

Proof state:
case h.e'_2.e_a.e_val
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin p.length
H : ¬↑i + 1 < p.length
⊢ ↑i + 1 ≤ p.length

Tactic:
omega

Result:
no goals

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

Tactic:
congr

Result:
no goals

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

Tactic:
rw [smash_toFun]

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

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

Tactic:
congr

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

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

Tactic:
change i.1 + 1 = p.length

Result:
case h.e'_3.e_a.h
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin p.length
H : ¬↑i + 1 < p.length
⊢ ↑i + 1 = p.length

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

Tactic:
simp only [Fin.val_succ, Fin.coe_castAdd, Nat.zero_mod, Nat.sub_eq_zero_iff_le]

Result:
case h.e'_2.e_a.e_val
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin p.length
H : ¬↑i + 1 < p.length
⊢ ↑i + 1 ≤ p.length

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

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

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

Tactic:
convert h.symm

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

case h.e'_3
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin p.length
H : ¬↑i + 1 < p.length
⊢ p.toFun i.succ = p.last