chore: backports for leanprover/lean4#4814 (part 13) (#15397)

see #15245

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Mathlib/Algebra/Order/Antidiag/Finsupp.lean

@@ -83,7 +83,7 @@ theorem mem_finsuppAntidiag_insert {a : ι} {s : Finset ι}
       intro x hx
       rw [update_noteq (ne_of_mem_of_not_mem hx h) n1 ⇑g]
 
-theorem finsuppAntidiag_insert [DecidableEq μ] {a : ι} {s : Finset ι}
+theorem finsuppAntidiag_insert {a : ι} {s : Finset ι}
     (h : a ∉ s) (n : μ) :
     finsuppAntidiag (insert a s) n = (antidiagonal n).biUnion
       (fun p : μ × μ =>

Mathlib/CategoryTheory/Galois/Basic.lean

@@ -106,6 +106,7 @@ class PreservesIsConnected {C : Type u₁} [Category.{u₂, u₁} C] {D : Type v
   /-- `F.obj X` is connected if `X` is connected. -/
   preserves : ∀ {X : C} [IsConnected X], IsConnected (F.obj X)
 
+section
 variable {C : Type u₁} [Category.{u₂, u₁} C] [PreGaloisCategory C]
 
 attribute [instance] hasTerminal hasPullbacks hasFiniteCoproducts hasQuotientsByFiniteGroups
@@ -116,6 +117,8 @@ instance : HasBinaryProducts C := hasBinaryProducts_of_hasTerminal_and_pullbacks
 
 instance : HasEqualizers C := hasEqualizers_of_hasPullbacks_and_binary_products
 
+end
+
 namespace FiberFunctor
 
 variable {C : Type u₁} [Category.{u₂, u₁} C] {F : C ⥤ FintypeCat.{w}} [PreGaloisCategory C]
@@ -156,7 +159,8 @@ instance : F.Faithful where
 
 end FiberFunctor
 
-variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
+variable {C : Type u₁} [Category.{u₂, u₁} C]
+  (F : C ⥤ FintypeCat.{w})
 
 /-- The canonical action of `Aut F` on the fiber of each object. -/
 instance (X : C) : MulAction (Aut F) (F.obj X) where
@@ -168,6 +172,20 @@ lemma mulAction_def {X : C} (σ : Aut F) (x : F.obj X) :
     σ • x = σ.hom.app X x :=
   rfl
 
+/-- An object that is neither initial or connected has a non-trivial subobject. -/
+lemma has_non_trivial_subobject_of_not_isConnected_of_not_initial (X : C) (hc : ¬ IsConnected X)
+    (hi : IsInitial X → False) :
+    ∃ (Y : C) (v : Y ⟶ X), (IsInitial Y → False) ∧ Mono v ∧ (¬ IsIso v) := by
+  contrapose! hc
+  exact ⟨hi, fun Y i hm hni ↦ hc Y i hni hm⟩
+
+/-- The cardinality of the fiber is preserved under isomorphisms. -/
+lemma card_fiber_eq_of_iso {X Y : C} (i : X ≅ Y) : Nat.card (F.obj X) = Nat.card (F.obj Y) := by
+  have e : F.obj X ≃ F.obj Y := Iso.toEquiv (mapIso (F ⋙ FintypeCat.incl) i)
+  exact Nat.card_eq_of_bijective e (Equiv.bijective e)
+
+variable [PreGaloisCategory C] [FiberFunctor F]
+
 /-- An object is initial if and only if its fiber is empty. -/
 lemma initial_iff_fiber_empty (X : C) : Nonempty (IsInitial X) ↔ IsEmpty (F.obj X) := by
   rw [(IsInitial.isInitialIffObj F X).nonempty_congr]
@@ -189,13 +207,6 @@ lemma not_initial_iff_fiber_nonempty (X : C) : (IsInitial X → False) ↔ Nonem
 lemma not_initial_of_inhabited {X : C} (x : F.obj X) (h : IsInitial X) : False :=
   ((initial_iff_fiber_empty F X).mp ⟨h⟩).false x
 
-/-- An object that is neither initial or connected has a non-trivial subobject. -/
-lemma has_non_trivial_subobject_of_not_isConnected_of_not_initial (X : C) (hc : ¬ IsConnected X)
-    (hi : IsInitial X → False) :
-    ∃ (Y : C) (v : Y ⟶ X), (IsInitial Y → False) ∧ Mono v ∧ (¬ IsIso v) := by
-  contrapose! hc
-  exact ⟨hi, fun Y i hm hni ↦ hc Y i hni hm⟩
-
 /-- The fiber of a connected object is nonempty. -/
 instance nonempty_fiber_of_isConnected (X : C) [IsConnected X] : Nonempty (F.obj X) := by
   by_contra h
@@ -339,11 +350,6 @@ lemma card_fiber_coprod_eq_sum (X Y : C) :
   rw [← Nat.card_sum]
   exact Nat.card_eq_of_bijective e.toFun (Equiv.bijective e)
 
-/-- The cardinality of the fiber is preserved under isomorphisms. -/
-lemma card_fiber_eq_of_iso {X Y : C} (i : X ≅ Y) : Nat.card (F.obj X) = Nat.card (F.obj Y) := by
-  have e : F.obj X ≃ F.obj Y := Iso.toEquiv (mapIso (F ⋙ FintypeCat.incl) i)
-  exact Nat.card_eq_of_bijective e (Equiv.bijective e)
-
 /-- The cardinality of morphisms `A ⟶ X` is smaller than the cardinality of
 the fiber of the target if the source is connected. -/
 lemma card_hom_le_card_fiber_of_connected (A X : C) [IsConnected A] :

Mathlib/Data/Nat/Choose/Multinomial.lean

@@ -249,7 +249,7 @@ lemma sum_pow_eq_sum_piAntidiag_of_commute (s : Finset α) (f : α → R)
   exact ne_of_mem_of_not_mem ht has
 
 /-- The **multinomial theorem**. -/
-theorem sum_pow_of_commute [Semiring R] (x : α → R) (s : Finset α)
+theorem sum_pow_of_commute (x : α → R) (s : Finset α)
     (hc : (s : Set α).Pairwise fun i j => Commute (x i) (x j)) :
     ∀ n,
       s.sum x ^ n =
@@ -297,7 +297,7 @@ lemma sum_pow_eq_sum_piAntidiag (s : Finset α) (f : α → R) (n : ℕ) :
   simp_rw [← noncommProd_eq_prod]
   rw [← sum_pow_eq_sum_piAntidiag_of_commute _ _ fun _ _ _ _ _ ↦ Commute.all ..]
 
-theorem sum_pow [CommSemiring R] (x : α → R) (n : ℕ) :
+theorem sum_pow (x : α → R) (n : ℕ) :
     s.sum x ^ n = ∑ k ∈ s.sym n, k.val.multinomial * (k.val.map x).prod := by
   conv_rhs => rw [← sum_coe_sort]
   convert sum_pow_of_commute x s (fun _ _ _ _ _ ↦ Commute.all ..) n

Mathlib/GroupTheory/Abelianization.lean

@@ -188,10 +188,10 @@ end Abelianization
 section AbelianizationCongr
 
 -- Porting note: `[Group G]` should not be necessary here
-variable {G} [Group G] {H : Type v} [Group H] (e : G ≃* H)
+variable {G} {H : Type v} [Group H]
 
 /-- Equivalent groups have equivalent abelianizations -/
-def MulEquiv.abelianizationCongr : Abelianization G ≃* Abelianization H where
+def MulEquiv.abelianizationCongr (e : G ≃* H) : Abelianization G ≃* Abelianization H where
   toFun := Abelianization.map e.toMonoidHom
   invFun := Abelianization.map e.symm.toMonoidHom
   left_inv := by
@@ -203,7 +203,7 @@ def MulEquiv.abelianizationCongr : Abelianization G ≃* Abelianization H where
   map_mul' := MonoidHom.map_mul _
 
 @[simp]
-theorem abelianizationCongr_of (x : G) :
+theorem abelianizationCongr_of (e : G ≃* H) (x : G) :
     e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x) :=
   rfl
 
@@ -213,11 +213,12 @@ theorem abelianizationCongr_refl :
   MulEquiv.toMonoidHom_injective Abelianization.lift_of
 
 @[simp]
-theorem abelianizationCongr_symm : e.abelianizationCongr.symm = e.symm.abelianizationCongr :=
+theorem abelianizationCongr_symm (e : G ≃* H) :
+    e.abelianizationCongr.symm = e.symm.abelianizationCongr :=
   rfl
 
 @[simp]
-theorem abelianizationCongr_trans {I : Type v} [Group I] (e₂ : H ≃* I) :
+theorem abelianizationCongr_trans {I : Type v} [Group I] (e : G ≃* H) (e₂ : H ≃* I) :
     e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr :=
   MulEquiv.toMonoidHom_injective (Abelianization.hom_ext _ _ rfl)
 

Mathlib/GroupTheory/GroupAction/Basic.lean

@@ -661,7 +661,7 @@ lemma stabilizer_smul_eq_left [SMul α β] [IsScalarTower G α β] (a : α) (b :
   simpa only [mem_stabilizer_iff, ← smul_assoc, h.eq_iff] using ha
 
 @[to_additive (attr := simp)]
-lemma stabilizer_smul_eq_right [Group α] [MulAction α β] [SMulCommClass G α β] (a : α) (b : β) :
+lemma stabilizer_smul_eq_right {α} [Group α] [MulAction α β] [SMulCommClass G α β] (a : α) (b : β) :
     stabilizer G (a • b) = stabilizer G b :=
   (le_stabilizer_smul_right _ _).antisymm' <| (le_stabilizer_smul_right a⁻¹ _).trans_eq <| by
     rw [inv_smul_smul]

Mathlib/GroupTheory/GroupAction/Quotient.lean

@@ -119,8 +119,8 @@ theorem _root_.MulActionHom.toQuotient_apply (H : Subgroup α) (g : α) :
 instance mulLeftCosetsCompSubtypeVal (H I : Subgroup α) : MulAction I (α ⧸ H) :=
   MulAction.compHom (α ⧸ H) (Subgroup.subtype I)
 
--- Porting note: Needed to insert [Group α] here
-variable (α) [Group α] [MulAction α β] (x : β)
+variable (α)
+variable [MulAction α β] (x : β)
 
 /-- The canonical map from the quotient of the stabilizer to the set. -/
 @[to_additive "The canonical map from the quotient of the stabilizer to the set. "]

Mathlib/GroupTheory/NoncommPiCoprod.lean

@@ -81,7 +81,7 @@ variable {M : Type*} [Monoid M]
 
 -- We have a family of monoids
 -- The fintype assumption is not always used, but declared here, to keep things in order
-variable {ι : Type*} [DecidableEq ι] [Fintype ι]
+variable {ι : Type*} [Fintype ι]
 variable {N : ι → Type*} [∀ i, Monoid (N i)]
 
 -- And morphisms ϕ into G
@@ -114,7 +114,7 @@ def noncommPiCoprod : (∀ i : ι, N i) →* M where
 variable {hcomm}
 
 @[to_additive (attr := simp)]
-theorem noncommPiCoprod_mulSingle (i : ι) (y : N i) :
+theorem noncommPiCoprod_mulSingle [DecidableEq ι] (i : ι) (y : N i) :
     noncommPiCoprod ϕ hcomm (Pi.mulSingle i y) = ϕ i y := by
   change Finset.univ.noncommProd (fun j => ϕ j (Pi.mulSingle i y j)) (fun _ _ _ _ h => hcomm h _ _)
     = ϕ i y
@@ -130,7 +130,7 @@ theorem noncommPiCoprod_mulSingle (i : ι) (y : N i) :
 
 /-- The universal property of `MonoidHom.noncommPiCoprod` -/
 @[to_additive "The universal property of `AddMonoidHom.noncommPiCoprod`"]
-def noncommPiCoprodEquiv :
+def noncommPiCoprodEquiv [DecidableEq ι] :
     { ϕ : ∀ i, N i →* M // Pairwise fun i j => ∀ x y, Commute (ϕ i x) (ϕ j y) } ≃
       ((∀ i, N i) →* M) where
   toFun ϕ := noncommPiCoprod ϕ.1 ϕ.2
@@ -164,7 +164,7 @@ end FamilyOfMonoids
 section FamilyOfGroups
 
 variable {G : Type*} [Group G]
-variable {ι : Type*} [hdec : DecidableEq ι] [hfin : Fintype ι]
+variable {ι : Type*}
 variable {H : ι → Type*} [∀ i, Group (H i)]
 variable (ϕ : ∀ i : ι, H i →* G)
 
@@ -174,7 +174,7 @@ variable (f g : ∀ i : ι, H i)
 namespace MonoidHom
 -- The subgroup version of `MonoidHom.noncommPiCoprod_mrange`
 @[to_additive]
-theorem noncommPiCoprod_range
+theorem noncommPiCoprod_range [Fintype ι]
     {hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)} :
     (noncommPiCoprod ϕ hcomm).range = ⨆ i : ι, (ϕ i).range := by
   letI := Classical.decEq ι
@@ -190,7 +190,7 @@ theorem noncommPiCoprod_range
     exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
 
 @[to_additive]
-theorem injective_noncommPiCoprod_of_independent
+theorem injective_noncommPiCoprod_of_independent [Fintype ι]
     {hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)}
     (hind : CompleteLattice.Independent fun i => (ϕ i).range)
     (hinj : ∀ i, Function.Injective (ϕ i)) : Function.Injective (noncommPiCoprod ϕ hcomm) := by
@@ -249,7 +249,7 @@ namespace Subgroup
 
 -- We have a family of subgroups
 variable {G : Type*} [Group G]
-variable {ι : Type*} [hdec : DecidableEq ι] [hfin : Fintype ι] {H : ι → Subgroup G}
+variable {ι : Type*} {H : ι → Subgroup G}
 
 -- Elements of `Π (i : ι), H i` are called `f` and `g` here
 variable (f g : ∀ i : ι, H i)
@@ -267,6 +267,18 @@ theorem commute_subtype_of_commute
   rintro ⟨x, hx⟩ ⟨y, hy⟩
   exact hcomm hne x y hx hy
 
+@[to_additive]
+theorem independent_of_coprime_order
+    (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y)
+    [Finite ι] [∀ i, Fintype (H i)]
+    (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
+    CompleteLattice.Independent H := by
+  simpa using
+    MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype)
+      (commute_subtype_of_commute hcomm) hcoprime
+
+variable [Fintype ι]
+
 /-- The canonical homomorphism from a family of subgroups where elements from different subgroups
 commute -/
 @[to_additive "The canonical homomorphism from a family of additive subgroups where elements from
@@ -276,7 +288,7 @@ def noncommPiCoprod (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i →
   MonoidHom.noncommPiCoprod (fun i => (H i).subtype) (commute_subtype_of_commute hcomm)
 
 @[to_additive (attr := simp)]
-theorem noncommPiCoprod_mulSingle
+theorem noncommPiCoprod_mulSingle [DecidableEq ι]
     {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y}(i : ι) (y : H i) :
     noncommPiCoprod hcomm (Pi.mulSingle i y) = y := by apply MonoidHom.noncommPiCoprod_mulSingle
 
@@ -296,16 +308,6 @@ theorem injective_noncommPiCoprod_of_independent
   · intro i
     exact Subtype.coe_injective
 
-@[to_additive]
-theorem independent_of_coprime_order
-    (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y)
-    [Finite ι] [∀ i, Fintype (H i)]
-    (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
-    CompleteLattice.Independent H := by
-  simpa using
-    MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype)
-      (commute_subtype_of_commute hcomm) hcoprime
-
 end CommutingSubgroups
 
 end Subgroup

Mathlib/GroupTheory/OrderOfElement.lean

@@ -751,10 +751,28 @@ lemma orderOf_eq_card_powers : orderOf x = Fintype.card (powers x : Set G) :=
 end FiniteCancelMonoid
 
 section FiniteGroup
-variable [Group G]
+variable [Group G] {x y : G}
+
+@[to_additive]
+theorem zpow_eq_one_iff_modEq {n : ℤ} : x ^ n = 1 ↔ n ≡ 0 [ZMOD orderOf x] := by
+  rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]
+
+
+@[to_additive]
+theorem zpow_eq_zpow_iff_modEq {m n : ℤ} : x ^ m = x ^ n ↔ m ≡ n [ZMOD orderOf x] := by
+  rw [← mul_inv_eq_one, ← zpow_sub, zpow_eq_one_iff_modEq, Int.modEq_iff_dvd, Int.modEq_iff_dvd,
+    zero_sub, neg_sub]
+
+@[to_additive (attr := simp)]
+theorem injective_zpow_iff_not_isOfFinOrder : (Injective fun n : ℤ => x ^ n) ↔ ¬IsOfFinOrder x := by
+  refine ⟨?_, fun h n m hnm => ?_⟩
+  · simp_rw [isOfFinOrder_iff_pow_eq_one]
+    rintro h ⟨n, hn, hx⟩
+    exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx)
+  rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm
 
 section Finite
-variable [Finite G] {x y : G}
+variable [Finite G]
 
 @[to_additive]
 theorem exists_zpow_eq_one (x : G) : ∃ (i : ℤ) (_ : i ≠ 0), x ^ (i : ℤ) = 1 := by
@@ -776,23 +794,6 @@ lemma mem_zpowers_iff_mem_range_orderOf [DecidableEq G] :
     y ∈ zpowers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·) :=
   (isOfFinOrder_of_finite _).mem_zpowers_iff_mem_range_orderOf
 
