Post #4445803

@mjd@mathstodon.xyz if the headline theorem talks about foozles and the mathlib definition of a foozle is wrong, then you've proved the wrong theorem. But the incorrect definition of foozle is only used in some intermediate lemmas, and is used consistently, then you have a correct overall proof.