fix: remove undercover open Classicals (#23750)

`attribute [local instance] Classical.propDecidable` is much worse than `open scoped Classical`, as it introduces the instance with a default priority that overrides other better decidable instances.

Author: eric-wieser

Archive/Imo/Imo1988Q6.lean

@@ -23,10 +23,6 @@ and apply this to prove Q6 of IMO1988.
 To illustrate the technique, we also prove a similar result.
 -/
 
-
--- open_locale classical
-attribute [local instance] Classical.propDecidable
-
 attribute [local simp] sq
 
 namespace Imo1988Q6

Mathlib/Analysis/NormedSpace/ENormedSpace.lean

@@ -34,7 +34,6 @@ normed space, extended norm
 
 noncomputable section
 
-attribute [local instance] Classical.propDecidable
 set_option linter.deprecated false
 
 open ENNReal
@@ -119,7 +118,7 @@ instance partialOrder : PartialOrder (ENormedSpace 𝕜 V) where
 
 /-- The `ENormedSpace` sending each non-zero vector to infinity. -/
 noncomputable instance : Top (ENormedSpace 𝕜 V) :=
-  ⟨{  toFun := fun x => if x = 0 then 0 else ⊤
+  ⟨{  toFun := fun x => open scoped Classical in if x = 0 then 0 else ⊤
       eq_zero' := fun x => by split_ifs <;> simp [*]
       map_add_le' := fun x y => by
         split_ifs with hxy hx hy hy hx hy hy <;> try simp [*]
@@ -140,7 +139,7 @@ theorem top_map {x : V} (hx : x ≠ 0) : (⊤ : ENormedSpace 𝕜 V) x = ⊤ :=
 
 noncomputable instance : OrderTop (ENormedSpace 𝕜 V) where
   top := ⊤
-  le_top e x := if h : x = 0 then by simp [h] else by simp [top_map h]
+  le_top e x := by obtain h | h := eq_or_ne x 0 <;> simp [top_map, h]
 
 noncomputable instance : SemilatticeSup (ENormedSpace 𝕜 V) :=
   { ENormedSpace.partialOrder with

Mathlib/Data/PFunctor/Univariate/M.lean

@@ -505,9 +505,8 @@ theorem ext_aux [Inhabited (M F)] [DecidableEq F.A] {n : ℕ} (x y z : M F) (hx
 
 open PFunctor.Approx
 
-attribute [local instance] Classical.propDecidable
-
-theorem ext [Inhabited (M F)] (x y : M F) (H : ∀ ps : Path F, iselect ps x = iselect ps y) :
+theorem ext [Inhabited (M F)] [DecidableEq F.A] (x y : M F)
+    (H : ∀ ps : Path F, iselect ps x = iselect ps y) :
     x = y := by
   apply ext'; intro i
   induction' i with i i_ih
@@ -538,7 +537,8 @@ structure IsBisimulation : Prop where
   /-- The tails are equal -/
   tail : ∀ {a} {f f' : F.B a → M F}, M.mk ⟨a, f⟩ ~ M.mk ⟨a, f'⟩ → ∀ i : F.B a, f i ~ f' i
 
-theorem nth_of_bisim [Inhabited (M F)] (bisim : IsBisimulation R) (s₁ s₂) (ps : Path F) :
+theorem nth_of_bisim [Inhabited (M F)] [DecidableEq F.A]
+    (bisim : IsBisimulation R) (s₁ s₂) (ps : Path F) :
     (R s₁ s₂) →
       IsPath ps s₁ ∨ IsPath ps s₂ →
         iselect ps s₁ = iselect ps s₂ ∧
@@ -567,6 +567,7 @@ theorem nth_of_bisim [Inhabited (M F)] (bisim : IsBisimulation R) (s₁ s₂) (p
 
 theorem eq_of_bisim [Nonempty (M F)] (bisim : IsBisimulation R) : ∀ s₁ s₂, R s₁ s₂ → s₁ = s₂ := by
   inhabit M F
+  classical
   introv Hr; apply ext
   introv
   by_cases h : IsPath ps s₁ ∨ IsPath ps s₂

Mathlib/Data/Set/Function.lean

@@ -884,11 +884,10 @@ namespace Function
 
 variable {s : Set α} {f : α → β} {a : α} {b : β}
 
-attribute [local instance] Classical.propDecidable
-
 /-- Construct the inverse for a function `f` on domain `s`. This function is a right inverse of `f`
 on `f '' s`. For a computable version, see `Function.Embedding.invOfMemRange`. -/
 noncomputable def invFunOn [Nonempty α] (f : α → β) (s : Set α) (b : β) : α :=
+  open scoped Classical in
   if h : ∃ a, a ∈ s ∧ f a = b then Classical.choose h else Classical.choice ‹Nonempty α›
 
 variable [Nonempty α]

Mathlib/Logic/Basic.lean

@@ -23,7 +23,6 @@ Classical versions are in the namespace `Classical`.
 -/
 
 open Function
-attribute [local instance 10] Classical.propDecidable
 
 section Miscellany
 
@@ -115,10 +114,12 @@ section Propositional
 alias Iff.imp := imp_congr
 
 -- This is a duplicate of `Classical.imp_iff_right_iff`. Deprecate?
-theorem imp_iff_right_iff {a b : Prop} : (a → b ↔ b) ↔ a ∨ b := Decidable.imp_iff_right_iff
+theorem imp_iff_right_iff {a b : Prop} : (a → b ↔ b) ↔ a ∨ b :=
+  open scoped Classical in Decidable.imp_iff_right_iff
 
 -- This is a duplicate of `Classical.and_or_imp`. Deprecate?
-theorem and_or_imp {a b c : Prop} : a ∧ b ∨ (a → c) ↔ a → b ∨ c := Decidable.and_or_imp
+theorem and_or_imp {a b c : Prop} : a ∧ b ∨ (a → c) ↔ a → b ∨ c :=
+  open scoped Classical in Decidable.and_or_imp
 
 /-- Provide modus tollens (`mt`) as dot notation for implications. -/
 protected theorem Function.mt {a b : Prop} : (a → b) → ¬b → ¬a := mt
@@ -145,10 +146,11 @@ theorem eq_or_ne {α : Sort*} (x y : α) : x = y ∨ x ≠ y := em <| x = y
 
 theorem ne_or_eq {α : Sort*} (x y : α) : x ≠ y ∨ x = y := em' <| x = y
 
-theorem by_contradiction {p : Prop} : (¬p → False) → p := Decidable.byContradiction
+theorem by_contradiction {p : Prop} : (¬p → False) → p :=
+  open scoped Classical in Decidable.byContradiction
 
 theorem by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
-if hp : p then hpq hp else hnpq hp
+  open scoped Classical in if hp : p then hpq hp else hnpq hp
 
 alias by_contra := by_contradiction
 
@@ -181,15 +183,15 @@ theorem of_not_not {a : Prop} : ¬¬a → a := by_contra
 
 theorem not_ne_iff {α : Sort*} {a b : α} : ¬a ≠ b ↔ a = b := not_not
 
-theorem of_not_imp : ¬(a → b) → a := Decidable.of_not_imp
+theorem of_not_imp : ¬(a → b) → a := open scoped Classical in Decidable.of_not_imp
 
 alias Not.decidable_imp_symm := Decidable.not_imp_symm
 
-theorem Not.imp_symm : (¬a → b) → ¬b → a := Not.decidable_imp_symm
+theorem Not.imp_symm : (¬a → b) → ¬b → a := open scoped Classical in Not.decidable_imp_symm
 
-theorem not_imp_comm : ¬a → b ↔ ¬b → a := Decidable.not_imp_comm
+theorem not_imp_comm : ¬a → b ↔ ¬b → a := open scoped Classical in Decidable.not_imp_comm
 
-@[simp] theorem not_imp_self : ¬a → a ↔ a := Decidable.not_imp_self
+@[simp] theorem not_imp_self : ¬a → a ↔ a := open scoped Classical in Decidable.not_imp_self
 
 theorem Imp.swap {a b : Sort*} {c : Prop} : a → b → c ↔ b → a → c :=
   ⟨fun h x y ↦ h y x, fun h x y ↦ h y x⟩
@@ -257,29 +259,31 @@ theorem Or.imp3 {d e c f : Prop} (had : a → d) (hbe : b → e) (hcf : c → f)
 
 export Classical (or_iff_not_imp_left or_iff_not_imp_right)
 
-theorem not_or_of_imp : (a → b) → ¬a ∨ b := Decidable.not_or_of_imp
+theorem not_or_of_imp : (a → b) → ¬a ∨ b := open scoped Classical in Decidable.not_or_of_imp
 
 -- See Note [decidable namespace]
 protected theorem Decidable.or_not_of_imp [Decidable a] (h : a → b) : b ∨ ¬a :=
   dite _ (Or.inl ∘ h) Or.inr
 
-theorem or_not_of_imp : (a → b) → b ∨ ¬a := Decidable.or_not_of_imp
+theorem or_not_of_imp : (a → b) → b ∨ ¬a := open scoped Classical in Decidable.or_not_of_imp
 
-theorem imp_iff_not_or : a → b ↔ ¬a ∨ b := Decidable.imp_iff_not_or
+theorem imp_iff_not_or : a → b ↔ ¬a ∨ b := open scoped Classical in Decidable.imp_iff_not_or
 
-theorem imp_iff_or_not {b a : Prop} : b → a ↔ a ∨ ¬b := Decidable.imp_iff_or_not
+theorem imp_iff_or_not {b a : Prop} : b → a ↔ a ∨ ¬b :=
+  open scoped Classical in Decidable.imp_iff_or_not
 
-theorem not_imp_not : ¬a → ¬b ↔ b → a := Decidable.not_imp_not
+theorem not_imp_not : ¬a → ¬b ↔ b → a := open scoped Classical in Decidable.not_imp_not
 
 theorem imp_and_neg_imp_iff (p q : Prop) : (p → q) ∧ (¬p → q) ↔ q := by simp
 
 /-- Provide the reverse of modus tollens (`mt`) as dot notation for implications. -/
 protected theorem Function.mtr : (¬a → ¬b) → b → a := not_imp_not.mp
 
 theorem or_congr_left' {c a b : Prop} (h : ¬c → (a ↔ b)) : a ∨ c ↔ b ∨ c :=
-  Decidable.or_congr_left' h
+  open scoped Classical in Decidable.or_congr_left' h
 
-theorem or_congr_right' {c : Prop} (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c := Decidable.or_congr_right' h
+theorem or_congr_right' {c : Prop} (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c :=
+  open scoped Classical in Decidable.or_congr_right' h
 
 /-! ### Declarations about distributivity -/
 
@@ -290,39 +294,44 @@ alias Iff.iff := iff_congr
 -- @[simp] -- FIXME simp ignores proof rewrites
 theorem iff_mpr_iff_true_intro {P : Prop} (h : P) : Iff.mpr (iff_true_intro h) True.intro = h := rfl
 
-theorem imp_or {a b c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c) := Decidable.imp_or
+theorem imp_or {a b c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c) :=
+  open scoped Classical in Decidable.imp_or
 
-theorem imp_or' {a : Sort*} {b c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c) := Decidable.imp_or'
+theorem imp_or' {a : Sort*} {b c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c) :=
+  open scoped Classical in Decidable.imp_or'
 
-theorem not_imp : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not
+theorem not_imp : ¬(a → b) ↔ a ∧ ¬b := open scoped Classical in Decidable.not_imp_iff_and_not
 
-theorem peirce (a b : Prop) : ((a → b) → a) → a := Decidable.peirce _ _
+theorem peirce (a b : Prop) : ((a → b) → a) → a := open scoped Classical in Decidable.peirce _ _
 
-theorem not_iff_not : (¬a ↔ ¬b) ↔ (a ↔ b) := Decidable.not_iff_not
+theorem not_iff_not : (¬a ↔ ¬b) ↔ (a ↔ b) := open scoped Classical in Decidable.not_iff_not
 
-theorem not_iff_comm : (¬a ↔ b) ↔ (¬b ↔ a) := Decidable.not_iff_comm
+theorem not_iff_comm : (¬a ↔ b) ↔ (¬b ↔ a) := open scoped Classical in Decidable.not_iff_comm
 
-theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff
+theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := open scoped Classical in Decidable.not_iff
 
-theorem iff_not_comm : (a ↔ ¬b) ↔ (b ↔ ¬a) := Decidable.iff_not_comm
+theorem iff_not_comm : (a ↔ ¬b) ↔ (b ↔ ¬a) := open scoped Classical in Decidable.iff_not_comm
 
 theorem iff_iff_and_or_not_and_not : (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b :=
-  Decidable.iff_iff_and_or_not_and_not
+  open scoped Classical in Decidable.iff_iff_and_or_not_and_not
 
 theorem iff_iff_not_or_and_or_not : (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b) :=
-  Decidable.iff_iff_not_or_and_or_not
+  open scoped Classical in Decidable.iff_iff_not_or_and_or_not
 
-theorem not_and_not_right : ¬(a ∧ ¬b) ↔ a → b := Decidable.not_and_not_right
+theorem not_and_not_right : ¬(a ∧ ¬b) ↔ a → b :=
+  open scoped Classical in Decidable.not_and_not_right
 
 /-! ### De Morgan's laws -/
 
 /-- One of **de Morgan's laws**: the negation of a conjunction is logically equivalent to the
 disjunction of the negations. -/
-theorem not_and_or : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and_iff_not_or_not
+theorem not_and_or : ¬(a ∧ b) ↔ ¬a ∨ ¬b := open scoped Classical in Decidable.not_and_iff_not_or_not
 
-theorem or_iff_not_and_not : a ∨ b ↔ ¬(¬a ∧ ¬b) := Decidable.or_iff_not_not_and_not
+theorem or_iff_not_and_not : a ∨ b ↔ ¬(¬a ∧ ¬b) :=
+  open scoped Classical in Decidable.or_iff_not_not_and_not
 
-theorem and_iff_not_or_not : a ∧ b ↔ ¬(¬a ∨ ¬b) := Decidable.and_iff_not_not_or_not
+theorem and_iff_not_or_not : a ∧ b ↔ ¬(¬a ∨ ¬b) :=
+  open scoped Classical in Decidable.and_iff_not_not_or_not
 
 @[simp] theorem not_xor (P Q : Prop) : ¬Xor' P Q ↔ (P ↔ Q) := by
   simp only [not_and, Xor', not_or, not_not, ← iff_iff_implies_and_implies]
@@ -495,7 +504,8 @@ theorem exists_and_exists_comm {P : α → Prop} {Q : β → Prop} :
 
 export Classical (not_forall)
 
-theorem not_forall_not : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not
+theorem not_forall_not : (¬∀ x, ¬p x) ↔ ∃ x, p x :=
+  open scoped Classical in Decidable.not_forall_not
 
 export Classical (not_exists_not)
 
@@ -507,6 +517,7 @@ lemma exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a :=
 
 theorem forall_imp_iff_exists_imp {α : Sort*} {p : α → Prop} {b : Prop} [ha : Nonempty α] :
     (∀ x, p x) → b ↔ ∃ x, p x → b := by
+  classical
   let ⟨a⟩ := ha
   refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
   exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (_root_.not_imp.1 (h' x)).1
@@ -531,7 +542,7 @@ theorem Decidable.and_forall_ne [DecidableEq α] (a : α) {p : α → Prop} :
   simp only [← @forall_eq _ p a, ← forall_and, ← or_imp, Decidable.em, forall_const]
 
 theorem and_forall_ne (a : α) : (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b :=
-  Decidable.and_forall_ne a
+  open scoped Classical in Decidable.and_forall_ne a
 
 theorem Ne.ne_or_ne {x y : α} (z : α) (h : x ≠ y) : x ≠ z ∨ y ≠ z :=
   not_and_or.1 <| mt (and_imp.2 (· ▸ ·)) h.symm
@@ -610,14 +621,14 @@ protected theorem Decidable.forall_or_left {q : Prop} {p : α → Prop} [Decidab
     Or.inr fun x ↦ (h x).resolve_left hq, forall_or_of_or_forall⟩
 
 theorem forall_or_left {q} {p : α → Prop} : (∀ x, q ∨ p x) ↔ q ∨ ∀ x, p x :=
-  Decidable.forall_or_left
+  open scoped Classical in Decidable.forall_or_left
 
 -- See Note [decidable namespace]
 protected theorem Decidable.forall_or_right {q} {p : α → Prop} [Decidable q] :
     (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q := by simp [or_comm, Decidable.forall_or_left]
 
 theorem forall_or_right {q} {p : α → Prop} : (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q :=
-  Decidable.forall_or_right
+  open scoped Classical in Decidable.forall_or_right
 
 theorem Exists.fst {b : Prop} {p : b → Prop} : Exists p → b
   | ⟨h, _⟩ => h
@@ -775,7 +786,8 @@ protected theorem Decidable.not_forall₂ [Decidable (∃ x h, ¬P x h)] [∀ x
   ⟨Not.decidable_imp_symm fun nx x h ↦ nx.decidable_imp_symm
     fun h' ↦ ⟨x, h, h'⟩, not_forall₂_of_exists₂_not⟩
 
-theorem not_forall₂ : (¬∀ x h, P x h) ↔ ∃ x h, ¬P x h := Decidable.not_forall₂
+theorem not_forall₂ : (¬∀ x h, P x h) ↔ ∃ x h, ¬P x h :=
+  open scoped Classical in Decidable.not_forall₂
 
 theorem forall₂_and : (∀ x h, P x h ∧ Q x h) ↔ (∀ x h, P x h) ∧ ∀ x h, Q x h :=
   Iff.trans (forall_congr' fun _ ↦ forall_and) forall_and
@@ -948,9 +960,9 @@ end ite
 theorem not_beq_of_ne {α : Type*} [BEq α] [LawfulBEq α] {a b : α} (ne : a ≠ b) : ¬(a == b) :=
   fun h => ne (eq_of_beq h)
 
-theorem beq_eq_decide {α : Type*} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = decide (a = b) := by
-  rw [← beq_iff_eq (a := a) (b := b)]
-  cases a == b <;> simp
+theorem beq_eq_decide {α : Type*} [BEq α] [LawfulBEq α] {a b : α} [Decidable (a = b)] :
+    (a == b) = decide (a = b) := by
+  by_cases a = b <;> simp_all [beq_iff_eq]
 
 @[simp] lemma beq_eq_beq {α β : Type*} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {a₁ a₂ : α}
     {b₁ b₂ : β} : (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂) := by rw [Bool.eq_iff_iff]; simp
@@ -970,4 +982,5 @@ theorem lawful_beq_subsingleton {α : Type*} (inst1 : BEq α) (inst2 : BEq α)
     inst1 = inst2 := by
   apply beq_ext
   intro x y
+  classical
   simp only [beq_eq_decide]