chore: backports for leanprover/lean4#4814 (part 22) (#15511)

Mathlib/Algebra/Category/ModuleCat/Sheaf/Limits.lean

@@ -30,11 +30,11 @@ namespace PresheafOfModules
 variable {R : Cᵒᵖ ⥤ RingCat.{u}}
   {F : D ⥤ PresheafOfModules.{v} R}
   [∀ X, Small.{v} ((F ⋙ evaluation R X) ⋙ forget _).sections]
-  {c : Cone F} (hc : IsLimit c)
-  (hF : ∀ j, Presheaf.IsSheaf J (F.obj j).presheaf)
+  {c : Cone F}
   [HasLimitsOfShape D AddCommGrp.{v}]
 
-lemma isSheaf_of_isLimit : Presheaf.IsSheaf J (c.pt.presheaf) := by
+lemma isSheaf_of_isLimit (hc : IsLimit c) (hF : ∀ j, Presheaf.IsSheaf J (F.obj j).presheaf) :
+    Presheaf.IsSheaf J (c.pt.presheaf) := by
   let G : D ⥤ Sheaf J AddCommGrp.{v} :=
     { obj := fun j => ⟨(F.obj j).presheaf, hF j⟩
       map := fun φ => ⟨(PresheafOfModules.toPresheaf R).map (F.map φ)⟩ }

Mathlib/Analysis/BoxIntegral/Partition/Filter.lean

@@ -173,8 +173,7 @@ noncomputable section
 
 namespace BoxIntegral
 
-variable {ι : Type*} [Fintype ι] {I J : Box ι} {c c₁ c₂ : ℝ≥0} {r r₁ r₂ : (ι → ℝ) → Ioi (0 : ℝ)}
-  {π π₁ π₂ : TaggedPrepartition I}
+variable {ι : Type*} [Fintype ι] {I J : Box ι} {c c₁ c₂ : ℝ≥0}
 
 open TaggedPrepartition
 