-@[to_additive]
-theorem zpow_eq_one_iff_modEq {n : ℤ} : x ^ n = 1 ↔ n ≡ 0 [ZMOD orderOf x] := by
-  rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]
-
-@[to_additive]
-theorem zpow_eq_zpow_iff_modEq {m n : ℤ} : x ^ m = x ^ n ↔ m ≡ n [ZMOD orderOf x] := by
-  rw [← mul_inv_eq_one, ← zpow_sub, zpow_eq_one_iff_modEq, Int.modEq_iff_dvd, Int.modEq_iff_dvd,
-    zero_sub, neg_sub]
-
-@[to_additive (attr := simp)]
-theorem injective_zpow_iff_not_isOfFinOrder : (Injective fun n : ℤ => x ^ n) ↔ ¬IsOfFinOrder x := by
-  refine ⟨?_, fun h n m hnm => ?_⟩
-  · simp_rw [isOfFinOrder_iff_pow_eq_one]
-    rintro h ⟨n, hn, hx⟩
-    exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx)
-  rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm
-
 /-- The equivalence between `Subgroup.zpowers` of two elements `x, y` of the same order, mapping
   `x ^ i` to `y ^ i`. -/
 @[to_additive
@@ -862,18 +863,18 @@ theorem orderOf_dvd_natCard {G : Type*} [Group G] (x : G) : orderOf x ∣ Nat.ca
   · simp only [card_eq_zero_of_infinite, dvd_zero]
 
 @[to_additive]
-nonrec lemma Subgroup.orderOf_dvd_natCard (s : Subgroup G) (hx : x ∈ s) :
+nonrec lemma Subgroup.orderOf_dvd_natCard {G : Type*} [Group G] (s : Subgroup G) {x} (hx : x ∈ s) :
   orderOf x ∣ Nat.card s := by simpa using orderOf_dvd_natCard (⟨x, hx⟩ : s)
 
 @[to_additive]
-lemma Subgroup.orderOf_le_card (s : Subgroup G) (hs : (s : Set G).Finite) (hx : x ∈ s) :
-    orderOf x ≤ Nat.card s :=
+lemma Subgroup.orderOf_le_card {G : Type*} [Group G] (s : Subgroup G) (hs : (s : Set G).Finite)
+    {x} (hx : x ∈ s) : orderOf x ≤ Nat.card s :=
   le_of_dvd (Nat.card_pos_iff.2 <| ⟨s.coe_nonempty.to_subtype, hs.to_subtype⟩) <|
     s.orderOf_dvd_natCard hx
 
 @[to_additive]
-lemma Submonoid.orderOf_le_card (s : Submonoid G) (hs : (s : Set G).Finite) (hx : x ∈ s) :
-    orderOf x ≤ Nat.card s := by
+lemma Submonoid.orderOf_le_card {G : Type*} [Group G] (s : Submonoid G) (hs : (s : Set G).Finite)
+    {x} (hx : x ∈ s) : orderOf x ≤ Nat.card s := by
   rw [← Nat.card_submonoidPowers]; exact Nat.card_mono hs <| powers_le.2 hx
 
 @[to_additive (attr := simp) card_nsmul_eq_zero']
@@ -899,11 +900,11 @@ theorem zpow_mod_card (a : G) (n : ℤ) : a ^ (n % Fintype.card G : ℤ) = a ^ n
     (Int.natCast_dvd_natCast.2 orderOf_dvd_card), zpow_mod_orderOf]
 
 @[to_additive (attr := simp) mod_natCard_nsmul]
-lemma pow_mod_natCard (a : G) (n : ℕ) : a ^ (n % Nat.card G) = a ^ n := by
+lemma pow_mod_natCard {G} [Group G] (a : G) (n : ℕ) : a ^ (n % Nat.card G) = a ^ n := by
   rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n $ orderOf_dvd_natCard _, pow_mod_orderOf]
 
 @[to_additive (attr := simp) mod_natCard_zsmul]
