bump to nightly-2023-04-24-02

mathlib commit leanprover-community/mathlib@0907952

Mathbin/Analysis/Normed/Group/Seminorm.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: María Inés de Frutos-Fernández, Yaël Dillies
 
 ! This file was ported from Lean 3 source module analysis.normed.group.seminorm
-! leanprover-community/mathlib commit 69c6a5a12d8a2b159f20933e60115a4f2de62b58
+! leanprover-community/mathlib commit 09079525fd01b3dda35e96adaa08d2f943e1648c
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -666,7 +666,7 @@ instance [SMul R' ℝ] [SMul R' ℝ≥0] [IsScalarTower R' ℝ≥0 ℝ] [SMul R
 theorem smul_sup (r : R) (p q : AddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q :=
   have real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
     simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
-      mul_max_of_nonneg x y (r • 1 : ℝ≥0).Prop
+      mul_max_of_nonneg x y (r • 1 : ℝ≥0).coe_nonneg
   ext fun x => real.smul_max _ _
 #align add_group_seminorm.smul_sup AddGroupSeminorm.smul_sup
 -/
@@ -927,7 +927,7 @@ theorem smul_apply (r : R) (p : GroupSeminorm E) (x : E) : (r • p) x = r • p
 theorem smul_sup (r : R) (p q : GroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q :=
   have real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
     simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
-      mul_max_of_nonneg x y (r • 1 : ℝ≥0).Prop
+      mul_max_of_nonneg x y (r • 1 : ℝ≥0).coe_nonneg
   ext fun x => real.smul_max _ _
 #align group_seminorm.smul_sup GroupSeminorm.smul_sup
 #align add_group_seminorm.smul_sup AddGroupSeminorm.smul_sup
@@ -1006,7 +1006,7 @@ theorem smul_apply (r : R) (p : NonarchAddGroupSeminorm E) (x : E) : (r • p) x
 theorem smul_sup (r : R) (p q : NonarchAddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q :=
   have real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
     simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
-      mul_max_of_nonneg x y (r • 1 : ℝ≥0).Prop
+      mul_max_of_nonneg x y (r • 1 : ℝ≥0).coe_nonneg
   ext fun x => real.smul_max _ _
 #align nonarch_add_group_seminorm.smul_sup NonarchAddGroupSeminorm.smul_sup
 -/

Mathbin/Analysis/Seminorm.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean Lo, Yaël Dillies, Moritz Doll
 
 ! This file was ported from Lean 3 source module analysis.seminorm
-! leanprover-community/mathlib commit 7ebf83ed9c262adbf983ef64d5e8c2ae94b625f4
+! leanprover-community/mathlib commit 09079525fd01b3dda35e96adaa08d2f943e1648c
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -248,7 +248,7 @@ theorem smul_sup [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] (r
     r • (p ⊔ q) = r • p ⊔ r • q :=
   have real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
     simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
-      mul_max_of_nonneg x y (r • 1 : ℝ≥0).Prop
+      mul_max_of_nonneg x y (r • 1 : ℝ≥0).coe_nonneg
   ext fun x => real.smul_max _ _
 #align seminorm.smul_sup Seminorm.smul_sup
 

Mathbin/Data/Matrix/Notation.lean

@@ -383,7 +383,7 @@ variable [Semiring α]
 lean 3 declaration is
   forall {α : Type.{u1}} {o' : Type.{u2}} [_inst_1 : Semiring.{u1} α] (v : (Fin (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))) -> α) (B : Matrix.{0, u2, u1} (Fin (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))) o' α), Eq.{max (succ u2) (succ u1)} (o' -> α) (Matrix.vecMul.{u1, 0, u2} (Fin (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))) o' α (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} α (Semiring.toNonAssocSemiring.{u1} α _inst_1)) (Fin.fintype (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))) v B) (OfNat.ofNat.{max u2 u1} (o' -> α) 0 (OfNat.mk.{max u2 u1} (o' -> α) 0 (Zero.zero.{max u2 u1} (o' -> α) (Pi.instZero.{u2, u1} o' (fun (ᾰ : o') => α) (fun (i : o') => MulZeroClass.toHasZero.{u1} α (NonUnitalNonAssocSemiring.toMulZeroClass.{u1} α (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} α (Semiring.toNonAssocSemiring.{u1} α _inst_1))))))))
 but is expected to have type
-  forall {α : Type.{u1}} {o' : Type.{u2}} [_inst_1 : Semiring.{u1} α] (v : (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) -> α) (B : Matrix.{0, u2, u1} (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) o' α), Eq.{max (succ u1) (succ u2)} (o' -> α) (Matrix.vecMul.{u1, 0, u2} (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) o' α (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} α (Semiring.toNonAssocSemiring.{u1} α _inst_1)) (Fin.fintype (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) v B) (OfNat.ofNat.{max u1 u2} (o' -> α) 0 (Zero.toOfNat0.{max u1 u2} (o' -> α) (Pi.instZero.{u2, u1} o' (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.17912 : o') => α) (fun (i : o') => MonoidWithZero.toZero.{u1} α (Semiring.toMonoidWithZero.{u1} α _inst_1)))))
+  forall {α : Type.{u1}} {o' : Type.{u2}} [_inst_1 : Semiring.{u1} α] (v : (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) -> α) (B : Matrix.{0, u2, u1} (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) o' α), Eq.{max (succ u1) (succ u2)} (o' -> α) (Matrix.vecMul.{u1, 0, u2} (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) o' α (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} α (Semiring.toNonAssocSemiring.{u1} α _inst_1)) (Fin.fintype (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) v B) (OfNat.ofNat.{max u1 u2} (o' -> α) 0 (Zero.toOfNat0.{max u1 u2} (o' -> α) (Pi.instZero.{u2, u1} o' (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.18134 : o') => α) (fun (i : o') => MonoidWithZero.toZero.{u1} α (Semiring.toMonoidWithZero.{u1} α _inst_1)))))
 Case conversion may be inaccurate. Consider using '#align matrix.empty_vec_mul Matrix.empty_vecMulₓ'. -/
 @[simp]
 theorem empty_vecMul (v : Fin 0 → α) (B : Matrix (Fin 0) o' α) : vecMul v B = 0 :=
@@ -441,7 +441,7 @@ theorem empty_mulVec [Fintype n'] (A : Matrix (Fin 0) n' α) (v : n' → α) : m
 lean 3 declaration is
   forall {α : Type.{u1}} {m' : Type.{u2}} [_inst_1 : Semiring.{u1} α] (A : Matrix.{u2, 0, u1} m' (Fin (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))) α) (v : (Fin (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))) -> α), Eq.{max (succ u2) (succ u1)} (m' -> α) (Matrix.mulVec.{u1, u2, 0} m' (Fin (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))) α (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} α (Semiring.toNonAssocSemiring.{u1} α _inst_1)) (Fin.fintype (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))) A v) (OfNat.ofNat.{max u2 u1} (m' -> α) 0 (OfNat.mk.{max u2 u1} (m' -> α) 0 (Zero.zero.{max u2 u1} (m' -> α) (Pi.instZero.{u2, u1} m' (fun (ᾰ : m') => α) (fun (i : m') => MulZeroClass.toHasZero.{u1} α (NonUnitalNonAssocSemiring.toMulZeroClass.{u1} α (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} α (Semiring.toNonAssocSemiring.{u1} α _inst_1))))))))
 but is expected to have type
