desc'_inr — Mathlib

English

If i = Sum.inr i2, then ac.desc' x1 x2 i equals desc.aux with the appropriate argument and x2 i2.

Русский

Если i равняется Sum.inr i2, то ac.desc' x1 x2 i равно desc.aux с соответствующим аргументом и x2 i2.

LaTeX

$$$\text{If } i = \mathrm{Sum.inr}(i_2),\ ac.desc'\,x_1\,x_2\,i = \mathrm{desc.aux}\, X\,\ldots\, (\text{proof})\,(x_2(i_2)).$$$

Lean4

theorem desc'_inr (i : ι₁ ⊕ ι₂) (i₂ : ι₂) (h : Sum.inr i₂ = i) :
    ac.desc' x₁ x₂ i = desc.aux _ _ _ (by subst h; simp) (x₂ i₂) := by subst h; rfl

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