Commit 2026-09-17 12:30 4abb71fe

chore(Basic/Logic): deduplicate Prop.exists and Prop.forall (#43381) Claude picked up on Prop.exists and Prop.exists_iff, as well as Prop.forall and Prop.forall_iff, being duplicates (up to reordering on the RHS). In deprecating, we've decided to keep the statement, proof and location of Prop.exists_iff and Prop.forall_iff:

• Statement: I couldn't find justification for choosing one or the other, so this choice is arbitrary.
• Location: We keep the earlier location out of necessity.
• Proof: The selected proof allows us to avoid importing Mathlib.Tactic.Convert. For the name, we went with Prop.exists and Prop.forall, since the naming convention isn't clear on the _iff suffix being needed.