getLeft_eq_getLeft? — Mathlib

English

If h1 asserts x isLeft and h2 asserts x.getLeft?.isSome, then x.getLeft h1 = x.getLeft? h2.

Русский

Если утверждается, что x является левой частью и естьSome для getLeft?, то получаем равенство значений.

LaTeX

$$$\forall {x : \mathrm{Sum} \ \alpha\ \beta}\\ (h_1 : x.isLeft) (h_2 : x.getLeft?.isSome),\ x.getLeft h_1 = x.getLeft?.get h_2$$

Lean4

theorem getLeft_eq_getLeft? (h₁ : x.isLeft) (h₂ : x.getLeft?.isSome) : x.getLeft h₁ = x.getLeft?.get h₂ := by
  simp [← getLeft?_eq_some_iff]

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