tail_congr — Mathlib

English

If s ~ʷ t, then tail s ~ʷ tail t.

Русский

Если s ~ʷ t, то tail s ~ʷ tail t.

LaTeX

$$$\forall s,t\in \mathrm{WSeq}(\alpha),\ s \sim_W t \rightarrow \mathrm{tail}(s) \sim_W \mathrm{tail}(t)$$$

Lean4

theorem tail_congr {s t : WSeq α} (h : s ~ʷ t) : tail s ~ʷ tail t :=
  by
  apply flatten_congr
  dsimp only [(· <$> ·)]; rw [← Computation.bind_pure, ← Computation.bind_pure]
  apply liftRel_bind _ _ (destruct_congr h)
  intro a b h; simp only [comp_apply, liftRel_pure]
  rcases a with - | a <;> rcases b with - | b
  · trivial
  · cases h
  · cases a
    cases h
  · obtain ⟨a, s'⟩ := a
    obtain ⟨b, t'⟩ := b
    exact h.right

Похожие утверждения