chore: remove unused Decidable* instances in theorem types (#31831)

This PR removes `Decidable*` instances that are not used by the remainder of a theorem's type and so can be replaced by `classical` in the proof (found by the  #31142). This allows us to turn on the `unusedDecidableInType` linter, which is done in #31747.

Notes:

- We rearrange the order of theorems slightly in [Mathlib/Combinatorics/SimpleGraph/Bipartite.lean](https://github.com/leanprover-community/mathlib4/pull/31747/files#diff-8acbd485d15b1e94a2afaf205ebedba12259361421342c715188192f1b0045f8) in order to put the ones that do require `DecidableRel` in a section.
- [lean4#5565](leanprover/lean4#5595) forces us to change two `instance`s to `@[instance] theorem` because of a failure in `omit`. We preserve the autogenerated name here.

Co-authored-by: thorimur <thomasmurrills@gmail.com>

Author: thorimur

Archive/Wiedijk100Theorems/Partition.lean

@@ -97,11 +97,11 @@ theorem coeff_indicator (s : Set ℕ) [Semiring α] (n : ℕ) [Decidable (n ∈
     coeff n (indicatorSeries α s) = if n ∈ s then 1 else 0 := by
   convert coeff_mk _ _
 
-theorem coeff_indicator_pos (s : Set ℕ) [Semiring α] (n : ℕ) (h : n ∈ s) [Decidable (n ∈ s)] :
-    coeff n (indicatorSeries α s) = 1 := by rw [coeff_indicator, if_pos h]
+theorem coeff_indicator_pos (s : Set ℕ) [Semiring α] (n : ℕ) (h : n ∈ s) :
+    coeff n (indicatorSeries α s) = 1 := by classical rw [coeff_indicator, if_pos h]
 
-theorem coeff_indicator_neg (s : Set ℕ) [Semiring α] (n : ℕ) (h : n ∉ s) [Decidable (n ∈ s)] :
-    coeff n (indicatorSeries α s) = 0 := by rw [coeff_indicator, if_neg h]
+theorem coeff_indicator_neg (s : Set ℕ) [Semiring α] (n : ℕ) (h : n ∉ s) :
+    coeff n (indicatorSeries α s) = 0 := by classical rw [coeff_indicator, if_neg h]
 
 theorem constantCoeff_indicator (s : Set ℕ) [Semiring α] [Decidable (0 ∈ s)] :
     constantCoeff (indicatorSeries α s) = if 0 ∈ s then 1 else 0 := by

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -956,7 +956,7 @@ open Associates
 
 variable [CancelCommMonoidWithZero α]
 
-private theorem map_mk_unit_aux [DecidableEq α] {f : Associates α →* α}
+private theorem map_mk_unit_aux {f : Associates α →* α}
     (hinv : Function.RightInverse f Associates.mk) (a : α) :
     a * ↑(Classical.choose (associated_map_mk hinv a)) = f (Associates.mk a) :=
   Classical.choose_spec (associated_map_mk hinv a)

Mathlib/Algebra/Homology/Homotopy.lean

@@ -805,9 +805,10 @@ noncomputable def Homotopy.toShortComplex (ho : Homotopy f g) (i : ι) :
       rw [congr_arg (fun j => ho.hom (c.next i) j ≫ L.d j (c.next i)) (c.prev_eq' h)]
     · abel
 
+omit [DecidableRel c.Rel]
 lemma Homotopy.homologyMap_eq (ho : Homotopy f g) (i : ι) [K.HasHomology i] [L.HasHomology i] :
     homologyMap f i = homologyMap g i :=
-  ShortComplex.Homotopy.homologyMap_congr (ho.toShortComplex i)
+  open scoped Classical in ShortComplex.Homotopy.homologyMap_congr (ho.toShortComplex i)
 
 /-- The isomorphism in homology induced by an homotopy equivalence. -/
 noncomputable def HomotopyEquiv.toHomologyIso (h : HomotopyEquiv K L) (i : ι)

Mathlib/Algebra/Homology/HomotopyCofiber.lean

@@ -340,6 +340,7 @@ lemma eq_desc (f : homotopyCofiber φ ⟶ K) (hc : ∀ j, ∃ i, c.Rel i j) :
 
 end
 
+omit [DecidableRel c.Rel] in
 lemma descSigma_ext_iff {φ : F ⟶ G} {K : HomologicalComplex C c}
     (x y : Σ (α : G ⟶ K), Homotopy (φ ≫ α) 0) :
     x = y ↔ x.1 = y.1 ∧ (∀ (i j : ι) (_ : c.Rel j i), x.2.hom i j = y.2.hom i j) := by
@@ -543,6 +544,7 @@ end
 
 end cylinder
 
+omit [DecidableRel c.Rel] in
 /-- If a functor inverts homotopy equivalences, it sends homotopic maps to the same map. -/
 lemma _root_.Homotopy.map_eq_of_inverts_homotopyEquivalences
     {φ₀ φ₁ : F ⟶ G} (h : Homotopy φ₀ φ₁) (hc : ∀ j, ∃ i, c.Rel i j)
@@ -551,6 +553,7 @@ lemma _root_.Homotopy.map_eq_of_inverts_homotopyEquivalences
     {D : Type*} [Category D] (H : HomologicalComplex C c ⥤ D)
     (hH : (homotopyEquivalences C c).IsInvertedBy H) :
     H.map φ₀ = H.map φ₁ := by
+  classical
   simp only [← cylinder.ι₀_desc _ _ h, ← cylinder.ι₁_desc _ _ h, H.map_comp,
     cylinder.map_ι₀_eq_map_ι₁ _ hc _ hH]
 

Mathlib/Algebra/Polynomial/Roots.lean

@@ -831,8 +831,9 @@ theorem card_roots_map_le_natDegree {A B : Type*} [Semiring A] [CommRing B] [IsD
   card_roots' _ |>.trans natDegree_map_le
 
 theorem filter_roots_map_range_eq_map_roots [IsDomain A] [IsDomain B] {f : A →+* B}
-    [DecidableEq A] [DecidableEq B] [DecidablePred (· ∈ f.range)] (hf : Function.Injective f)
+    [DecidablePred (· ∈ f.range)] (hf : Function.Injective f)
     (p : A[X]) : (p.map f).roots.filter (· ∈ f.range) = p.roots.map f := by
+  classical
   ext b
   rw [Multiset.count_filter]
   split_ifs with h

Mathlib/Analysis/AbsoluteValue/Equivalence.lean

@@ -163,7 +163,7 @@ open scoped Topology
 
 variable {R S : Type*} [Field R] [Field S] [LinearOrder S] {v w : AbsoluteValue R S}
   [TopologicalSpace S] [IsStrictOrderedRing S] [Archimedean S] [OrderTopology S]
-  {ι : Type*} [Fintype ι] [DecidableEq ι] {v : ι → AbsoluteValue R S} {w : AbsoluteValue R S}
+  {ι : Type*} [Fintype ι] {v : ι → AbsoluteValue R S} {w : AbsoluteValue R S}
   {a b : R} {i : ι}
 
 /--
@@ -179,6 +179,7 @@ each `v j` for `j ≠ i`.
 private theorem exists_one_lt_lt_one_pi_of_eq_one (ha : 1 < v i a) (haj : ∀ j ≠ i, v j a < 1)
     (haw : w a = 1) (hb : 1 < v i b) (hbw : w b < 1) :
     ∃ k : R, 1 < v i k ∧ (∀ j ≠ i, v j k < 1) ∧ w k < 1 := by
+  classical
   let c : ℕ → R := fun n ↦ a ^ n * b
   have hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop := by
     simpa [c] using Tendsto.atTop_mul_const (by linarith) (tendsto_pow_atTop_atTop_of_one_lt ha)
@@ -206,6 +207,7 @@ each `v j` for `j ≠ i`.
 private theorem exists_one_lt_lt_one_pi_of_one_lt (ha : 1 < v i a) (haj : ∀ j ≠ i, v j a < 1)
     (haw : 1 < w a) (hb : 1 < v i b) (hbw : w b < 1) :
     ∃ k : R, 1 < v i k ∧ (∀ j ≠ i, v j k < 1) ∧ w k < 1 := by
+  classical
   let c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
   have hcᵢ : Tendsto (fun n ↦ v i (c n)) atTop (𝓝 (v i b)) := by
     have : v i a⁻¹ < 1 := map_inv₀ (v i) a ▸ inv_lt_one_of_one_lt₀ ha
@@ -239,12 +241,13 @@ absolute values, then for any `i` there is some `a : R` such that `1 < v i a` an
 theorem exists_one_lt_lt_one_pi_of_not_isEquiv (h : ∀ i, (v i).IsNontrivial)
     (hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) :
     ∀ i, ∃ (a : R), 1 < v i a ∧ ∀ j ≠ i, v j a < 1 := by
-  let P (ι : Type _) [Fintype ι] : Prop := [DecidableEq ι] →
+  classical
+  let P (ι : Type _) [Fintype ι] : Prop :=
     ∀ v : ι → AbsoluteValue R S, (∀ i, (v i).IsNontrivial) →
       (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ i, ∃ (a : R), 1 < v i a ∧ ∀ j ≠ i, v j a < 1
   -- Use strong induction on the index.
-  revert hv h; refine induction_subsingleton_or_nontrivial (P := P) ι (fun ι _ _ _ v h hv i ↦ ?_)
-    (fun ι _ _ ih _ v h hv i ↦ ?_) v
+  revert hv h; refine induction_subsingleton_or_nontrivial (P := P) ι (fun ι _ _ v h hv i ↦ ?_)
+    (fun ι _ _ ih v h hv i ↦ ?_) v
   · -- If `ι` is trivial this follows immediately from `(v i).IsNontrivial`.
     let ⟨a, ha⟩ := (h i).exists_abv_gt_one
     exact ⟨a, ha, fun j hij ↦ absurd (Subsingleton.elim i j) hij.symm⟩

Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

@@ -435,16 +435,18 @@ theorem ext_iff_inner_left_threefold' {x y : E ⊗[𝕜] (F ⊗[𝕜] G)} :
 end TensorProduct
 
 section orthonormal
-variable {ι₁ ι₂ : Type*} [DecidableEq ι₁] [DecidableEq ι₂]
+variable {ι₁ ι₂ : Type*}
 
 open Module
 
 /-- The tensor product of two orthonormal vectors is orthonormal. -/
 theorem Orthonormal.tmul
     {b₁ : ι₁ → E} {b₂ : ι₂ → F} (hb₁ : Orthonormal 𝕜 b₁) (hb₂ : Orthonormal 𝕜 b₂) :
-    Orthonormal 𝕜 fun i : ι₁ × ι₂ ↦ b₁ i.1 ⊗ₜ[𝕜] b₂ i.2 :=
-  orthonormal_iff_ite.mpr fun ⟨i₁, i₂⟩ ⟨j₁, j₂⟩ => by
-    simp [orthonormal_iff_ite.mp, hb₁, hb₂, ← ite_and, and_comm]
+    Orthonormal 𝕜 fun i : ι₁ × ι₂ ↦ b₁ i.1 ⊗ₜ[𝕜] b₂ i.2 := by
+  classical
+  rw [orthonormal_iff_ite]
+  rintro ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
+  simp [orthonormal_iff_ite.mp, hb₁, hb₂, ← ite_and, and_comm]
 
 /-- The tensor product of two orthonormal bases is orthonormal. -/
 theorem Orthonormal.basisTensorProduct

Mathlib/Combinatorics/SimpleGraph/Bipartite.lean

@@ -142,12 +142,16 @@ theorem isBipartiteWith_neighborSet_disjoint' (h : G.IsBipartiteWith s t) (hw :
     Disjoint (G.neighborSet w) t :=
   Set.disjoint_of_subset_left (isBipartiteWith_neighborSet_subset' h hw) h.disjoint
 
-variable {s t : Finset V} [DecidableRel G.Adj]
+variable {s t : Finset V}
 
 section
 
 variable [Fintype ↑(G.neighborSet v)] [Fintype ↑(G.neighborSet w)]
 
+section decidableRel
+
+variable [DecidableRel G.Adj]
+
 /-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is the set of vertices
 in `s` adjacent to `v` in `G`. -/
 theorem isBipartiteWith_neighborFinset (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
@@ -156,19 +160,35 @@ theorem isBipartiteWith_neighborFinset (h : G.IsBipartiteWith s t) (hv : v ∈ s
   rw [mem_neighborFinset, mem_filter, iff_and_self]
   exact h.mem_of_mem_adj hv
 
+/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is the set of vertices
+in `s` adjacent to `w` in `G`. -/
+theorem isBipartiteWith_neighborFinset' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
+    G.neighborFinset w = { v ∈ s | G.Adj v w } := by
+  ext v
+  rw [mem_neighborFinset, adj_comm, mem_filter, iff_and_self]
+  exact h.mem_of_mem_adj' hw
+
 /-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is the set of vertices
 "above" `v` according to the adjacency relation of `G`. -/
 theorem isBipartiteWith_bipartiteAbove (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
     G.neighborFinset v = bipartiteAbove G.Adj t v := by
   rw [isBipartiteWith_neighborFinset h hv, bipartiteAbove]
 
+/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is the set of vertices
+"below" `w` according to the adjacency relation of `G`. -/
+theorem isBipartiteWith_bipartiteBelow (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
+    G.neighborFinset w = bipartiteBelow G.Adj s w := by
+  rw [isBipartiteWith_neighborFinset' h hw, bipartiteBelow]
+
+end decidableRel
+
 /-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is a subset of `s`. -/
 theorem isBipartiteWith_neighborFinset_subset (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
     G.neighborFinset v ⊆ t := by
+  classical
   rw [isBipartiteWith_neighborFinset h hv]
   exact filter_subset (G.Adj v ·) t
 
-omit [DecidableRel G.Adj] in
 /-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is disjoint to `s`. -/
 theorem isBipartiteWith_neighborFinset_disjoint (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
     Disjoint (G.neighborFinset v) s := by
@@ -181,27 +201,13 @@ theorem isBipartiteWith_degree_le (h : G.IsBipartiteWith s t) (hv : v ∈ s) : G
   rw [← card_neighborFinset_eq_degree]
   exact card_le_card (isBipartiteWith_neighborFinset_subset h hv)
 
-/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is the set of vertices
-in `s` adjacent to `w` in `G`. -/
-theorem isBipartiteWith_neighborFinset' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
-    G.neighborFinset w = { v ∈ s | G.Adj v w } := by
-  ext v
-  rw [mem_neighborFinset, adj_comm, mem_filter, iff_and_self]
-  exact h.mem_of_mem_adj' hw
-
-/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is the set of vertices
-"below" `w` according to the adjacency relation of `G`. -/
-theorem isBipartiteWith_bipartiteBelow (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
-    G.neighborFinset w = bipartiteBelow G.Adj s w := by
-  rw [isBipartiteWith_neighborFinset' h hw, bipartiteBelow]
-
 /-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is a subset of `s`. -/
 theorem isBipartiteWith_neighborFinset_subset' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
     G.neighborFinset w ⊆ s := by
+  classical
   rw [isBipartiteWith_neighborFinset' h hw]
   exact filter_subset (G.Adj · w) s
 
-omit [DecidableRel G.Adj] in
 /-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is disjoint to `t`. -/
 theorem isBipartiteWith_neighborFinset_disjoint' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
     Disjoint (G.neighborFinset w) t := by
@@ -222,6 +228,7 @@ of the degrees of vertices in `t`.
 See `Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow`. -/
 theorem isBipartiteWith_sum_degrees_eq [G.LocallyFinite] (h : G.IsBipartiteWith s t) :
     ∑ v ∈ s, G.degree v = ∑ w ∈ t, G.degree w := by
+  classical
   simp_rw [← sum_attach t, ← sum_attach s, ← card_neighborFinset_eq_degree]
   conv_lhs =>
     rhs; intro v
@@ -233,7 +240,7 @@ theorem isBipartiteWith_sum_degrees_eq [G.LocallyFinite] (h : G.IsBipartiteWith
     sum_attach t fun v ↦ #(bipartiteBelow G.Adj s v)]
   exact sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow G.Adj
 
-variable [Fintype V]
+variable [Fintype V] [DecidableRel G.Adj]
 
 lemma isBipartiteWith_sum_degrees_eq_twice_card_edges [DecidableEq V] (h : G.IsBipartiteWith s t) :
     ∑ v ∈ s ∪ t, G.degree v = 2 * #G.edgeFinset := by

Mathlib/Combinatorics/SimpleGraph/Coloring.lean

@@ -430,8 +430,9 @@ theorem chromaticNumber_top_eq_top_of_infinite (V : Type*) [Infinite V] :
   obtain ⟨n, ⟨hn⟩⟩ := hc
   exact not_injective_infinite_finite _ hn.injective_of_top_hom
 
-theorem eq_top_of_chromaticNumber_eq_card [DecidableEq V] [Fintype V]
+theorem eq_top_of_chromaticNumber_eq_card [Fintype V]
     (h : G.chromaticNumber = Fintype.card V) : G = ⊤ := by
+  classical
   by_contra! hh
   have : G.chromaticNumber ≤ Fintype.card V - 1 := by
     obtain ⟨a, b, hne, _⟩ := ne_top_iff_exists_not_adj.mp hh
@@ -443,7 +444,7 @@ theorem eq_top_of_chromaticNumber_eq_card [DecidableEq V] [Fintype V]
   have := Fintype.one_lt_card_iff_nontrivial.mpr <| SimpleGraph.nontrivial_iff.mp ⟨_, _, hh⟩
   grind
 
-theorem chromaticNumber_eq_card_iff [DecidableEq V] [Fintype V] :
+theorem chromaticNumber_eq_card_iff [Fintype V] :
     G.chromaticNumber = Fintype.card V ↔ G = ⊤ :=
   ⟨eq_top_of_chromaticNumber_eq_card, fun h ↦ h ▸ chromaticNumber_top⟩
 

Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean

@@ -228,9 +228,12 @@ lemma exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartit
 lemma CliqueFree.fiveWheelLikeFree_of_le (h : G.CliqueFree (r + 2)) (hk : r ≤ k) :
     G.FiveWheelLikeFree r k := fun hw ↦ (hw.card_inter_lt_of_cliqueFree h).not_ge hk
 
+end withDecEq
+
 /-- A maximally `Kᵣ₊₁`-free graph is `r`-colorable iff it is complete-multipartite. -/
 theorem colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree
     (h : Maximal (fun H => H.CliqueFree (r + 1)) G) : G.Colorable r ↔ G.IsCompleteMultipartite := by
+  classical
   match r with
   | 0 => exact ⟨fun _ ↦ fun x ↦ cliqueFree_one.1 h.1 |>.elim' x,
                 fun _ ↦ G.colorable_zero_iff.2 <| cliqueFree_one.1 h.1⟩
@@ -241,8 +244,6 @@ theorem colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree
       exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hc
     exact hw.not_colorable_succ
 
-end withDecEq
-
 section AES
 variable {i j n : ℕ} {d x v w₁ w₂ : α} {s t : Finset α}
 
@@ -411,8 +412,6 @@ lemma minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ [Fintype α]
 
 end IsFiveWheelLike
 
-variable [DecidableEq α]
-
 /-- **Andrasfái-Erdős-Sós** theorem
 
 If `G` is a `Kᵣ₊₁`-free graph with `n` vertices and `(3 * r - 4) * n / (3 * r - 1) < G.minDegree`
@@ -425,6 +424,7 @@ theorem colorable_of_cliqueFree_lt_minDegree [Fintype α] [DecidableRel G.Adj]
   match r with
   | 0 | 1 => aesop
   | r + 2 =>
+    classical
     -- There is an edge maximal `Kᵣ₊₃`-free supergraph `H` of `G`
     obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf
     -- If `H` is `r + 2`-colorable then so is `G`
@@ -436,7 +436,6 @@ theorem colorable_of_cliqueFree_lt_minDegree [Fintype α] [DecidableRel G.Adj]
     -- Hence `H` contains `Wᵣ₊₁,ₖ` but not `Wᵣ₊₁,ₖ₊₁`, for some `k < r + 1`
     obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
       exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn
-    classical
     -- But the minimum degree of `G`, and hence of `H`, is too large for it to be `Wᵣ₊₁,ₖ₊₁`-free,
     -- a contradiction.
     have hD := hw.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ hmcf.1 <| hm _ <| lt_add_one _