snd_inr — Mathlib

English

The second projection applied to the right injection recovers the original element: snd(inr(x)) = x.

Русский

Вторую проекцию после правой инекции получаем исходный элемент: snd(inr(x)) = x.

LaTeX

$$$\mathrm{snd}(\mathrm{inr}(x)) = x$$$

Lean4

@[simp]
theorem snd_inr [DecidablePred fun x : H₀ ↦ x = 0] (x : H₀) : snd _ _ (inr G₀ _ x) = x := by
  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;> simp [WithZero.withZeroUnitsEquiv, snd, inr]

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