-  forall {α : Type.{u1}} {m' : Type.{u2}} [_inst_1 : Semiring.{u1} α] (A : Matrix.{u2, 0, u1} m' (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) α) (v : (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) -> α), Eq.{max (succ u1) (succ u2)} (m' -> α) (Matrix.mulVec.{u1, u2, 0} m' (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) α (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} α (Semiring.toNonAssocSemiring.{u1} α _inst_1)) (Fin.fintype (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) A v) (OfNat.ofNat.{max u1 u2} (m' -> α) 0 (Zero.toOfNat0.{max u1 u2} (m' -> α) (Pi.instZero.{u2, u1} m' (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.17854 : m') => α) (fun (i : m') => MonoidWithZero.toZero.{u1} α (Semiring.toMonoidWithZero.{u1} α _inst_1)))))
+  forall {α : Type.{u1}} {m' : Type.{u2}} [_inst_1 : Semiring.{u1} α] (A : Matrix.{u2, 0, u1} m' (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) α) (v : (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) -> α), Eq.{max (succ u1) (succ u2)} (m' -> α) (Matrix.mulVec.{u1, u2, 0} m' (Fin (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) α (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} α (Semiring.toNonAssocSemiring.{u1} α _inst_1)) (Fin.fintype (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) A v) (OfNat.ofNat.{max u1 u2} (m' -> α) 0 (Zero.toOfNat0.{max u1 u2} (m' -> α) (Pi.instZero.{u2, u1} m' (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.18076 : m') => α) (fun (i : m') => MonoidWithZero.toZero.{u1} α (Semiring.toMonoidWithZero.{u1} α _inst_1)))))
 Case conversion may be inaccurate. Consider using '#align matrix.mul_vec_empty Matrix.mulVec_emptyₓ'. -/
 @[simp]
 theorem mulVec_empty (A : Matrix m' (Fin 0) α) (v : Fin 0 → α) : mulVec A v = 0 :=

Mathbin/LinearAlgebra/Matrix/Nondegenerate.lean

@@ -93,7 +93,7 @@ theorem nondegenerate_of_det_ne_zero [DecidableEq m] {M : Matrix m m A} (hM : M.
 lean 3 declaration is
   forall {m : Type.{u1}} {A : Type.{u2}} [_inst_1 : Fintype.{u1} m] [_inst_3 : CommRing.{u2} A] [_inst_4 : IsDomain.{u2} A (Ring.toSemiring.{u2} A (CommRing.toRing.{u2} A _inst_3))] [_inst_5 : DecidableEq.{succ u1} m] {M : Matrix.{u1, u1, u2} m m A}, (Ne.{succ u2} A (Matrix.det.{u2, u1} m (fun (a : m) (b : m) => _inst_5 a b) _inst_1 A _inst_3 M) (OfNat.ofNat.{u2} A 0 (OfNat.mk.{u2} A 0 (Zero.zero.{u2} A (MulZeroClass.toHasZero.{u2} A (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} A (NonAssocRing.toNonUnitalNonAssocRing.{u2} A (Ring.toNonAssocRing.{u2} A (CommRing.toRing.{u2} A _inst_3)))))))))) -> (forall {v : m -> A}, (Eq.{max (succ u1) (succ u2)} (m -> A) (Matrix.vecMul.{u2, u1, u1} m m A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} A (NonAssocRing.toNonUnitalNonAssocRing.{u2} A (Ring.toNonAssocRing.{u2} A (CommRing.toRing.{u2} A _inst_3)))) _inst_1 v M) (OfNat.ofNat.{max u1 u2} (m -> A) 0 (OfNat.mk.{max u1 u2} (m -> A) 0 (Zero.zero.{max u1 u2} (m -> A) (Pi.instZero.{u1, u2} m (fun (ᾰ : m) => A) (fun (i : m) => MulZeroClass.toHasZero.{u2} A (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} A (NonAssocRing.toNonUnitalNonAssocRing.{u2} A (Ring.toNonAssocRing.{u2} A (CommRing.toRing.{u2} A _inst_3))))))))))) -> (Eq.{max (succ u1) (succ u2)} (m -> A) v (OfNat.ofNat.{max u1 u2} (m -> A) 0 (OfNat.mk.{max u1 u2} (m -> A) 0 (Zero.zero.{max u1 u2} (m -> A) (Pi.instZero.{u1, u2} m (fun (ᾰ : m) => A) (fun (i : m) => MulZeroClass.toHasZero.{u2} A (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} A (NonAssocRing.toNonUnitalNonAssocRing.{u2} A (Ring.toNonAssocRing.{u2} A (CommRing.toRing.{u2} A _inst_3))))))))))))
 but is expected to have type
