destruct_eq_think — Mathlib

English

If destruct s equals inr s', then s equals think s'.

Русский

Если destruct s равно inr s', то s = think s'.

LaTeX

$$$\\text{destruct}(s) = \\mathrm{Sum.inr}(s') \\Rightarrow s = \\mathrm{think}(s')$$$

Lean4

theorem destruct_eq_think {s : Computation α} {s'} : destruct s = Sum.inr s' → s = think s' :=
  by
  dsimp [destruct]
  rcases f0 : s.1 0 with - | a' <;> intro h
  · injection h with h'
    rw [← h']
    obtain ⟨f, al⟩ := s
    apply Subtype.eq
    dsimp [think, tail]
    rw [← f0]
    exact (Stream'.eta f).symm
  · contradiction

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