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

…8277)

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.

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,

src/data/finsupp/alist.lean

@@ -91,6 +91,7 @@ by { classical, simp [←alist.insert_empty] }
 @[simp] lemma _root_.finsupp.to_alist_lookup_finsupp (f : α →₀ M) : f.to_alist.lookup_finsupp = f :=
 begin
   ext,
+  classical,
   by_cases h : f a = 0,
   { suffices : f.to_alist.lookup a = none,
     { simp [h, this] },

src/data/finsupp/basic.lean

@@ -901,7 +901,7 @@ prod_bij (λp _, p.val)
   (λ _, by classical; exact mem_subtype.1)
   (λ _ _, rfl)
   (λ _ _ _ _, subtype.eq)
-  (λ b hb, ⟨⟨b, hp b hb⟩, mem_subtype.2 hb, rfl⟩)
+  (λ b hb, ⟨⟨b, hp b hb⟩, by classical; exact mem_subtype.2 hb, rfl⟩)
 
 end zero
 

src/data/finsupp/defs.lean

@@ -222,21 +222,21 @@ def single (a : α) (b : M) : α →₀ M :=
   end }
 
 lemma single_apply [decidable (a = a')] : single a b a' = if a = a' then b else 0 :=
-by { simp_rw [@eq_comm _ a a'], convert pi.single_apply _ _ _, }
+by { classical, simp_rw [@eq_comm _ a a'], convert pi.single_apply _ _ _, }
 
 lemma single_apply_left {f : α → β} (hf : function.injective f)
   (x z : α) (y : M) :
   single (f x) y (f z) = single x y z :=
-by simp only [single_apply, hf.eq_iff]
+by { classical, simp only [single_apply, hf.eq_iff] }
 
 lemma single_eq_indicator : ⇑(single a b) = set.indicator {a} (λ _, b) :=
-by { ext, simp [single_apply, set.indicator, @eq_comm _ a] }
+by { classical, ext, simp [single_apply, set.indicator, @eq_comm _ a] }
 
 @[simp] lemma single_eq_same : (single a b : α →₀ M) a = b :=
-pi.single_eq_same a b
+by { classical, exact pi.single_eq_same a b }
 
 @[simp] lemma single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ M) a' = 0 :=
-pi.single_eq_of_ne' h _
+by { classical, exact pi.single_eq_of_ne' h _ }
 
 lemma single_eq_update [decidable_eq α] (a : α) (b : M) : ⇑(single a b) = function.update 0 a b :=
 by rw [single_eq_indicator, ← set.piecewise_eq_indicator, set.piecewise_singleton]
@@ -245,12 +245,15 @@ lemma single_eq_pi_single [decidable_eq α] (a : α) (b : M) : ⇑(single a b) =
 single_eq_update a b
 
 @[simp] lemma single_zero (a : α) : (single a 0 : α →₀ M) = 0 :=
-coe_fn_injective $ by simpa only [single_eq_update, coe_zero]
-  using function.update_eq_self a (0 : α → M)
+coe_fn_injective $ begin
+  classical,
+  simpa only [single_eq_update, coe_zero] using function.update_eq_self a (0 : α → M)
+end
 
 lemma single_of_single_apply (a a' : α) (b : M) :
   single a ((single a' b) a) = single a' (single a' b) a :=
 begin
+  classical,
   rw [single_apply, single_apply],
   ext,
   split_ifs,
@@ -259,10 +262,10 @@ begin
 end
 
 lemma support_single_ne_zero (a : α) (hb : b ≠ 0) : (single a b).support = {a} :=
-if_neg hb
+by { classical, exact if_neg hb }
 
 lemma support_single_subset : (single a b).support ⊆ {a} :=
-show ite _ _ _ ⊆ _, by split_ifs; [exact empty_subset _, exact subset.refl _]
+by { classical, show ite _ _ _ ⊆ _, split_ifs; [exact empty_subset _, exact subset.refl _] }
 
 lemma single_apply_mem (x) : single a b x ∈ ({0, b} : set M) :=
 by rcases em (a = x) with (rfl|hx); [simp, simp [single_eq_of_ne hx]]
@@ -334,7 +337,7 @@ by rw [support_single_ne_zero _ hb, support_single_ne_zero _ hb', disjoint_singl
 by simp [ext_iff, single_eq_indicator]
 
 lemma single_swap (a₁ a₂ : α) (b : M) : single a₁ b a₂ = single a₂ b a₁ :=
-by simp only [single_apply]; ac_refl
+by { classical, simp only [single_apply], ac_refl }
 
 instance [nonempty α] [nontrivial M] : nontrivial (α →₀ M) :=
 begin

src/data/finsupp/to_dfinsupp.lean

@@ -257,6 +257,7 @@ begin
   suffices : finsupp.single (⟨i, a⟩ : Σ i, η i) n ⟨j, b⟩ = 0,
   { simp [split_apply, dif_neg h, this] },
   have H : (⟨i, a⟩ : Σ i, η i) ≠ ⟨j, b⟩ := by simp [h],
+  classical,
   rw [finsupp.single_apply, if_neg H]
 end
 

src/data/fintype/basic.lean

@@ -756,7 +756,7 @@ noncomputable def finset_equiv_set [fintype α] : finset α ≃ set α :=
 { to_fun := coe,
   inv_fun := by { classical, exact λ s, s.to_finset },
   left_inv := λ s, by convert finset.to_finset_coe s,
-  right_inv := λ s, s.coe_to_finset }
+  right_inv := λ s, by { classical, exact s.coe_to_finset } }
 
 @[simp] lemma finset_equiv_set_apply [fintype α] (s : finset α) : finset_equiv_set s = s := rfl