-  forall {m : Type.{u2}} {A : Type.{u1}} [_inst_1 : Fintype.{u2} m] [_inst_3 : CommRing.{u1} A] [_inst_4 : IsDomain.{u1} A (Ring.toSemiring.{u1} A (CommRing.toRing.{u1} A _inst_3))] [_inst_5 : DecidableEq.{succ u2} m] {M : Matrix.{u2, u2, u1} m m A}, (Ne.{succ u1} A (Matrix.det.{u1, u2} m (fun (a : m) (b : m) => _inst_5 a b) _inst_1 A _inst_3 M) (OfNat.ofNat.{u1} A 0 (Zero.toOfNat0.{u1} A (CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4)))))) -> (forall {v : m -> A}, (Eq.{max (succ u2) (succ u1)} (m -> A) (Matrix.vecMul.{u1, u2, u2} m m A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} A (NonAssocRing.toNonUnitalNonAssocRing.{u1} A (Ring.toNonAssocRing.{u1} A (CommRing.toRing.{u1} A _inst_3)))) _inst_1 v M) (OfNat.ofNat.{max u2 u1} (m -> A) 0 (Zero.toOfNat0.{max u2 u1} (m -> A) (Pi.instZero.{u2, u1} m (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.17912 : m) => A) (fun (i : m) => CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4))))))) -> (Eq.{max (succ u2) (succ u1)} (m -> A) v (OfNat.ofNat.{max u2 u1} (m -> A) 0 (Zero.toOfNat0.{max u2 u1} (m -> A) (Pi.instZero.{u2, u1} m (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.17912 : m) => A) (fun (i : m) => CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4))))))))
+  forall {m : Type.{u2}} {A : Type.{u1}} [_inst_1 : Fintype.{u2} m] [_inst_3 : CommRing.{u1} A] [_inst_4 : IsDomain.{u1} A (Ring.toSemiring.{u1} A (CommRing.toRing.{u1} A _inst_3))] [_inst_5 : DecidableEq.{succ u2} m] {M : Matrix.{u2, u2, u1} m m A}, (Ne.{succ u1} A (Matrix.det.{u1, u2} m (fun (a : m) (b : m) => _inst_5 a b) _inst_1 A _inst_3 M) (OfNat.ofNat.{u1} A 0 (Zero.toOfNat0.{u1} A (CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4)))))) -> (forall {v : m -> A}, (Eq.{max (succ u2) (succ u1)} (m -> A) (Matrix.vecMul.{u1, u2, u2} m m A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} A (NonAssocRing.toNonUnitalNonAssocRing.{u1} A (Ring.toNonAssocRing.{u1} A (CommRing.toRing.{u1} A _inst_3)))) _inst_1 v M) (OfNat.ofNat.{max u2 u1} (m -> A) 0 (Zero.toOfNat0.{max u2 u1} (m -> A) (Pi.instZero.{u2, u1} m (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.18134 : m) => A) (fun (i : m) => CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4))))))) -> (Eq.{max (succ u2) (succ u1)} (m -> A) v (OfNat.ofNat.{max u2 u1} (m -> A) 0 (Zero.toOfNat0.{max u2 u1} (m -> A) (Pi.instZero.{u2, u1} m (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.18134 : m) => A) (fun (i : m) => CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4))))))))
 Case conversion may be inaccurate. Consider using '#align matrix.eq_zero_of_vec_mul_eq_zero Matrix.eq_zero_of_vecMul_eq_zeroₓ'. -/
 theorem eq_zero_of_vecMul_eq_zero [DecidableEq m] {M : Matrix m m A} (hM : M.det ≠ 0) {v : m → A}
     (hv : M.vecMul v = 0) : v = 0 :=
