fix(*): add missing classical tactics and decidable arguments (#18277)

As discussed in [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60classical.60.20attribute.20leakage/near/282726128), the `classical` tactic is buggy in Mathlib3, and "leaks" into subsequent declarations.

This doesn't port well, as the bug is fixed in lean 4.

This PR installs a temporary hack to contain these leaks, fixes all of the correponding breakages, then reverts the hack.

The result is that the new `classical` tactics in the diff are not needed in Lean 3, but will be needed in Lean 4.

In a future PR, I will try committing the hack itself; but in the meantime, these files are very close to (if not beyond) the port, so the sooner they are fixed the better.

Author: eric-wieser

src/algebra/direct_sum/basic.lean

@@ -230,16 +230,20 @@ noncomputable def sigma_curry : (⨁ (i : Σ i, _), δ i.1 i.2) →+ ⨁ i j, δ
 
 /--The natural map between `⨁ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
 `curry`.-/
-noncomputable def sigma_uncurry : (⨁ i j, δ i j) →+ ⨁ (i : Σ i, _), δ i.1 i.2 :=
+def sigma_uncurry [Π i, decidable_eq (α i)] [Π i j, decidable_eq (δ i j)] :
+  (⨁ i j, δ i j) →+ ⨁ (i : Σ i, _), δ i.1 i.2 :=
 { to_fun := dfinsupp.sigma_uncurry,
   map_zero' := dfinsupp.sigma_uncurry_zero,
   map_add' := dfinsupp.sigma_uncurry_add }
 
-@[simp] lemma sigma_uncurry_apply (f : ⨁ i j, δ i j) (i : ι) (j : α i) :
+@[simp] lemma sigma_uncurry_apply [Π i, decidable_eq (α i)] [Π i j, decidable_eq (δ i j)]
+  (f : ⨁ i j, δ i j) (i : ι) (j : α i) :
   sigma_uncurry f ⟨i, j⟩ = f i j := dfinsupp.sigma_uncurry_apply f i j
 
 /--The natural map between `⨁ (i : Σ i, α i), δ i.1 i.2` and `⨁ i (j : α i), δ i j`.-/
-noncomputable def sigma_curry_equiv : (⨁ (i : Σ i, _), δ i.1 i.2) ≃+ ⨁ i j, δ i j :=
+noncomputable def sigma_curry_equiv
+  [Π i, decidable_eq (α i)] [Π i j, decidable_eq (δ i j)] :
+  (⨁ (i : Σ i, _), δ i.1 i.2) ≃+ ⨁ i j, δ i j :=
 { ..sigma_curry, ..dfinsupp.sigma_curry_equiv }
 
 end sigma

src/algebra/direct_sum/module.lean

@@ -222,15 +222,19 @@ noncomputable def sigma_lcurry : (⨁ (i : Σ i, _), δ i.1 i.2) →ₗ[R] ⨁ i
   sigma_lcurry R f i j = f ⟨i, j⟩ := sigma_curry_apply f i j
 
 /--`uncurry` as a linear map.-/
-noncomputable def sigma_luncurry : (⨁ i j, δ i j) →ₗ[R] ⨁ (i : Σ i, _), δ i.1 i.2 :=
+def sigma_luncurry [Π i, decidable_eq (α i)] [Π i j, decidable_eq (δ i j)] :
+  (⨁ i j, δ i j) →ₗ[R] ⨁ (i : Σ i, _), δ i.1 i.2 :=
 { map_smul' := dfinsupp.sigma_uncurry_smul,
   ..sigma_uncurry }
 
-@[simp] lemma sigma_luncurry_apply (f : ⨁ i j, δ i j) (i : ι) (j : α i) :
+@[simp] lemma sigma_luncurry_apply [Π i, decidable_eq (α i)] [Π i j, decidable_eq (δ i j)]
+  (f : ⨁ i j, δ i j) (i : ι) (j : α i) :
   sigma_luncurry R f ⟨i, j⟩ = f i j := sigma_uncurry_apply f i j
 
 /--`curry_equiv` as a linear equiv.-/
-noncomputable def sigma_lcurry_equiv : (⨁ (i : Σ i, _), δ i.1 i.2) ≃ₗ[R] ⨁ i j, δ i j :=
+noncomputable def sigma_lcurry_equiv
+  [Π i, decidable_eq (α i)] [Π i j, decidable_eq (δ i j)] :
+  (⨁ (i : Σ i, _), δ i.1 i.2) ≃ₗ[R] ⨁ i j, δ i j :=
 { ..sigma_curry_equiv, ..sigma_lcurry R }
 
 end sigma

src/algebra/free_algebra.lean

@@ -344,9 +344,9 @@ map_eq_one_iff (algebra_map _ _) algebra_map_left_inverse.injective
 
 -- this proof is copied from the approach in `free_abelian_group.of_injective`
 lemma ι_injective [nontrivial R] : function.injective (ι R : X → free_algebra R X) :=
-λ x y hoxy, classical.by_contradiction $ assume hxy : x ≠ y,
+λ x y hoxy, classical.by_contradiction $ by classical; exact assume hxy : x ≠ y,
   let f : free_algebra R X →ₐ[R] R :=
-    lift R (λ z, by classical; exact if x = z then (1 : R) else 0) in
+    lift R (λ z, if x = z then (1 : R) else 0) in
   have hfx1 : f (ι R x) = 1, from (lift_ι_apply _ _).trans $ if_pos rfl,
   have hfy1 : f (ι R y) = 1, from hoxy ▸ hfx1,
   have hfy0 : f (ι R y) = 0, from (lift_ι_apply _ _).trans $ if_neg hxy,

src/algebra/module/pid.lean

@@ -213,6 +213,7 @@ begin
     haveI := λ i, is_noetherian_submodule' (torsion_by R N $ p i ^ e i),
     exact λ i, torsion_by_prime_power_decomposition (hp i)
       ((is_torsion'_powers_iff $ p i).mpr $ λ x, ⟨e i, smul_torsion_by _ _⟩) },
+  classical,
   refine ⟨Σ i, fin (this i).some, infer_instance,
     λ ⟨i, j⟩, p i, λ ⟨i, j⟩, hp i, λ ⟨i, j⟩, (this i).some_spec.some j,
     ⟨(linear_equiv.of_bijective (direct_sum.coe_linear_map _) h).symm.trans $

src/algebra/monoid_algebra/basic.lean

@@ -330,7 +330,8 @@ end
 lemma mul_apply_antidiagonal [has_mul G] (f g : monoid_algebra k G) (x : G) (s : finset (G × G))
   (hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x) :
   (f * g) x = ∑ p in s, (f p.1 * g p.2) :=
-let F : G × G → k := λ p, by classical; exact if p.1 * p.2 = x then f p.1 * g p.2 else 0 in
+by classical; exact
+let F : G × G → k := λ p, if p.1 * p.2 = x then f p.1 * g p.2 else 0 in
 calc (f * g) x = (∑ a₁ in f.support, ∑ a₂ in g.support, F (a₁, a₂)) :
   mul_apply f g x
 ... = ∑ p in f.support ×ˢ g.support, F p : finset.sum_product.symm
@@ -477,8 +478,8 @@ end⟩
 also commute with the algebra multiplication. -/
 instance smul_comm_class_self [smul_comm_class R k k] :
   smul_comm_class R (monoid_algebra k G) (monoid_algebra k G) :=
-⟨λ t a b,
-begin
+⟨λ t a b, begin
+  classical,
   ext m,
   simp only [mul_apply, finsupp.sum, finset.smul_sum, smul_ite, mul_smul_comm, sum_smul_index',
     implies_true_iff, eq_self_iff_true, coe_smul, ite_eq_right_iff, smul_eq_mul, pi.smul_apply,

src/algebraic_geometry/elliptic_curve/weierstrass.lean

@@ -433,18 +433,25 @@ instance : is_scalar_tower R R[X] W.coordinate_ring := ideal.quotient.is_scalar_
 
 instance [subsingleton R] : subsingleton W.coordinate_ring := module.subsingleton R[X] _
 
+section
+open_locale classical
 /-- The basis $\{1, Y\}$ for the coordinate ring $R[W]$ over the polynomial ring $R[X]$.
 
 Given a Weierstrass curve `W`, write `W^.coordinate_ring.basis` for this basis. -/
 protected noncomputable def basis : basis (fin 2) R[X] W.coordinate_ring :=
 (subsingleton_or_nontrivial R).by_cases (λ _, by exactI default) $ λ _, by exactI
   (basis.reindex (adjoin_root.power_basis' W.monic_polynomial).basis $
     fin_congr $ W.nat_degree_polynomial)
+end
 
 lemma basis_apply (n : fin 2) :
   W^.coordinate_ring.basis n = (adjoin_root.power_basis' W.monic_polynomial).gen ^ (n : ℕ) :=
-by { nontriviality R, simpa only [coordinate_ring.basis, or.by_cases, dif_neg (not_subsingleton R),
-                                  basis.reindex_apply, power_basis.basis_eq_pow] }
+begin
+  classical,
+  nontriviality R,
+  simpa only [coordinate_ring.basis, or.by_cases, dif_neg (not_subsingleton R),
+                                  basis.reindex_apply, power_basis.basis_eq_pow]
+end
 
 lemma basis_zero : W^.coordinate_ring.basis 0 = 1 := by simpa only [basis_apply] using pow_zero _
 

src/analysis/inner_product_space/orientation.lean

@@ -213,7 +213,8 @@ lemma volume_form_robust (b : orthonormal_basis (fin n) ℝ E) (hb : b.to_basis.
   o.volume_form = b.to_basis.det :=
 begin
   unfreezingI { cases n },
-  { have : o = positive_orientation := hb.symm.trans b.to_basis.orientation_is_empty,
+  { classical,
+    have : o = positive_orientation := hb.symm.trans b.to_basis.orientation_is_empty,
     simp [volume_form, or.by_cases, dif_pos this] },
   { dsimp [volume_form],
     rw [same_orientation_iff_det_eq_det, hb],
@@ -227,7 +228,8 @@ lemma volume_form_robust_neg (b : orthonormal_basis (fin n) ℝ E)
   o.volume_form = - b.to_basis.det :=
 begin
   unfreezingI { cases n },
-  { have : positive_orientation ≠ o := by rwa b.to_basis.orientation_is_empty at hb,
+  { classical,
+    have : positive_orientation ≠ o := by rwa b.to_basis.orientation_is_empty at hb,
     simp [volume_form, or.by_cases, dif_neg this.symm] },
   let e : orthonormal_basis (fin n.succ) ℝ E := o.fin_orthonormal_basis n.succ_pos (fact.out _),
   dsimp [volume_form],
@@ -239,7 +241,7 @@ end
 @[simp] lemma volume_form_neg_orientation : (-o).volume_form = - o.volume_form :=
 begin
   unfreezingI { cases n },
-  { refine o.eq_or_eq_neg_of_is_empty.by_cases _ _; rintros rfl; simp [volume_form_zero_neg] },
+  { refine o.eq_or_eq_neg_of_is_empty.elim _ _; rintros rfl; simp [volume_form_zero_neg] },
   let e : orthonormal_basis (fin n.succ) ℝ E := o.fin_orthonormal_basis n.succ_pos (fact.out _),
   have h₁ : e.to_basis.orientation = o := o.fin_orthonormal_basis_orientation _ _,
   have h₂ : e.to_basis.orientation ≠ -o,
@@ -252,7 +254,7 @@ lemma volume_form_robust' (b : orthonormal_basis (fin n) ℝ E) (v : fin n → E
   |o.volume_form v| = |b.to_basis.det v| :=
 begin
   unfreezingI { cases n },
-  { refine o.eq_or_eq_neg_of_is_empty.by_cases _ _; rintros rfl; simp },
+  { refine o.eq_or_eq_neg_of_is_empty.elim _ _; rintros rfl; simp },
   { rw [o.volume_form_robust (b.adjust_to_orientation o) (b.orientation_adjust_to_orientation o),
       b.abs_det_adjust_to_orientation] },
 end
@@ -263,7 +265,7 @@ value by the product of the norms of the vectors `v i`. -/
 lemma abs_volume_form_apply_le (v : fin n → E) : |o.volume_form v| ≤ ∏ i : fin n, ‖v i‖ :=
 begin
   unfreezingI { cases n },
-  { refine o.eq_or_eq_neg_of_is_empty.by_cases _ _; rintros rfl; simp },
+  { refine o.eq_or_eq_neg_of_is_empty.elim _ _; rintros rfl; simp },
   haveI : finite_dimensional ℝ E := fact_finite_dimensional_of_finrank_eq_succ n,
   have : finrank ℝ E = fintype.card (fin n.succ) := by simpa using _i.out,
   let b : orthonormal_basis (fin n.succ) ℝ E := gram_schmidt_orthonormal_basis this v,
@@ -288,7 +290,7 @@ lemma abs_volume_form_apply_of_pairwise_orthogonal
   |o.volume_form v| = ∏ i : fin n, ‖v i‖ :=
 begin
   unfreezingI { cases n },
-  { refine o.eq_or_eq_neg_of_is_empty.by_cases _ _; rintros rfl; simp },
+  { refine o.eq_or_eq_neg_of_is_empty.elim _ _; rintros rfl; simp },
   haveI : finite_dimensional ℝ E := fact_finite_dimensional_of_finrank_eq_succ n,
   have hdim : finrank ℝ E = fintype.card (fin n.succ) := by simpa using _i.out,
   let b : orthonormal_basis (fin n.succ) ℝ E := gram_schmidt_orthonormal_basis hdim v,
@@ -320,7 +322,7 @@ lemma volume_form_map {F : Type*} [inner_product_space ℝ F] [fact (finrank ℝ
   (orientation.map (fin n) φ.to_linear_equiv o).volume_form x = o.volume_form (φ.symm ∘ x) :=
 begin
   unfreezingI { cases n },
-  { refine o.eq_or_eq_neg_of_is_empty.by_cases _ _; rintros rfl; simp },
+  { refine o.eq_or_eq_neg_of_is_empty.elim _ _; rintros rfl; simp },
   let e : orthonormal_basis (fin n.succ) ℝ E := o.fin_orthonormal_basis n.succ_pos (fact.out _),
   have he : e.to_basis.orientation = o :=
     (o.fin_orthonormal_basis_orientation n.succ_pos (fact.out _)),

src/analysis/inner_product_space/pi_L2.lean

@@ -296,6 +296,7 @@ basis.of_equiv_fun b.repr.to_linear_equiv
 begin
   change ⇑(basis.of_equiv_fun b.repr.to_linear_equiv) = b,
   ext j,
+  classical,
   rw basis.coe_of_equiv_fun,
   congr,
 end
@@ -402,7 +403,7 @@ protected lemma coe_mk (hon : orthonormal 𝕜 v) (hsp: ⊤ ≤ submodule.span 
 by classical; rw [orthonormal_basis.mk, _root_.basis.coe_to_orthonormal_basis, basis.coe_mk]
 
 /-- Any finite subset of a orthonormal family is an `orthonormal_basis` for its span. -/
-protected def span {v' : ι' → E} (h : orthonormal 𝕜 v') (s : finset ι') :
+protected def span [decidable_eq E] {v' : ι' → E} (h : orthonormal 𝕜 v') (s : finset ι') :
   orthonormal_basis s 𝕜 (span 𝕜 (s.image v' : set E)) :=
 let
   e₀' : basis s 𝕜 _ := basis.span (h.linear_independent.comp (coe : s → ι') subtype.coe_injective),
@@ -421,7 +422,8 @@ let
 in
 e₀.map φ.symm
 
-@[simp] protected lemma span_apply {v' : ι' → E} (h : orthonormal 𝕜 v') (s : finset ι') (i : s) :
+@[simp] protected lemma span_apply [decidable_eq E]
+  {v' : ι' → E} (h : orthonormal 𝕜 v') (s : finset ι') (i : s) :
   (orthonormal_basis.span h s i : E) = v' i :=
 by simp only [orthonormal_basis.span, basis.span_apply, linear_isometry_equiv.of_eq_symm,
               orthonormal_basis.map_apply, orthonormal_basis.coe_mk,

src/combinatorics/simple_graph/basic.lean

@@ -606,13 +606,16 @@ attribute [mono] edge_finset_mono edge_finset_strict_mono
 
 @[simp] lemma edge_finset_bot : (⊥ : simple_graph V).edge_finset = ∅ := by simp [edge_finset]
 
-@[simp] lemma edge_finset_sup : (G₁ ⊔ G₂).edge_finset = G₁.edge_finset ∪ G₂.edge_finset :=
+@[simp] lemma edge_finset_sup [decidable_eq V] :
+  (G₁ ⊔ G₂).edge_finset = G₁.edge_finset ∪ G₂.edge_finset :=
 by simp [edge_finset]
 
-@[simp] lemma edge_finset_inf : (G₁ ⊓ G₂).edge_finset = G₁.edge_finset ∩ G₂.edge_finset :=
+@[simp] lemma edge_finset_inf [decidable_eq V] :
+  (G₁ ⊓ G₂).edge_finset = G₁.edge_finset ∩ G₂.edge_finset :=
 by simp [edge_finset]
 
-@[simp] lemma edge_finset_sdiff : (G₁ \ G₂).edge_finset = G₁.edge_finset \ G₂.edge_finset :=
+@[simp] lemma edge_finset_sdiff [decidable_eq V] :
+  (G₁ \ G₂).edge_finset = G₁.edge_finset \ G₂.edge_finset :=
 by simp [edge_finset]
 
 lemma edge_finset_card : G.edge_finset.card = fintype.card G.edge_set := set.to_finset_card _

src/data/dfinsupp/basic.lean

@@ -1221,7 +1221,8 @@ begin
       sigma_curry_apply, smul_apply]
 end
 
-@[simp] lemma sigma_curry_single [Π i j, has_zero (δ i j)] (ij : Σ i, α i) (x : δ ij.1 ij.2) :
+@[simp] lemma sigma_curry_single [decidable_eq ι] [Π i, decidable_eq (α i)]
+  [Π i j, has_zero (δ i j)] (ij : Σ i, α i) (x : δ ij.1 ij.2) :
   @sigma_curry _ _ _ _ (single ij x) = single ij.1 (single ij.2 x : Π₀ j, δ ij.1 j) :=
 begin
   obtain ⟨i, j⟩ := ij,
@@ -1240,7 +1241,8 @@ end
 
 /--The natural map between `Π₀ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
 `curry`.-/
-noncomputable def sigma_uncurry [Π i j, has_zero (δ i j)] (f : Π₀ i j, δ i j) :
+def sigma_uncurry [Π i j, has_zero (δ i j)]
+  [Π i, decidable_eq (α i)] [Π i j (x : δ i j), decidable (x ≠ 0)] (f : Π₀ i j, δ i j) :
   Π₀ (i : Σ i, _), δ i.1 i.2 :=
 { to_fun := λ i, f i.1 i.2,
   support' := f.support'.map $ λ s,
@@ -1255,24 +1257,32 @@ noncomputable def sigma_uncurry [Π i j, has_zero (δ i j)] (f : Π₀ i j, δ i
         rw [hi, zero_apply] }
     end⟩ }
 
-@[simp] lemma sigma_uncurry_apply [Π i j, has_zero (δ i j)] (f : Π₀ i j, δ i j) (i : ι) (j : α i) :
+@[simp] lemma sigma_uncurry_apply [Π i j, has_zero (δ i j)]
+  [Π i, decidable_eq (α i)] [Π i j (x : δ i j), decidable (x ≠ 0)]
+  (f : Π₀ i j, δ i j) (i : ι) (j : α i) :
   sigma_uncurry f ⟨i, j⟩ = f i j :=
 rfl
 
-@[simp] lemma sigma_uncurry_zero [Π i j, has_zero (δ i j)] :
+@[simp] lemma sigma_uncurry_zero [Π i j, has_zero (δ i j)]
+  [Π i, decidable_eq (α i)] [Π i j (x : δ i j), decidable (x ≠ 0)]:
   sigma_uncurry (0 : Π₀ i j, δ i j) = 0 :=
 rfl
 
-@[simp] lemma sigma_uncurry_add [Π i j, add_zero_class (δ i j)] (f g : Π₀ i j, δ i j) :
+@[simp] lemma sigma_uncurry_add [Π i j, add_zero_class (δ i j)]
+  [Π i, decidable_eq (α i)] [Π i j (x : δ i j), decidable (x ≠ 0)]
+  (f g : Π₀ i j, δ i j) :
   sigma_uncurry (f + g) = sigma_uncurry f + sigma_uncurry g :=
 coe_fn_injective rfl
 
 @[simp] lemma sigma_uncurry_smul [monoid γ] [Π i j, add_monoid (δ i j)]
+  [Π i, decidable_eq (α i)] [Π i j (x : δ i j), decidable (x ≠ 0)]
   [Π i j, distrib_mul_action γ (δ i j)] (r : γ) (f : Π₀ i j, δ i j) :
   sigma_uncurry (r • f) = r • sigma_uncurry f :=
 coe_fn_injective rfl
 
-@[simp] lemma sigma_uncurry_single [Π i j, has_zero (δ i j)] (i) (j : α i) (x : δ i j) :
+@[simp] lemma sigma_uncurry_single [Π i j, has_zero (δ i j)]
+  [decidable_eq ι] [Π i, decidable_eq (α i)] [Π i j (x : δ i j), decidable (x ≠ 0)]
+  (i) (j : α i) (x : δ i j) :
   sigma_uncurry (single i (single j x : Π₀ (j : α i), δ i j)) = single ⟨i, j⟩ x:=
 begin
   ext ⟨i', j'⟩,
@@ -1291,7 +1301,8 @@ end
 /--The natural bijection between `Π₀ (i : Σ i, α i), δ i.1 i.2` and `Π₀ i (j : α i), δ i j`.
 
 This is the dfinsupp version of `equiv.Pi_curry`. -/
-noncomputable def sigma_curry_equiv [Π i j, has_zero (δ i j)] :
+noncomputable def sigma_curry_equiv [Π i j, has_zero (δ i j)]
+  [Π i, decidable_eq (α i)] [Π i j (x : δ i j), decidable (x ≠ 0)] :
   (Π₀ (i : Σ i, _), δ i.1 i.2) ≃ Π₀ i j, δ i j :=
 { to_fun := sigma_curry,
   inv_fun := sigma_uncurry,