-lemma zpow_mod_natCard (a : G) (n : ℤ) : a ^ (n % Nat.card G : ℤ) = a ^ n := by
+lemma zpow_mod_natCard {G} [Group G] (a : G) (n : ℤ) : a ^ (n % Nat.card G : ℤ) = a ^ n := by
   rw [eq_comm, ← zpow_mod_orderOf,
     ← Int.emod_emod_of_dvd n $ Int.natCast_dvd_natCast.2 $ orderOf_dvd_natCard _, zpow_mod_orderOf]
 
@@ -933,7 +934,8 @@ theorem powCoprime_inv {G : Type*} [Group G] (h : (Nat.card G).Coprime n) {g : G
   inv_pow g n
 
 @[to_additive Nat.Coprime.nsmul_right_bijective]
-lemma Nat.Coprime.pow_left_bijective (hn : (Nat.card G).Coprime n) : Bijective (· ^ n : G → G) :=
+lemma Nat.Coprime.pow_left_bijective {G} [Group G] (hn : (Nat.card G).Coprime n) :
+    Bijective (· ^ n : G → G) :=
   (powCoprime hn).bijective
 
 @[to_additive add_inf_eq_bot_of_coprime]
@@ -1080,11 +1082,13 @@ lemma Nat.cast_card_eq_zero (R) [AddGroupWithOne R] [Fintype R] : (Fintype.card
   rw [← nsmul_one, card_nsmul_eq_zero]
 
 section NonAssocRing
-variable (R : Type*) [NonAssocRing R] [Fintype R] (p : ℕ)
+variable (R : Type*) [NonAssocRing R] (p : ℕ)
 
 lemma CharP.addOrderOf_one : CharP R (addOrderOf (1 : R)) where
   cast_eq_zero_iff' n := by rw [← Nat.smul_one_eq_cast, addOrderOf_dvd_iff_nsmul_eq_zero]
 
+variable [Fintype R]
+
 variable {R} in
 lemma charP_of_ne_zero (hn : card R = p) (hR : ∀ i < p, (i : R) = 0 → i = 0) : CharP R p where
   cast_eq_zero_iff' n := by