Def Mathlib.Tactic.Translate.declUnfoldSimpAuxLemmas

Modification history

2026-01-09 10:48

Mathlib/Tactic/Translate/Core.lean

fix(translate): don't unfold aux lemmas, but translate them (#33603) …

Added Mathlib.Tactic.Translate.declUnfoldSimpAuxLemmas View on Github →