From f2edd790f6c6e1d660515f76768f63cb717434d7 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 22 Jan 2023 01:07:31 +0000
Subject: [PATCH] fix(linear_algebra/basis): add missing decidable arguments in
 lemmas (#18252)

The resulting lemmas are syntactically more general.

To ensure that this catches all of them, this also removes `open_locale classical` from the file, replacing it with manual construction of classical decidability instances within definitions, and `classical` within proofs.
---
 src/analysis/normed_space/pi_Lp.lean |  3 +--
 src/linear_algebra/basis.lean        | 29 ++++++++++++++++++----------
 src/linear_algebra/std_basis.lean    |  4 +---
 3 files changed, 21 insertions(+), 15 deletions(-)

diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean
index 12b33f1a0c6db..acb6eda1527de 100644
--- a/src/analysis/normed_space/pi_Lp.lean
+++ b/src/analysis/normed_space/pi_Lp.lean
@@ -698,8 +698,7 @@ basis.of_equiv_fun (pi_Lp.linear_equiv p 𝕜 (λ _ : ι, 𝕜))
 
 @[simp] lemma basis_fun_apply [decidable_eq ι] (i) :
   basis_fun p 𝕜 ι i = (pi_Lp.equiv p _).symm (pi.single i 1) :=
-by { simp_rw [basis_fun, basis.coe_of_equiv_fun, pi_Lp.linear_equiv_symm_apply, pi.single],
-     congr /- Get rid of a `decidable_eq` mismatch. -/ }
+by simp_rw [basis_fun, basis.coe_of_equiv_fun, pi_Lp.linear_equiv_symm_apply, pi.single]
 
 @[simp] lemma basis_fun_repr (x : pi_Lp p (λ i : ι, 𝕜)) (i : ι) :
   (basis_fun p 𝕜 ι).repr x i = x i :=
diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean
index 4baa8870d7ddd..215594ec368a7 100644
--- a/src/linear_algebra/basis.lean
+++ b/src/linear_algebra/basis.lean
@@ -66,7 +66,7 @@ noncomputable theory
 universe u
 
 open function set submodule
-open_locale classical big_operators
+open_locale big_operators
 
 variables {ι : Type*} {ι' : Type*} {R : Type*} {R₂ : Type*} {K : Type*}
 variables {M : Type*} {M' M'' : Type*} {V : Type u} {V' : Type*}
@@ -367,6 +367,7 @@ by rw [coe_reindex, range_reindex']
 
 /-- `b.reindex_range` is a basis indexed by `range b`, the basis vectors themselves. -/
 def reindex_range : basis (range b) R M :=
+by haveI := classical.dec (nontrivial R); exact
 if h : nontrivial R then
   by letI := h; exact b.reindex (equiv.of_injective b (basis.injective b))
 else
@@ -419,7 +420,7 @@ b.reindex_range_repr' _ rfl
 
 section fintype
 
-variables [fintype ι]
+variables [fintype ι] [decidable_eq M]
 
 /-- `b.reindex_finset_range` is a basis indexed by `finset.univ.image b`,
 the finite set of basis vectors themselves. -/
@@ -750,11 +751,13 @@ linear_equiv.trans b.repr
      ..finsupp.equiv_fun_on_finite } : (ι →₀ R) ≃ₗ[R] (ι → R))
 
 /-- A module over a finite ring that admits a finite basis is finite. -/
-def module.fintype_of_fintype [fintype R] : fintype M :=
-fintype.of_equiv _ b.equiv_fun.to_equiv.symm
+def module.fintype_of_fintype (b : basis ι R M) [fintype R] : fintype M :=
+by haveI := classical.dec_eq ι; exact
+  fintype.of_equiv _ b.equiv_fun.to_equiv.symm
 
-theorem module.card_fintype [fintype R] [fintype M] :
+theorem module.card_fintype (b : basis ι R M) [fintype R] [fintype M] :
   card M = (card R) ^ (card ι) :=
+by classical; exact
 calc card M = card (ι → R)    : card_congr b.equiv_fun.to_equiv
         ... = card R ^ card ι : card_fun
 
@@ -781,7 +784,8 @@ lemma basis.sum_repr (u : M) : ∑ i, b.repr u i • b i = u :=
 b.sum_equiv_fun u
 
 @[simp]
-lemma basis.equiv_fun_self (i j : ι) : b.equiv_fun (b i) j = if i = j then 1 else 0 :=
+lemma basis.equiv_fun_self [decidable_eq ι] (i j : ι) :
+  b.equiv_fun (b i) j = if i = j then 1 else 0 :=
 by { rw [b.equiv_fun_apply, b.repr_self_apply] }
 
 lemma basis.repr_sum_self (c : ι → R) : ⇑(b.repr (∑ i, c i • b i)) = c :=
@@ -802,7 +806,7 @@ basis.of_repr $ e.trans $ linear_equiv.symm $ finsupp.linear_equiv_fun_on_finite
 @[simp] lemma basis.of_equiv_fun_repr_apply (e : M ≃ₗ[R] (ι → R)) (x : M) (i : ι) :
   (basis.of_equiv_fun e).repr x i = e x i := rfl
 
-@[simp] lemma basis.coe_of_equiv_fun (e : M ≃ₗ[R] (ι → R)) :
+@[simp] lemma basis.coe_of_equiv_fun [decidable_eq ι] (e : M ≃ₗ[R] (ι → R)) :
   (basis.of_equiv_fun e : ι → M) = λ i, e.symm (function.update 0 i 1) :=
 funext $ λ i, e.injective $ funext $ λ j,
   by simp [basis.of_equiv_fun, ←finsupp.single_eq_pi_single, finsupp.single_eq_update]
@@ -810,6 +814,7 @@ funext $ λ i, e.injective $ funext $ λ j,
 @[simp] lemma basis.of_equiv_fun_equiv_fun
   (v : basis ι R M) : basis.of_equiv_fun v.equiv_fun = v :=
 begin
+  classical,
   ext j,
   simp only [basis.equiv_fun_symm_apply, basis.coe_of_equiv_fun],
   simp_rw [function.update_apply, ite_smul],
@@ -971,7 +976,7 @@ by simp [hli.repr_eq_single j, h]
 
 /-- Given a basis, the `i`th element of the dual basis evaluates to the Kronecker delta on the
 `j`th element of the basis. -/
-lemma mk_coord_apply {i j : ι} :
+lemma mk_coord_apply [decidable_eq ι] {i j : ι} :
   (basis.mk hli hsp).coord i (v j) = if j = i then 1 else 0 :=
 begin
   cases eq_or_ne j i,
@@ -1058,6 +1063,7 @@ mk_apply
 @[simp] lemma coord_units_smul (e : basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) :
   (e.units_smul w).coord i = (w i)⁻¹ • e.coord i :=
 begin
+  classical,
   apply e.ext,
   intros j,
   transitivity ((e.units_smul w).coord i) ((w j)⁻¹ • (e.units_smul w) j),
@@ -1227,7 +1233,9 @@ let s := set.range v,
     b := hs.to_subtype_range.extend (subset_univ (set.range v)) in
 (basis.extend hs.to_subtype_range).reindex $ equiv.symm $
   calc ι ⊕ (b \ s : set V) ≃ s ⊕ (b \ s : set V) : equiv.sum_congr e (equiv.refl _)
-  ... ≃ b                   : equiv.set.sum_diff_subset (hs.to_subtype_range.subset_extend _)
+  ... ≃ b                   :
+    by haveI := classical.dec_pred (∈ s); exact
+      equiv.set.sum_diff_subset (hs.to_subtype_range.subset_extend _)
 
 lemma subset_extend {s : set V} (hs : linear_independent K (coe : s → V)) :
   s ⊆ hs.extend (set.subset_univ _) :=
@@ -1275,7 +1283,8 @@ variables (K V)
 
 theorem vector_space.card_fintype [fintype K] [fintype V] :
   ∃ n : ℕ, card V = (card K) ^ n :=
-⟨card (basis.of_vector_space_index K V), module.card_fintype (basis.of_vector_space K V)⟩
+by classical; exact
+  ⟨card (basis.of_vector_space_index K V), module.card_fintype (basis.of_vector_space K V)⟩
 
 section atoms_of_submodule_lattice
 
diff --git a/src/linear_algebra/std_basis.lean b/src/linear_algebra/std_basis.lean
index 1b47691c937d7..c198c0bcd33be 100644
--- a/src/linear_algebra/std_basis.lean
+++ b/src/linear_algebra/std_basis.lean
@@ -34,7 +34,6 @@ this is a basis over `fin 3 → R`.
 
 open function submodule
 open_locale big_operators
-open_locale big_operators
 
 namespace linear_map
 
@@ -247,8 +246,7 @@ basis.of_equiv_fun (linear_equiv.refl _ _)
 @[simp] lemma basis_fun_apply [decidable_eq η] (i) :
   basis_fun R η i = std_basis R (λ (i : η), R) i 1 :=
 by { simp only [basis_fun, basis.coe_of_equiv_fun, linear_equiv.refl_symm,
-                linear_equiv.refl_apply, std_basis_apply],
-     congr /- Get rid of a `decidable_eq` mismatch. -/ }
+                linear_equiv.refl_apply, std_basis_apply] }
 
 @[simp] lemma basis_fun_repr (x : η → R) (i : η) :
   (pi.basis_fun R η).repr x i = x i :=