chore: prefer classical over open scoped Classical in proofs

Mathlib/Logic/Basic.lean

@@ -223,11 +223,13 @@ 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 :=
-  open scoped Classical in Decidable.byContradiction
+theorem by_contradiction {p : Prop} : (¬p → False) → p := by
+  classical
+  exact Decidable.byContradiction
 
-theorem by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
-  open scoped Classical in if hp : p then hpq hp else hnpq hp
+theorem by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q := by
+  classical
+  exact if hp : p then hpq hp else hnpq hp
 
 alias by_contra := by_contradiction
 
@@ -262,15 +264,23 @@ 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 := open scoped Classical in Decidable.of_not_imp
+theorem of_not_imp : ¬(a → b) → a := by
+  classical
+  exact Decidable.of_not_imp
 
 alias Not.decidable_imp_symm := Decidable.not_imp_symm
 
-theorem Not.imp_symm : (¬a → b) → ¬b → a := open scoped Classical in Not.decidable_imp_symm
+theorem Not.imp_symm : (¬a → b) → ¬b → a := by
+  classical
+  exact Not.decidable_imp_symm
 
-theorem not_imp_comm : ¬a → b ↔ ¬b → a := open scoped Classical in Decidable.not_imp_comm
+theorem not_imp_comm : ¬a → b ↔ ¬b → a := by
+  classical
+  exact Decidable.not_imp_comm
 
-@[simp] theorem not_imp_self : ¬a → a ↔ a := open scoped Classical in Decidable.not_imp_self
+@[simp] theorem not_imp_self : ¬a → a ↔ a := by
+  classical
+  exact 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⟩
@@ -344,20 +354,29 @@ 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 := open scoped Classical in Decidable.not_or_of_imp
+theorem not_or_of_imp : (a → b) → ¬a ∨ b := by
+  classical
+  exact 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 := open scoped Classical in Decidable.or_not_of_imp
+theorem or_not_of_imp : (a → b) → b ∨ ¬a := by
+  classical
+  exact Decidable.or_not_of_imp
 
-theorem imp_iff_not_or : a → b ↔ ¬a ∨ b := open scoped Classical in Decidable.imp_iff_not_or
+theorem imp_iff_not_or : a → b ↔ ¬a ∨ b := by
+  classical
+  exact Decidable.imp_iff_not_or
 
-theorem imp_iff_or_not {b a : Prop} : b → a ↔ a ∨ ¬b :=
-  open scoped Classical in Decidable.imp_iff_or_not
+theorem imp_iff_or_not {b a : Prop} : b → a ↔ a ∨ ¬b := by
+  classical
+  exact Decidable.imp_iff_or_not
 
-theorem not_imp_not : ¬a → ¬b ↔ b → a := open scoped Classical in Decidable.not_imp_not
+theorem not_imp_not : ¬a → ¬b ↔ b → a := by
+  classical
+  exact Decidable.not_imp_not
 
 @[deprecated Classical.imp_and_neg_imp_iff (since := "2026-01-30")]
 theorem imp_and_neg_imp_iff (p q : Prop) : (p → q) ∧ (¬p → q) ↔ q :=
@@ -366,11 +385,13 @@ theorem imp_and_neg_imp_iff (p q : Prop) : (p → q) ∧ (¬p → q) ↔ q :=
 /-- 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 :=
-  open scoped Classical in Decidable.or_congr_left' h
+theorem or_congr_left' {c a b : Prop} (h : ¬c → (a ↔ b)) : a ∨ c ↔ b ∨ c := by
+  classical
+  exact Decidable.or_congr_left' h
 
-theorem or_congr_right' {c : Prop} (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c :=
-  open scoped Classical in Decidable.or_congr_right' h
+theorem or_congr_right' {c : Prop} (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c := by
+  classical
+  exact Decidable.or_congr_right' h
 
 /-! ### Declarations about distributivity -/
 
@@ -381,44 +402,63 @@ 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) :=
-  open scoped Classical in Decidable.imp_or
+theorem imp_or {a b c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c) := by
+  classical
+  exact 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 imp_or' {a : Sort*} {b c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c) := by
+  classical
+  exact Decidable.imp_or'
 
 @[deprecated (since := "2026-01-30")] alias not_imp := Classical.not_imp
 
-theorem peirce (a b : Prop) : ((a → b) → a) → a := open scoped Classical in Decidable.peirce _ _
+theorem peirce (a b : Prop) : ((a → b) → a) → a := by
+  classical
+  exact Decidable.peirce _ _
 
