English
recENNReal applied to ENNReal via x.toEReal yields the original motive: recENNReal coe neg_coe x.toEReal = coe x.
Русский
recENNReal, применяемый к x.toEReal из ENNReal, возвращает исходный мотив: recENNReal coe neg_coe x.toEReal = coe x.
LaTeX
$$$$\mathrm{recENNReal}\;\bigl(coe, neg\_coe, x^{\mathrm{toEReal}}\bigr) = coe\left(x\right),\quad x \in \mathbb{ENNReal}.$$$$
Lean4
@[simp]
theorem recENNReal_coe_ennreal {motive : EReal → Sort*} (coe : ∀ x : ℝ≥0∞, motive x)
(neg_coe : ∀ x : ℝ≥0∞, 0 < x → motive (-x)) (x : ℝ≥0∞) : recENNReal coe neg_coe x = coe x :=
by
suffices ∀ y : EReal, x = y → (recENNReal coe neg_coe y : motive y) ≍ coe x from heq_iff_eq.mp (this x rfl)
intro y hy
have H₁ : 0 ≤ y := hy ▸ coe_ennreal_nonneg x
obtain rfl : y.toENNReal = x := by simp [← hy]
simp [recENNReal, H₁]
