English
For p, q and a connecting edge, the i-th element at the left side of (p ⧺ q) equals p i for i in the left range.
Русский
Для p, q и соединения, i-й элемент слева в (p ⧺ q) равен p i на левой части.
LaTeX
$$$ (p \\append q \\;\\text{connect})_{i} = p_{i} \\quad\\text{for } i < p.length + 1 $$$
Lean4
/-- If `a₀ -r→ a₁ -r→ ... -r→ aₙ` is an `r`-series and `a` is such that
`aᵢ -r→ a -r→ a_ᵢ₊₁`, then
`a₀ -r→ a₁ -r→ ... -r→ aᵢ -r→ a -r→ aᵢ₊₁ -r→ ... -r→ aₙ`
is another `r`-series
-/
@[simps]
def insertNth (p : RelSeries r) (i : Fin p.length) (a : α) (prev_connect : p (Fin.castSucc i) ~[r] a)
(connect_next : a ~[r] p i.succ) : RelSeries r
where
length := p.length + 1
toFun := (Fin.castSucc i.succ).insertNth a p
step
m := by
set x := _; set y := _; change x ~[r] y
obtain hm | hm | hm := lt_trichotomy m.1 i.1
· convert p.step ⟨m, hm.trans i.2⟩
· change Fin.insertNth _ _ _ _ = _
rw [Fin.insertNth_apply_below]
pick_goal 2
· exact hm.trans (lt_add_one _)
simp
· change Fin.insertNth _ _ _ _ = _
rw [Fin.insertNth_apply_below]
pick_goal 2
· change m.1 + 1 < i.1 + 1; rwa [add_lt_add_iff_right]
simp; rfl
· rw [show x = p m from
show Fin.insertNth _ _ _ _ = _ by
rw [Fin.insertNth_apply_below]
pick_goal 2
· change m.1 < i.1 + 1; exact hm ▸ lt_add_one _
simp]
convert prev_connect
· ext; exact hm
· change Fin.insertNth _ _ _ _ = _
rw [show m.succ = i.succ.castSucc by ext; change _ + 1 = _ + 1; rw [hm], Fin.insertNth_apply_same]
· rw [Nat.lt_iff_add_one_le, le_iff_lt_or_eq] at hm
obtain hm | hm := hm
· convert p.step ⟨m.1 - 1, Nat.sub_lt_right_of_lt_add (by omega) m.2⟩
· change Fin.insertNth _ _ _ _ = _
rw [Fin.insertNth_apply_above (h := hm)]
aesop
· change Fin.insertNth _ _ _ _ = _
rw [Fin.insertNth_apply_above]
swap
· exact hm.trans (lt_add_one _)
simp only [Fin.pred_succ, eq_rec_constant, Fin.succ_mk]
congr
exact Fin.ext <| Eq.symm <| Nat.succ_pred_eq_of_pos (lt_trans (Nat.zero_lt_succ _) hm)
· convert connect_next
· change Fin.insertNth _ _ _ _ = _
rw [show m.castSucc = i.succ.castSucc from Fin.ext hm.symm, Fin.insertNth_apply_same]
· change Fin.insertNth _ _ _ _ = _
rw [Fin.insertNth_apply_above]
swap
· change i.1 + 1 < m.1 + 1; omega
simp only [Fin.pred_succ, eq_rec_constant]
congr; ext; exact hm.symm