-theorem not_iff_not : (¬a ↔ ¬b) ↔ (a ↔ b) := open scoped Classical in Decidable.not_iff_not
+theorem not_iff_not : (¬a ↔ ¬b) ↔ (a ↔ b) := by
+  classical
+  exact Decidable.not_iff_not
 
-theorem not_iff_comm : (¬a ↔ b) ↔ (¬b ↔ a) := open scoped Classical in Decidable.not_iff_comm
+theorem not_iff_comm : (¬a ↔ b) ↔ (¬b ↔ a) := by
+  classical
+  exact Decidable.not_iff_comm
 
-theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := open scoped Classical in Decidable.not_iff
+theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := by
+  classical
+  exact Decidable.not_iff
 
-theorem iff_not_comm : (a ↔ ¬b) ↔ (b ↔ ¬a) := open scoped Classical in Decidable.iff_not_comm
+theorem iff_not_comm : (a ↔ ¬b) ↔ (b ↔ ¬a) := by
+  classical
+  exact Decidable.iff_not_comm
 
-theorem iff_iff_and_or_not_and_not : (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b :=
-  open scoped Classical in Decidable.iff_iff_and_or_not_and_not
+theorem iff_iff_and_or_not_and_not : (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b := by
+  classical
+  exact Decidable.iff_iff_and_or_not_and_not
 
-theorem iff_iff_not_or_and_or_not : (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b) :=
-  open scoped Classical in Decidable.iff_iff_not_or_and_or_not
+theorem iff_iff_not_or_and_or_not : (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b) := by
+  classical
+  exact Decidable.iff_iff_not_or_and_or_not
 
-theorem not_and_not_right : ¬(a ∧ ¬b) ↔ a → b :=
-  open scoped Classical in Decidable.not_and_not_right
+theorem not_and_not_right : ¬(a ∧ ¬b) ↔ a → b := by
+  classical
+  exact 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 := open scoped Classical in Decidable.not_and_iff_not_or_not
+theorem not_and_or : ¬(a ∧ b) ↔ ¬a ∨ ¬b := by
+  classical
+  exact Decidable.not_and_iff_not_or_not
 
-theorem or_iff_not_and_not : a ∨ b ↔ ¬(¬a ∧ ¬b) :=
-  open scoped Classical in Decidable.or_iff_not_not_and_not
+theorem or_iff_not_and_not : a ∨ b ↔ ¬(¬a ∧ ¬b) := by
+  classical
+  exact Decidable.or_iff_not_not_and_not
 
-theorem and_iff_not_or_not : a ∧ b ↔ ¬(¬a ∨ ¬b) :=
-  open scoped Classical in Decidable.and_iff_not_not_or_not
+theorem and_iff_not_or_not : a ∧ b ↔ ¬(¬a ∨ ¬b) := by
+  classical
+  exact 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]
@@ -559,8 +599,9 @@ theorem exists_and_exists_comm {P : α → Prop} {Q : β → Prop} :
 
 export Classical (not_forall)
 
-theorem not_forall_not : (¬∀ x, ¬p x) ↔ ∃ x, p x :=
-  open scoped Classical in Decidable.not_forall_not
+theorem not_forall_not : (¬∀ x, ¬p x) ↔ ∃ x, p x := by
+  classical
+  exact Decidable.not_forall_not
 
 export Classical (not_exists_not)
 
@@ -596,8 +637,9 @@ theorem Decidable.and_forall_ne [DecidableEq α] (a : α) {p : α → Prop} :
     (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b := by
   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 :=
-  open scoped Classical in Decidable.and_forall_ne a
+theorem and_forall_ne (a : α) : (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b := by
+  classical
+  exact 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
@@ -675,15 +717,17 @@ protected theorem Decidable.forall_or_left {q : Prop} {p : α → Prop} [Decidab
   ⟨fun h ↦ if hq : q then Or.inl hq else
     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 :=
-  open scoped Classical in Decidable.forall_or_left
+theorem forall_or_left {q} {p : α → Prop} : (∀ x, q ∨ p x) ↔ q ∨ ∀ x, p x := by
+  classical
+  exact 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 :=
-  open scoped Classical in Decidable.forall_or_right
+theorem forall_or_right {q} {p : α → Prop} : (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q := by
+  classical
+  exact Decidable.forall_or_right
 
 @[simp]
 theorem forall_and_index {p q : Prop} {r : p ∧ q → Prop} :
@@ -865,8 +909,9 @@ 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 :=
-  open scoped Classical in Decidable.not_forall₂
+theorem not_forall₂ : (¬∀ x h, P x h) ↔ ∃ x h, ¬P x h := by
+  classical
+  exact 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

Mathlib/Logic/Function/Basic.lean

@@ -885,8 +885,9 @@ lemma factorsThrough_iff (g : α → γ) [Nonempty γ] : g.FactorsThrough f ↔
   fun h _ _ hf => by rw [Classical.choose_spec h, comp_apply, comp_apply, hf]⟩
 
 lemma apply_extend {δ} {g : α → γ} (F : γ → δ) (f : α → β) (e' : β → γ) (b : β) :
-    F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b :=
-  open scoped Classical in apply_dite F _ _ _
+    F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b := by
+  classical
+  exact apply_dite F _ _ _
 
 theorem extend_injective (hf : Injective f) (e' : β → γ) : Injective fun g ↦ extend f g e' := by
   intro g₁ g₂ hg
@@ -900,8 +901,9 @@ lemma FactorsThrough.extend_comp {g : α → γ} (e' : β → γ) (hf : FactorsT
   funext fun a => hf.extend_apply e' a
 
 @[simp]
-lemma extend_const (f : α → β) (c : γ) : extend f (fun _ ↦ c) (fun _ ↦ c) = fun _ ↦ c :=
-  funext fun _ ↦ open scoped Classical in ite_id _
+lemma extend_const (f : α → β) (c : γ) : extend f (fun _ ↦ c) (fun _ ↦ c) = fun _ ↦ c := by
+  classical
+  exact funext fun _ ↦ ite_id _
 
 @[simp]
 theorem extend_comp (hf : Injective f) (g : α → γ) (e' : β → γ) : extend f g e' ∘ f = g :=

Mathlib/Order/Basic.lean

@@ -257,8 +257,9 @@ protected theorem Decidable.eq_iff_le_not_lt [DecidableLE α] : a = b ↔ a ≤
     h₁.antisymm <| Decidable.byContradiction fun h₃ ↦ h₂ (h₁.lt_of_not_ge h₃)⟩
 
 @[to_dual eq_iff_ge_not_gt]
-theorem eq_iff_le_not_lt : a = b ↔ a ≤ b ∧ ¬a < b := open scoped Classical in
-  Decidable.eq_iff_le_not_lt
+theorem eq_iff_le_not_lt : a = b ↔ a ≤ b ∧ ¬a < b := by
+  classical
+  exact Decidable.eq_iff_le_not_lt
 
 -- See Note [decidable namespace]
 @[to_dual eq_or_lt_of_le']
@@ -290,8 +291,9 @@ protected theorem Decidable.ne_iff_lt_iff_le [DecidableEq α] : (a ≠ b ↔ a <
   ⟨fun h ↦ Decidable.byCases le_of_eq (le_of_lt ∘ h.mp), fun h ↦ ⟨lt_of_le_of_ne h, ne_of_lt⟩⟩
 
 @[to_dual (attr := simp) ne_iff_gt_iff_ge]
-theorem ne_iff_lt_iff_le : (a ≠ b ↔ a < b) ↔ a ≤ b := open scoped Classical in
-  Decidable.ne_iff_lt_iff_le
+theorem ne_iff_lt_iff_le : (a ≠ b ↔ a < b) ↔ a ≤ b := by
+  classical
+  exact Decidable.ne_iff_lt_iff_le
 
 @[to_dual eq_of_forall_ge_iff]
 lemma eq_of_forall_le_iff (H : ∀ c, c ≤ a ↔ c ≤ b) : a = b :=

Mathlib/Order/Defs/PartialOrder.lean

@@ -221,8 +221,12 @@ protected lemma Decidable.le_iff_lt_or_eq [DecidableLE α] : a ≤ b ↔ a < b 
   ⟨Decidable.lt_or_eq_of_le, le_of_lt_or_eq⟩
 
 @[to_dual lt_or_eq_of_le']
-lemma lt_or_eq_of_le : a ≤ b → a < b ∨ a = b := open scoped Classical in Decidable.lt_or_eq_of_le
+lemma lt_or_eq_of_le : a ≤ b → a < b ∨ a = b := by
+  classical
+  exact Decidable.lt_or_eq_of_le
 @[to_dual le_iff_lt_or_eq']
-lemma le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b := open scoped Classical in Decidable.le_iff_lt_or_eq
+lemma le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b := by
+  classical
+  exact Decidable.le_iff_lt_or_eq
 
 end PartialOrder