chore: remove Fintype.card_fin_even (#10273)

This instance was meant to apply to even literal numbers. Because Lean 4 no longer uses bit0/bit1 for literals, it no longer serves that purpose. Instead, a specific instance for Fin 2 is added.
leanprover-community · Feb 11, 2024 · 7d2b303 · 7d2b303
1 parent 87dac0a
commit 7d2b303
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 17 deletions.
diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
@@ -32,8 +32,6 @@ open Matrix Matrix.SpecialLinearGroup
 
 open scoped Classical BigOperators MatrixGroups
 
-attribute [local instance] Fintype.card_fin_even
-
 /- Disable these instances as they are not the simp-normal form, and having them disabled ensures
 we state lemmas in this file without spurious `coe_fn` terms. -/
 attribute [-instance] Matrix.SpecialLinearGroup.instCoeFun
@@ -385,9 +383,6 @@ theorem im_smul_eq_div_normSq (g : GL(2, ℝ)⁺) (z : ℍ) :
   smulAux'_im g z
 #align upper_half_plane.im_smul_eq_div_norm_sq UpperHalfPlane.im_smul_eq_div_normSq
 
--- Porting note FIXME: this instance isn't being found, but is needed here.
-instance : Fact (Even (Fintype.card (Fin 2))) := ⟨Nat.even_iff.mpr rfl⟩
-
 @[simp]
 theorem neg_smul (g : GL(2, ℝ)⁺) (z : ℍ) : -g • z = g • z := by
   ext1

diff --git a/Mathlib/Data/Fintype/Parity.lean b/Mathlib/Data/Fintype/Parity.lean
@@ -9,7 +9,7 @@ import Mathlib.Algebra.Parity
 #align_import data.fintype.parity from "leanprover-community/mathlib"@"509de852e1de55e1efa8eacfa11df0823f26f226"
 
 /-!
-# The cardinality of `Fin (bit0 n)` is even.
+# The cardinality of `Fin 2` is even.
 -/
 
 
@@ -21,12 +21,10 @@ instance IsSquare.decidablePred [Mul α] [Fintype α] [DecidableEq α] :
     DecidablePred (IsSquare : α → Prop) := fun _ => Fintype.decidableExistsFintype
 #align fintype.is_square.decidable_pred Fintype.IsSquare.decidablePred
 
-end Fintype
-
-set_option linter.deprecated false
+/-- The cardinality of `Fin 2` is even, `Fact` version.
+This `Fact` is needed as an instance by `Matrix.SpecialLinearGroup.instNeg`. -/
+instance card_fin_two : Fact (Even (Fintype.card (Fin 2))) :=
+  ⟨⟨1, rfl⟩⟩
+#noalign fintype.card_fin_even
 
-/-- The cardinality of `Fin (bit0 n)` is even, `Fact` version.
-This `Fact` is needed as an instance by `Matrix.SpecialLinearGroup.has_neg`. -/
-theorem Fintype.card_fin_even {n : ℕ} : Fact (Even (Fintype.card (Fin (bit0 n)))) :=
-  ⟨by rw [Fintype.card_fin]; exact even_bit0 _⟩
-#align fintype.card_fin_even Fintype.card_fin_even
+end Fintype
diff --git a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
@@ -271,7 +271,7 @@ variable [Fact (Even (Fintype.card n))]
 
 /-- Formal operation of negation on special linear group on even cardinality `n` given by negating
 each element. -/
-instance : Neg (SpecialLinearGroup n R) :=
+instance instNeg : Neg (SpecialLinearGroup n R) :=
   ⟨fun g => ⟨-g, by
     simpa [(@Fact.out <| Even <| Fintype.card n).neg_one_pow, g.det_coe] using det_smul (↑ₘg) (-1)⟩⟩
 

diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean
@@ -75,8 +75,6 @@ local macro "↑ₘ" t:term:80 : term => `(term| ($t : Matrix (Fin 2) (Fin 2)
 
 open scoped UpperHalfPlane ComplexConjugate
 
-attribute [local instance] Fintype.card_fin_even
-
 namespace ModularGroup
 
 variable {g : SL(2, ℤ)} (z : ℍ)