@@ -105,7 +105,7 @@ theorem eq_zero_of_vecMul_eq_zero [DecidableEq m] {M : Matrix m m A} (hM : M.det
 lean 3 declaration is
   forall {m : Type.{u1}} {A : Type.{u2}} [_inst_1 : Fintype.{u1} m] [_inst_3 : CommRing.{u2} A] [_inst_4 : IsDomain.{u2} A (Ring.toSemiring.{u2} A (CommRing.toRing.{u2} A _inst_3))] [_inst_5 : DecidableEq.{succ u1} m] {M : Matrix.{u1, u1, u2} m m A}, (Ne.{succ u2} A (Matrix.det.{u2, u1} m (fun (a : m) (b : m) => _inst_5 a b) _inst_1 A _inst_3 M) (OfNat.ofNat.{u2} A 0 (OfNat.mk.{u2} A 0 (Zero.zero.{u2} A (MulZeroClass.toHasZero.{u2} A (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} A (NonAssocRing.toNonUnitalNonAssocRing.{u2} A (Ring.toNonAssocRing.{u2} A (CommRing.toRing.{u2} A _inst_3)))))))))) -> (forall {v : m -> A}, (Eq.{max (succ u1) (succ u2)} (m -> A) (Matrix.mulVec.{u2, u1, u1} m m A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} A (NonAssocRing.toNonUnitalNonAssocRing.{u2} A (Ring.toNonAssocRing.{u2} A (CommRing.toRing.{u2} A _inst_3)))) _inst_1 M v) (OfNat.ofNat.{max u1 u2} (m -> A) 0 (OfNat.mk.{max u1 u2} (m -> A) 0 (Zero.zero.{max u1 u2} (m -> A) (Pi.instZero.{u1, u2} m (fun (ᾰ : m) => A) (fun (i : m) => MulZeroClass.toHasZero.{u2} A (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} A (NonAssocRing.toNonUnitalNonAssocRing.{u2} A (Ring.toNonAssocRing.{u2} A (CommRing.toRing.{u2} A _inst_3))))))))))) -> (Eq.{max (succ u1) (succ u2)} (m -> A) v (OfNat.ofNat.{max u1 u2} (m -> A) 0 (OfNat.mk.{max u1 u2} (m -> A) 0 (Zero.zero.{max u1 u2} (m -> A) (Pi.instZero.{u1, u2} m (fun (ᾰ : m) => A) (fun (i : m) => MulZeroClass.toHasZero.{u2} A (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} A (NonAssocRing.toNonUnitalNonAssocRing.{u2} A (Ring.toNonAssocRing.{u2} A (CommRing.toRing.{u2} A _inst_3))))))))))))
 but is expected to have type
