Function normalize_at 

pub fn normalize_at(ctx: &Context, term: &Term, tr: Transparency<'_>) -> Term

The δ-transparency axis (Lean’s TransparencyMode): normalize_at/normalize_checked_at keep an @[irreducible] constant folded with its body intact, while normalize stays the kernel’s own always-unfolding setting. normalize at a chosen transparency. At Transparency::Excluding the named constants keep their bodies and stay FOLDED, which is what @[irreducible] means at Lean’s default transparency; normalize itself is the kernel’s setting and unfolds everything.