[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ det (mvPolynomialX m m R) ≠ 0
[PROOFSTEP]
intro h_det
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : det (mvPolynomialX m m R) = 0
⊢ False
[PROOFSTEP]
have := congr_arg Matrix.det (mvPolynomialX_mapMatrix_eval (1 : Matrix m m R))
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : det (mvPolynomialX m m R) = 0
this : det (↑(RingHom.mapMatrix (MvPolynomial.eval fun p => OfNat.ofNat 1 p.fst p.snd)) (mvPolynomialX m m R)) = det 1
⊢ False
[PROOFSTEP]
rw [det_one, ← RingHom.map_det, h_det, RingHom.map_zero] at this 
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : det (mvPolynomialX m m R) = 0
this : 0 = 1
⊢ False
[PROOFSTEP]
exact zero_ne_one this
