m : Type u_1
n : Type ?u.39994
R : Type u_2
S : Type ?u.40000
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : det (mvPolynomialX m m R) = 0
⊢ False
m : Type u_1
n : Type ?u.39994
R : Type u_2
S : Type ?u.40000
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ det (mvPolynomialX m m R) ≠ 0
intro h_det
m : Type u_1
n : Type ?u.39994
R : Type u_2
S : Type ?u.40000
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
m : Type u_1
n : Type ?u.39994
R : Type u_2
S : Type ?u.40000
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : det (mvPolynomialX m m R) = 0
⊢ False
have := congr_arg Matrix.det (mvPolynomialX_mapMatrix_eval (1 : Matrix m m R))
m : Type u_1
n : Type ?u.39994
R : Type u_2
S : Type ?u.40000
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : det (mvPolynomialX m m R) = 0
this : 0 = 1
⊢ False
m : Type u_1
n : Type ?u.39994
R : Type u_2
S : Type ?u.40000
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
rw [det_one, ← RingHom.map_det, h_det, RingHom.map_zero] at this
no goals
m : Type u_1
n : Type ?u.39994
R : Type u_2
S : Type ?u.40000
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : det (mvPolynomialX m m R) = 0
this : 0 = 1
⊢ False
exact zero_ne_one this