theorem
let_body_congr
{α : Sort u}
{β : α → Sort v}
{b b' : (a : α) → β a}
(a : α)
(h : ∀ (x : α), b x = b' x)
:
theorem
letFun_body_congr
{α : Sort u}
{β : Sort v}
(a : α)
{f f' : α → β}
(h : ∀ (x : α), f x = f' x)
:
and #
or #
@[reducible, inline, deprecated decide_false (since := "2024-11-05")]
Equations
Instances For
@[reducible, inline, deprecated decide_true (since := "2024-11-05")]