Commit 2024-02-06 10:43 fbec264c
View on Github →refactor(PartialHomeomorph): make (s : Opens \alpha) implicit (#10082)
It is always used in conjunction with a hypothesis hs about s.
In Lean 3, these arguments were kept explicit on purpose: given a definition myDef {x : α} (hx : MyProp x),
if the proof of hx was nontrivial (not a variable), Lean would pretty-print it as myDef _.
In Lean 4, setting pp.proofs.withType or pp.proofs to true makes such terms pretty-print as myDef (x : MyProp).
Hence, this workaround is no longer necessary.
Follow-up to #9894.