destruct_eq_pure — Mathlib

English

If destruct s equals inl a, then s equals pure a.

Русский

Если destruct s равно inl a, то s равняется pure a.

LaTeX

$$$\\text{destruct}(s) = \\mathrm{Sum.inl}(a) \\Rightarrow s = \\mathrm{pure}(a)$$$

Lean4

theorem destruct_eq_pure {s : Computation α} {a : α} : destruct s = Sum.inl a → s = pure a :=
  by
  dsimp [destruct]
  cases f0 : s.1 0 <;> intro h
  · contradiction
  · apply Subtype.eq
    funext n
    induction n with
    | zero => injection h with h'; rwa [h'] at f0
    | succ n IH => exact s.2 IH

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