@@ -327,6 +326,8 @@ theorem toFilter_inf_iUnion_eq (l : IntegrationParams) (I : Box ι) (π₀ : Pre
     l.toFilter I ⊓ 𝓟 { π | π.iUnion = π₀.iUnion } = l.toFilteriUnion I π₀ :=
   (iSup_inf_principal _ _).symm
 
+variable {r r₁ r₂ : (ι → ℝ) → Ioi (0 : ℝ)} {π π₁ π₂ : TaggedPrepartition I}
+
 theorem MemBaseSet.mono' (I : Box ι) (h : l₁ ≤ l₂) (hc : c₁ ≤ c₂) {π : TaggedPrepartition I}
     (hr : ∀ J ∈ π, r₁ (π.tag J) ≤ r₂ (π.tag J)) (hπ : l₁.MemBaseSet I c₁ r₁ π) :
     l₂.MemBaseSet I c₂ r₂ π :=
@@ -345,7 +346,7 @@ theorem MemBaseSet.exists_common_compl (h₁ : l.MemBaseSet I c₁ r₁ π₁) (
       (l.bDistortion → π.distortion ≤ c₁) ∧ (l.bDistortion → π.distortion ≤ c₂) := by
   wlog hc : c₁ ≤ c₂ with H
   · simpa [hU, _root_.and_comm] using
-      @H _ _ I J c c₂ c₁ r r₂ r₁ π π₂ π₁ _ l₂ l₁ h₂ h₁ hU.symm (le_of_not_le hc)
+      @H _ _ I J c c₂ c₁ _ l₂ l₁ r r₂ r₁ π π₂ π₁ h₂ h₁ hU.symm (le_of_not_le hc)
   by_cases hD : (l.bDistortion : Prop)
   · rcases h₁.4 hD with ⟨π, hπU, hπc⟩
     exact ⟨π, hπU, fun _ => hπc, fun _ => hπc.trans hc⟩

Mathlib/Analysis/Convex/Radon.lean

@@ -64,14 +64,14 @@ theorem radon_partition {f : ι → E} (h : ¬ AffineIndependent 𝕜 f) :
 
 open FiniteDimensional
 
-variable [FiniteDimensional 𝕜 E]
-
 /-- Corner case for `helly_theorem'`. -/
 private lemma helly_theorem_corner {F : ι → Set E} {s : Finset ι}
     (h_card_small : s.card ≤ finrank 𝕜 E + 1)
     (h_inter : ∀ I ⊆ s, I.card ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
     (⋂ i ∈ s, F i).Nonempty := h_inter s (by simp) h_card_small
 
+variable [FiniteDimensional 𝕜 E]
+
 /-- **Helly's theorem** for finite families of convex sets.
 
 If `F` is a finite family of convex sets in a vector space of finite dimension `d`, and any

Mathlib/Data/Matrix/ColumnRowPartitioned.lean

@@ -26,10 +26,6 @@ namespace Matrix
 
 variable {R : Type*}
 variable {m m₁ m₂ n n₁ n₂ : Type*}
-variable [Fintype m] [Fintype m₁] [Fintype m₂]
-variable [Fintype n] [Fintype n₁] [Fintype n₂]
-variable [DecidableEq m] [DecidableEq m₁] [DecidableEq m₂]
-variable [DecidableEq n] [DecidableEq n₁] [DecidableEq n₂]
 
 /-- Concatenate together two matrices A₁[m₁ × N] and A₂[m₂ × N] with the same columns (N) to get a
 bigger matrix indexed by [(m₁ ⊕ m₂) × N] -/
@@ -158,41 +154,53 @@ lemma fromColumns_neg (A₁ : Matrix n m₁ R) (A₂ : Matrix n m₂ R) :
 
 end Neg
 
+@[simp]
+lemma fromColumns_fromRows_eq_fromBlocks (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R)
+    (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
+    fromColumns (fromRows B₁₁ B₂₁) (fromRows B₁₂ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ := by
+  ext (_ | _) (_ | _) <;> simp
+
+@[simp]
+lemma fromRows_fromColumn_eq_fromBlocks (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R)
+    (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
+    fromRows (fromColumns B₁₁ B₁₂) (fromColumns B₂₁ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ := by
+  ext (_ | _) (_ | _) <;> simp
+
 section Semiring
 
 variable [Semiring R]
 
 @[simp]
-lemma fromRows_mulVec (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (v : n → R) :
+lemma fromRows_mulVec [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (v : n → R) :
     fromRows A₁ A₂ *ᵥ v = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) := by
   ext (_ | _) <;> rfl
 
 @[simp]
-lemma vecMul_fromColumns (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) :
+lemma vecMul_fromColumns [Fintype m] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) :
     v ᵥ* fromColumns B₁ B₂ = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) := by
   ext (_ | _) <;> rfl
 
 @[simp]
-lemma sum_elim_vecMul_fromRows (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R)
+lemma sum_elim_vecMul_fromRows [Fintype m₁] [Fintype m₂] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R)
     (v₁ : m₁ → R) (v₂ : m₂ → R) :
     Sum.elim v₁ v₂ ᵥ* fromRows B₁ B₂ = v₁ ᵥ* B₁ + v₂ ᵥ* B₂ := by
   ext
   simp [Matrix.vecMul, fromRows, dotProduct]
 
 @[simp]
-lemma fromColumns_mulVec_sum_elim (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R)
-    (v₁ : n₁ → R) (v₂ : n₂ → R) :
+lemma fromColumns_mulVec_sum_elim [Fintype n₁] [Fintype n₂]
+    (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R) (v₂ : n₂ → R) :
     fromColumns A₁ A₂ *ᵥ Sum.elim v₁ v₂ = A₁ *ᵥ v₁ + A₂ *ᵥ v₂ := by
   ext
   simp [Matrix.mulVec, fromColumns]
 
 @[simp]
-lemma fromRows_mul (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B : Matrix n m R) :
+lemma fromRows_mul [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B : Matrix n m R) :
     fromRows A₁ A₂ * B = fromRows (A₁ * B) (A₂ * B) := by
   ext (_ | _) _ <;> simp [mul_apply]
 
 @[simp]
-lemma mul_fromColumns (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
+lemma mul_fromColumns [Fintype n] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
     A * fromColumns B₁ B₂ = fromColumns (A * B₁) (A * B₂) := by
   ext _ (_ | _) <;> simp [mul_apply]
 
@@ -204,42 +212,30 @@ lemma fromRows_zero : fromRows (0 : Matrix m₁ n R) (0 : Matrix m₂ n R) = 0 :
 lemma fromColumns_zero : fromColumns (0 : Matrix m n₁ R) (0 : Matrix m n₂ R) = 0 := by
   ext _ (_ | _) <;> simp
 
-@[simp]
-lemma fromColumns_fromRows_eq_fromBlocks (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R)
-    (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
-    fromColumns (fromRows B₁₁ B₂₁) (fromRows B₁₂ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ := by
-  ext (_ | _) (_ | _) <;> simp
-
-@[simp]
-lemma fromRows_fromColumn_eq_fromBlocks (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R)
-    (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
-    fromRows (fromColumns B₁₁ B₁₂) (fromColumns B₂₁ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ := by
-  ext (_ | _) (_ | _) <;> simp
-
 /-- A row partitioned matrix multiplied by a column partioned matrix gives a 2 by 2 block matrix -/
-lemma fromRows_mul_fromColumns (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R)
+lemma fromRows_mul_fromColumns [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R)
     (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
     (fromRows A₁ A₂) * (fromColumns B₁ B₂) =
       fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) := by
   ext (_ | _) (_ | _) <;> simp
 
 /-- A column partitioned matrix mulitplied by a row partitioned matrix gives the sum of the "outer"
 products of the block matrices -/
-lemma fromColumns_mul_fromRows (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R)
+lemma fromColumns_mul_fromRows [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R)
     (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
     fromColumns A₁ A₂ * fromRows B₁ B₂ = (A₁ * B₁ + A₂ * B₂) := by
   ext
   simp [mul_apply]
 
 /-- A column partitioned matrix multipiled by a block matrix results in a column partioned matrix -/
-lemma fromColumns_mul_fromBlocks (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R)
+lemma fromColumns_mul_fromBlocks [Fintype m₁] [Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R)
     (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
     (fromColumns A₁ A₂) * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ =
       fromColumns (A₁ * B₁₁ + A₂ * B₂₁) (A₁ * B₁₂ + A₂ * B₂₂) := by
   ext _ (_ | _) <;> simp [mul_apply]
 
 /-- A block matrix mulitplied by a row partitioned matrix gives a row partitioned matrix -/
-lemma fromBlocks_mul_fromRows (A₁ : Matrix n₁ n R) (A₂ : Matrix n₂ n R)
+lemma fromBlocks_mul_fromRows [Fintype n₁] [Fintype n₂] (A₁ : Matrix n₁ n R) (A₂ : Matrix n₂ n R)
     (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
     fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * (fromRows A₁ A₂) =
       fromRows (B₁₁ * A₁ + B₁₂ * A₂) (B₂₁ * A₁ + B₂₂ * A₂) := by
@@ -256,7 +252,9 @@ This is the column and row partitioned matrix form of `Matrix.mul_eq_one_comm`.
 
 The condition `e : n ≃ n₁ ⊕ n₂` states that `fromColumns A₁ A₂` and `fromRows B₁ B₂` are "square".
 -/
-lemma fromColumns_mul_fromRows_eq_one_comm (e : n ≃ n₁ ⊕ n₂)
+lemma fromColumns_mul_fromRows_eq_one_comm
+    [Fintype n₁] [Fintype n₂] [Fintype n] [DecidableEq n] [DecidableEq n₁] [DecidableEq n₂]
+    (e : n ≃ n₁ ⊕ n₂)
     (A₁ : Matrix n n₁ R) (A₂ : Matrix n n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
     fromColumns A₁ A₂ * fromRows B₁ B₂ = 1 ↔ fromRows B₁ B₂ * fromColumns A₁ A₂ = 1 := by
   calc fromColumns A₁ A₂ * fromRows B₁ B₂ = 1
@@ -272,7 +270,8 @@ lemma fromColumns_mul_fromRows_eq_one_comm (e : n ≃ n₁ ⊕ n₂)
 
 /-- The lemma `fromColumns_mul_fromRows_eq_one_comm` specialized to the case where the index sets n₁
 and n₂, are the result of subtyping by a predicate and its complement. -/
-lemma equiv_compl_fromColumns_mul_fromRows_eq_one_comm (p : n → Prop)[DecidablePred p]
+lemma equiv_compl_fromColumns_mul_fromRows_eq_one_comm
+    [Fintype n] [DecidableEq n] (p : n → Prop) [DecidablePred p]
     (A₁ : Matrix n {i // p i} R) (A₂ : Matrix n {i // ¬p i} R)
     (B₁ : Matrix {i // p i} n R) (B₂ : Matrix {i // ¬p i} n R) :
     fromColumns A₁ A₂ * fromRows B₁ B₂ = 1 ↔ fromRows B₁ B₂ * fromColumns A₁ A₂ = 1 :=

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

@@ -320,7 +320,6 @@ end Inv
 
 section InjectiveMul
 variable [Fintype n] [Fintype m] [DecidableEq m] [CommRing α]
-variable [Fintype l] [DecidableEq l]
 
 lemma mul_left_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) :
     Function.Injective (fun x : Matrix l m α => x * A) := fun _ _ g => by
@@ -334,13 +333,12 @@ end InjectiveMul
 
 section vecMul
 
-variable [DecidableEq m] [DecidableEq n]
-
 section Semiring
 
 variable {R : Type*} [Semiring R]
 
-theorem vecMul_surjective_iff_exists_left_inverse [Fintype m] [Finite n] {A : Matrix m n R} :
+theorem vecMul_surjective_iff_exists_left_inverse
+    [DecidableEq n] [Fintype m] [Finite n] {A : Matrix m n R} :
     Function.Surjective A.vecMul ↔ ∃ B : Matrix n m R, B * A = 1 := by
   cases nonempty_fintype n
   refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨y ᵥ* B, by simp [hBA]⟩⟩
@@ -349,7 +347,8 @@ theorem vecMul_surjective_iff_exists_left_inverse [Fintype m] [Finite n] {A : Ma
   rw [mul_apply_eq_vecMul, one_eq_pi_single, ← hrows]
   rfl
 
-theorem mulVec_surjective_iff_exists_right_inverse [Finite m] [Fintype n] {A : Matrix m n R} :
+theorem mulVec_surjective_iff_exists_right_inverse
+    [DecidableEq m] [Finite m] [Fintype n] {A : Matrix m n R} :
     Function.Surjective A.mulVec ↔ ∃ B : Matrix n m R, A * B = 1 := by
   cases nonempty_fintype m
   refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B *ᵥ y, by simp [hBA]⟩⟩
@@ -360,7 +359,7 @@ theorem mulVec_surjective_iff_exists_right_inverse [Finite m] [Fintype n] {A : M
 
 end Semiring
 
-variable {R K : Type*} [CommRing R] [Field K] [Fintype m]
+variable [DecidableEq m] {R K : Type*} [CommRing R] [Field K] [Fintype m]
 
 theorem vecMul_surjective_iff_isUnit {A : Matrix m m R} :
     Function.Surjective A.vecMul ↔ IsUnit A := by
@@ -711,7 +710,7 @@ end Submatrix
 
 section Det
 
-variable [Fintype m] [DecidableEq m] [CommRing α]
+variable [Fintype m] [DecidableEq m]
 
 /-- A variant of `Matrix.det_units_conj`. -/
 theorem det_conj {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :

Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

@@ -137,7 +137,7 @@ This section deals with the conversion between matrices and sesquilinear maps on
 -/
 
 variable [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂]
-  [SMulCommClass R R N₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂]
+  [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂]
   [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂]
 variable {σ₁ : R₁ →+* S₁} {σ₂ : R₂ →+* S₂}
 variable [Fintype n] [Fintype m]

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

@@ -780,13 +780,15 @@ theorem _root_.QuadraticMap.polarBilin_comp (Q : QuadraticMap R N' N) (f : M →
 
 end
 
-variable {N' : Type*} [AddCommGroup N'] [Module R N']
+variable {N' : Type*} [AddCommGroup N']
 
 theorem _root_.LinearMap.compQuadraticMap_polar [CommSemiring S] [Algebra S R] [Module S N]
     [Module S N'] [IsScalarTower S R N] [Module S M] [IsScalarTower S R M] (f : N →ₗ[S] N')
     (Q : QuadraticMap R M N) (x y : M) : polar (f.compQuadraticMap' Q) x y = f (polar Q x y) := by
   simp [polar]
 
+variable [Module R N']
+
 theorem _root_.LinearMap.compQuadraticMap_polarBilin (f : N →ₗ[R] N') (Q : QuadraticMap R M N) :
     (f.compQuadraticMap' Q).polarBilin = Q.polarBilin.compr₂ f := by
   ext
@@ -1032,7 +1034,7 @@ end Anisotropic
 section PosDef
 
 variable {R₂ : Type u} [CommSemiring R₂] [AddCommMonoid M] [Module R₂ M]
-variable [PartialOrder N] [AddCommMonoid N] [Module R₂ N] [CovariantClass N N (· + ·) (· < ·)]
+variable [PartialOrder N] [AddCommMonoid N] [Module R₂ N]
 variable {Q₂ : QuadraticMap R₂ M N}
 
 /-- A positive definite quadratic form is positive on nonzero vectors. -/
@@ -1057,13 +1059,16 @@ theorem PosDef.anisotropic {Q : QuadraticMap R₂ M N} (hQ : Q.PosDef) : Q.Aniso
       exact this
 
 theorem posDef_of_nonneg {Q : QuadraticMap R₂ M N} (h : ∀ x, 0 ≤ Q x) (h0 : Q.Anisotropic) :
-    PosDef Q := fun x hx => lt_of_le_of_ne (h x) (Ne.symm fun hQx => hx <| h0 _ hQx)
+    PosDef Q :=
+  fun x hx => lt_of_le_of_ne (h x) (Ne.symm fun hQx => hx <| h0 _ hQx)
 
 theorem posDef_iff_nonneg {Q : QuadraticMap R₂ M N} : PosDef Q ↔ (∀ x, 0 ≤ Q x) ∧ Q.Anisotropic :=
   ⟨fun h => ⟨h.nonneg, h.anisotropic⟩, fun ⟨n, a⟩ => posDef_of_nonneg n a⟩
 
-theorem PosDef.add (Q Q' : QuadraticMap R₂ M N) (hQ : PosDef Q) (hQ' : PosDef Q') :
-    PosDef (Q + Q') := fun x hx => add_pos (hQ x hx) (hQ' x hx)
+theorem PosDef.add [CovariantClass N N (· + ·) (· < ·)]
+    (Q Q' : QuadraticMap R₂ M N) (hQ : PosDef Q) (hQ' : PosDef Q') :
+    PosDef (Q + Q') :=
+  fun x hx => add_pos (hQ x hx) (hQ' x hx)
 
 theorem linMulLinSelfPosDef {R} [LinearOrderedCommRing R] [Module R M] [LinearOrderedSemiring A]
     [ExistsAddOfLE A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (f : M →ₗ[R] A)

Mathlib/RepresentationTheory/Maschke.lean

@@ -71,11 +71,12 @@ theorem conjugate_apply (g : G) (v : W) :
     π.conjugate g v = MonoidAlgebra.single g⁻¹ (1 : k) • π (MonoidAlgebra.single g (1 : k) • v) :=
   rfl
 
-variable (i : V →ₗ[MonoidAlgebra k G] W) (h : ∀ v : V, (π : W → V) (i v) = v)
+variable (i : V →ₗ[MonoidAlgebra k G] W)
 
 section
 
-theorem conjugate_i (g : G) (v : V) : (conjugate π g : W → V) (i v) = v := by
+theorem conjugate_i (h : ∀ v : V, (π : W → V) (i v) = v) (g : G) (v : V) :
+    (conjugate π g : W → V) (i v) = v := by
   rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, mul_left_inv,
     ← one_def, one_smul]
 
@@ -119,7 +120,8 @@ theorem equivariantProjection_apply (v : W) :
     π.equivariantProjection G v = ⅟(Fintype.card G : k) • ∑ g : G, π.conjugate g v := by
   simp only [equivariantProjection, smul_apply, sumOfConjugatesEquivariant_apply]
 
-theorem equivariantProjection_condition (v : V) : (π.equivariantProjection G) (i v) = v := by
+theorem equivariantProjection_condition (h : ∀ v : V, (π : W → V) (i v) = v) (v : V) :
+    (π.equivariantProjection G) (i v) = v := by
   rw [equivariantProjection_apply]
   simp only [conjugate_i π i h]
   rw [Finset.sum_const, Finset.card_univ, ← Nat.cast_smul_eq_nsmul k, smul_smul,

Mathlib/RingTheory/SimpleModule.lean

@@ -68,12 +68,14 @@ theorem IsSimpleModule.nontrivial [IsSimpleModule R M] : Nontrivial M :=
       ext x
       simp [Submodule.mem_bot, Submodule.mem_top, h x]⟩⟩
 
-variable {m : Submodule R M} {N : Type*} [AddCommGroup N] [Module R N] {R S M}
+variable {m : Submodule R M} {N : Type*} [AddCommGroup N] {R S M}
 
 theorem LinearMap.isSimpleModule_iff_of_bijective [Module S N] {σ : R →+* S} [RingHomSurjective σ]
     (l : M →ₛₗ[σ] N) (hl : Function.Bijective l) : IsSimpleModule R M ↔ IsSimpleModule S N :=
   (Submodule.orderIsoMapComapOfBijective l hl).isSimpleOrder_iff
 
+variable [Module R N]
+
 theorem IsSimpleModule.congr (l : M ≃ₗ[R] N) [IsSimpleModule R N] : IsSimpleModule R M :=
   (Submodule.orderIsoMapComap l).isSimpleOrder
 
@@ -204,7 +206,7 @@ instance submodule {m : Submodule R M} : IsSemisimpleModule R m :=
 variable {R M}
 open LinearMap
 
-theorem congr [IsSemisimpleModule R N] (e : M ≃ₗ[R] N) : IsSemisimpleModule R M :=
+theorem congr (e : N ≃ₗ[R] M) : IsSemisimpleModule R N :=
   (Submodule.orderIsoMapComap e.symm).complementedLattice
 
 instance quotient : IsSemisimpleModule R (M ⧸ m) :=
@@ -217,19 +219,21 @@ protected theorem range (f : M →ₗ[R] N) : IsSemisimpleModule R (range f) :=
 
 section
 
-variable [Module S N] {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] N)
+variable {M' : Type*} [AddCommGroup M'] [Module R M'] {N'} [AddCommGroup N'] [Module S N']
+  {σ : R →+* S} (l : M' →ₛₗ[σ] N')
 
-theorem _root_.LinearMap.isSemisimpleModule_iff_of_bijective (hl : Function.Bijective l) :
-    IsSemisimpleModule R M ↔ IsSemisimpleModule S N :=
+theorem _root_.LinearMap.isSemisimpleModule_iff_of_bijective
+    [RingHomSurjective σ] (hl : Function.Bijective l) :
+    IsSemisimpleModule R M' ↔ IsSemisimpleModule S N' :=
   (Submodule.orderIsoMapComapOfBijective l hl).complementedLattice_iff
 
 -- TODO: generalize Submodule.equivMapOfInjective from InvPair to RingHomSurjective
 proof_wanted _root_.LinearMap.isSemisimpleModule_of_injective (_ : Function.Injective l)
-    [IsSemisimpleModule S N] : IsSemisimpleModule R M
+    [IsSemisimpleModule S N'] : IsSemisimpleModule R M'
 
 --TODO: generalize LinearMap.quotKerEquivOfSurjective to SemilinearMaps + RingHomSurjective
 proof_wanted _root_.LinearMap.isSemisimpleModule_of_surjective (_ : Function.Surjective l)
-    [IsSemisimpleModule R M] : IsSemisimpleModule S N
+    [IsSemisimpleModule R M'] : IsSemisimpleModule S N'
 
 end