-  forall {m : Type.{u2}} {A : Type.{u1}} [_inst_1 : Fintype.{u2} m] [_inst_3 : CommRing.{u1} A] [_inst_4 : IsDomain.{u1} A (Ring.toSemiring.{u1} A (CommRing.toRing.{u1} A _inst_3))] [_inst_5 : DecidableEq.{succ u2} m] {M : Matrix.{u2, u2, u1} m m A}, (Ne.{succ u1} A (Matrix.det.{u1, u2} m (fun (a : m) (b : m) => _inst_5 a b) _inst_1 A _inst_3 M) (OfNat.ofNat.{u1} A 0 (Zero.toOfNat0.{u1} A (CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4)))))) -> (forall {v : m -> A}, (Eq.{max (succ u2) (succ u1)} (m -> A) (Matrix.mulVec.{u1, u2, u2} m m A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} A (NonAssocRing.toNonUnitalNonAssocRing.{u1} A (Ring.toNonAssocRing.{u1} A (CommRing.toRing.{u1} A _inst_3)))) _inst_1 M v) (OfNat.ofNat.{max u2 u1} (m -> A) 0 (Zero.toOfNat0.{max u2 u1} (m -> A) (Pi.instZero.{u2, u1} m (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.17854 : m) => A) (fun (i : m) => CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4))))))) -> (Eq.{max (succ u2) (succ u1)} (m -> A) v (OfNat.ofNat.{max u2 u1} (m -> A) 0 (Zero.toOfNat0.{max u2 u1} (m -> A) (Pi.instZero.{u2, u1} m (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.17854 : m) => A) (fun (i : m) => CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4))))))))
+  forall {m : Type.{u2}} {A : Type.{u1}} [_inst_1 : Fintype.{u2} m] [_inst_3 : CommRing.{u1} A] [_inst_4 : IsDomain.{u1} A (Ring.toSemiring.{u1} A (CommRing.toRing.{u1} A _inst_3))] [_inst_5 : DecidableEq.{succ u2} m] {M : Matrix.{u2, u2, u1} m m A}, (Ne.{succ u1} A (Matrix.det.{u1, u2} m (fun (a : m) (b : m) => _inst_5 a b) _inst_1 A _inst_3 M) (OfNat.ofNat.{u1} A 0 (Zero.toOfNat0.{u1} A (CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4)))))) -> (forall {v : m -> A}, (Eq.{max (succ u2) (succ u1)} (m -> A) (Matrix.mulVec.{u1, u2, u2} m m A (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} A (NonAssocRing.toNonUnitalNonAssocRing.{u1} A (Ring.toNonAssocRing.{u1} A (CommRing.toRing.{u1} A _inst_3)))) _inst_1 M v) (OfNat.ofNat.{max u2 u1} (m -> A) 0 (Zero.toOfNat0.{max u2 u1} (m -> A) (Pi.instZero.{u2, u1} m (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.18076 : m) => A) (fun (i : m) => CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4))))))) -> (Eq.{max (succ u2) (succ u1)} (m -> A) v (OfNat.ofNat.{max u2 u1} (m -> A) 0 (Zero.toOfNat0.{max u2 u1} (m -> A) (Pi.instZero.{u2, u1} m (fun (a._@.Mathlib.Data.Matrix.Basic._hyg.18076 : m) => A) (fun (i : m) => CommMonoidWithZero.toZero.{u1} A (CancelCommMonoidWithZero.toCommMonoidWithZero.{u1} A (IsDomain.toCancelCommMonoidWithZero.{u1} A (CommRing.toCommSemiring.{u1} A _inst_3) _inst_4))))))))
 Case conversion may be inaccurate. Consider using '#align matrix.eq_zero_of_mul_vec_eq_zero Matrix.eq_zero_of_mulVec_eq_zeroₓ'. -/
 theorem eq_zero_of_mulVec_eq_zero [DecidableEq m] {M : Matrix m m A} (hM : M.det ≠ 0) {v : m → A}
     (hv : M.mulVec v = 0) : v = 0 :=