-- Mathlib/Order/RelSeries.lean
lemma append_apply_right (p q : RelSeries r) (connect : r p.last q.head)
    (i : Fin (q.length + 1)) :
    p.append q connect (i.natAdd p.length + 1) = q i

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ { length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }.toFun
      (↑↑(Fin.natAdd p.length i) + 1) =
    q.toFun i

Tactic:
simp only [Fin.coe_natAdd, Nat.cast_add, Function.comp_apply]

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ Fin.append p.toFun q.toFun (Fin.cast ⋯ (↑(p.length + ↑i) + 1)) = q.toFun i

Proof state:
case h.e'_2.h.e'_6.h.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ ↑(↑(p.length + ↑i) + 1) = p.length + 1 + ↑i

Tactic:
conv_rhs => rw [add_assoc, add_comm 1, ← add_assoc]

Result:
case h.e'_2.h.e'_6.h.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ ↑(↑(p.length + ↑i) + 1) = p.length + ↑i + 1

Proof state:
case h.e'_2.h.e'_6.h.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ ((p.length + ↑i) % (p.length + q.length + 1 + 1) +
        1 %
          ({ length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }.length +
            1)) %
      (p.length + q.length + 1 + 1) =
    p.length + ↑i + 1

Tactic:
simp only [Nat.add_mod_mod, Nat.mod_add_mod, Nat.one_mod, Nat.mod_succ_eq_iff_lt]

Result:
case h.e'_2.h.e'_6.h.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ p.length + ↑i + 1 < (p.length + q.length + 1).succ

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ Fin.append p.toFun q.toFun (Fin.cast ⋯ (↑(p.length + ↑i) + 1)) = q.toFun i

Tactic:
convert Fin.append_right _ _ _

Result:
case h.e'_2.h.e'_6.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ Fin.cast ⋯ (↑(p.length + ↑i) + 1) = Fin.natAdd (p.length + 1) i

Proof state:
case h.e'_2.h.e'_6.h.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ ↑(↑(p.length + ↑i) + 1) = p.length + ↑i + 1

Tactic:
change _ % _ = _

Result:
case h.e'_2.h.e'_6.h.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ ((p.length + ↑i) % (p.length + q.length + 1 + 1) +
        1 %
          ({ length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }.length +
            1)) %
      (p.length + q.length + 1 + 1) =
    p.length + ↑i + 1

Proof state:
case h.e'_2.h.e'_6.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ Fin.cast ⋯ (↑(p.length + ↑i) + 1) = Fin.natAdd (p.length + 1) i

Tactic:
ext

Result:
case h.e'_2.h.e'_6.h.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ ↑(Fin.cast ⋯ (↑(p.length + ↑i) + 1)) = ↑(Fin.natAdd (p.length + 1) i)

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ (p.append q connect).toFun (↑↑(Fin.natAdd p.length i) + 1) = q.toFun i

Tactic:
delta append

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ { length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }.toFun
      (↑↑(Fin.natAdd p.length i) + 1) =
    q.toFun i

Proof state:
case h.e'_2.h.e'_6.h.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ ↑(Fin.cast ⋯ (↑(p.length + ↑i) + 1)) = ↑(Fin.natAdd (p.length + 1) i)

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

Result:
case h.e'_2.h.e'_6.h.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ ↑(↑(p.length + ↑i) + 1) = p.length + 1 + ↑i

Proof state:
case h.e'_2.h.e'_6.h.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (q.length + 1)
⊢ p.length + ↑i + 1 < (p.length + q.length + 1).succ

Tactic:
omega

Result:
no goals