[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ ∀ (a₁ a₂ : A) (b₁ b₂ : Matrix n n R),
    ↑(toFunLinear R A n) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      ↑(toFunLinear R A n) (a₁ ⊗ₜ[R] b₁) * ↑(toFunLinear R A n) (a₂ ⊗ₜ[R] b₂)
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
⊢ ↑(toFunLinear R A n) ((a₁✝ * a₂✝) ⊗ₜ[R] (b₁✝ * b₂✝)) =
    ↑(toFunLinear R A n) (a₁✝ ⊗ₜ[R] b₁✝) * ↑(toFunLinear R A n) (a₂✝ ⊗ₜ[R] b₂✝)
[PROOFSTEP]
simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply, Matrix.map_mul]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
⊢ (a₁✝ * a₂✝) • (Matrix.map b₁✝ ↑(algebraMap R A) * Matrix.map b₂✝ ↑(algebraMap R A)) =
    a₁✝ • Matrix.map b₁✝ ↑(algebraMap R A) * a₂✝ • Matrix.map b₂✝ ↑(algebraMap R A)
[PROOFSTEP]
ext
[GOAL]
case a.h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
i✝ x✝ : n
⊢ ((a₁✝ * a₂✝) • (Matrix.map b₁✝ ↑(algebraMap R A) * Matrix.map b₂✝ ↑(algebraMap R A))) i✝ x✝ =
    (a₁✝ • Matrix.map b₁✝ ↑(algebraMap R A) * a₂✝ • Matrix.map b₂✝ ↑(algebraMap R A)) i✝ x✝
[PROOFSTEP]
dsimp
[GOAL]
case a.h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
i✝ x✝ : n
⊢ a₁✝ * a₂✝ * (Matrix.map b₁✝ ↑(algebraMap R A) * Matrix.map b₂✝ ↑(algebraMap R A)) i✝ x✝ =
    (a₁✝ • Matrix.map b₁✝ ↑(algebraMap R A) * a₂✝ • Matrix.map b₂✝ ↑(algebraMap R A)) i✝ x✝
[PROOFSTEP]
simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum, _root_.mul_assoc,
  Algebra.left_comm]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ ∀ (r : R), ↑(toFunLinear R A n) (↑(algebraMap R A) r ⊗ₜ[R] 1) = ↑(algebraMap R (Matrix n n A)) r
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
r✝ : R
⊢ ↑(toFunLinear R A n) (↑(algebraMap R A) r✝ ⊗ₜ[R] 1) = ↑(algebraMap R (Matrix n n A)) r✝
[PROOFSTEP]
simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply, Matrix.map_one (algebraMap R A) (map_zero _) (map_one _),
  algebraMap_smul, Algebra.algebraMap_eq_smul_one]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : A
m : Matrix n n R
⊢ ↑(toFunAlgHom R A n) (a ⊗ₜ[R] m) = a • Matrix.map m ↑(algebraMap R A)
[PROOFSTEP]
simp [toFunAlgHom, algHomOfLinearMapTensorProduct, toFunLinear]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : A
m : Matrix n n R
⊢ AddHom.toFun (lift (toFunBilinear R A n)).toAddHom (a ⊗ₜ[R] m) = a • Matrix.map m ↑(algebraMap R A)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ invFun R A n 0 = 0
[PROOFSTEP]
simp [invFun]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M N : Matrix n n A
⊢ invFun R A n (M + N) = invFun R A n M + invFun R A n N
[PROOFSTEP]
simp [invFun, add_tmul, Finset.sum_add_distrib]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : A
M : Matrix n n A
⊢ invFun R A n (a • M) = a ⊗ₜ[R] 1 * invFun R A n M
[PROOFSTEP]
simp [invFun, Finset.mul_sum]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ invFun R A n (Matrix.map M ↑(algebraMap R A)) = 1 ⊗ₜ[R] M
[PROOFSTEP]
dsimp [invFun]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ p : n × n, ↑(algebraMap R A) (M p.fst p.snd) ⊗ₜ[R] stdBasisMatrix p.fst p.snd 1 = 1 ⊗ₜ[R] M
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, smul_tmul, ← tmul_sum, mul_boole]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 ⊗ₜ[R] ∑ a : n × n, M a.fst a.snd • stdBasisMatrix a.fst a.snd 1 = 1 ⊗ₜ[R] M
[PROOFSTEP]
congr
[GOAL]
case e_n
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ a : n × n, M a.fst a.snd • stdBasisMatrix a.fst a.snd 1 = M
[PROOFSTEP]
conv_rhs => rw [matrix_eq_sum_std_basis M]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
case e_n
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ a : n × n, M a.fst a.snd • stdBasisMatrix a.fst a.snd 1 = ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j)
[PROOFSTEP]
convert Finset.sum_product (β := Matrix n n R)
[GOAL]
case h.e'_3.a.a
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
x✝¹ : n
a✝¹ : x✝¹ ∈ Finset.univ
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ stdBasisMatrix x✝¹ x✝ (M x✝¹ x✝) = M (x✝¹, x✝).fst (x✝¹, x✝).snd • stdBasisMatrix (x✝¹, x✝).fst (x✝¹, x✝).snd 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ ↑(toFunAlgHom R A n) (invFun R A n M) = M
[PROOFSTEP]
simp only [invFun, AlgHom.map_sum, stdBasisMatrix, apply_ite ↑(algebraMap R A), smul_eq_mul, mul_boole,
  toFunAlgHom_apply, RingHom.map_zero, RingHom.map_one, Matrix.map_apply, Pi.smul_def]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ ∑ x : n × n, M x.fst x.snd • Matrix.map (fun i' j' => if x.fst = i' ∧ x.snd = j' then 1 else 0) ↑(algebraMap R A) = M
[PROOFSTEP]
convert Finset.sum_product (β := Matrix n n A)
[GOAL]
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ M =
    ∑ x : n,
      ∑ y : n,
        M (x, y).fst (x, y).snd •
          Matrix.map (fun i' j' => if (x, y).fst = i' ∧ (x, y).snd = j' then 1 else 0) ↑(algebraMap R A)
[PROOFSTEP]
conv_lhs => rw [matrix_eq_sum_std_basis M]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j) =
    ∑ x : n,
      ∑ y : n,
        M (x, y).fst (x, y).snd •
          Matrix.map (fun i' j' => if (x, y).fst = i' ∧ (x, y).snd = j' then 1 else 0) ↑(algebraMap R A)
[PROOFSTEP]
refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => Matrix.ext fun a b => ?_
[GOAL]
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
⊢ stdBasisMatrix i j (M i j) a b =
    (M (i, j).fst (i, j).snd •
        Matrix.map (fun i' j' => if (i, j).fst = i' ∧ (i, j).snd = j' then 1 else 0) ↑(algebraMap R A))
      a b
[PROOFSTEP]
simp only [stdBasisMatrix, smul_apply, Matrix.map_apply]
[GOAL]
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
⊢ (if i = a ∧ j = b then M i j else 0) = M i j • ↑(algebraMap R A) (if i = a ∧ j = b then 1 else 0)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
h✝ : i = a ∧ j = b
⊢ M i j = M i j • ↑(algebraMap R A) 1
[PROOFSTEP]
aesop
[GOAL]
case neg
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
h✝ : ¬(i = a ∧ j = b)
⊢ 0 = M i j • ↑(algebraMap R A) 0
[PROOFSTEP]
aesop
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : A ⊗[R] Matrix n n R
⊢ invFun R A n (↑(toFunAlgHom R A n) M) = M
[PROOFSTEP]
induction M using TensorProduct.induction_on with
| zero => simp
| tmul a m => simp
| add x y hx hy =>
  rw [map_add]
  conv_rhs => rw [← hx, ← hy, ← invFun_add]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : A ⊗[R] Matrix n n R
⊢ invFun R A n (↑(toFunAlgHom R A n) M) = M
[PROOFSTEP]
induction M using TensorProduct.induction_on with
| zero => simp
| tmul a m => simp
| add x y hx hy =>
  rw [map_add]
  conv_rhs => rw [← hx, ← hy, ← invFun_add]
[GOAL]
case zero
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ invFun R A n (↑(toFunAlgHom R A n) 0) = 0
[PROOFSTEP]

| zero => simp
[GOAL]
case zero
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ invFun R A n (↑(toFunAlgHom R A n) 0) = 0
[PROOFSTEP]
simp
[GOAL]
case tmul
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : A
m : Matrix n n R
⊢ invFun R A n (↑(toFunAlgHom R A n) (a ⊗ₜ[R] m)) = a ⊗ₜ[R] m
[PROOFSTEP]

| tmul a m => simp
[GOAL]
case tmul
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : A
m : Matrix n n R
⊢ invFun R A n (↑(toFunAlgHom R A n) (a ⊗ₜ[R] m)) = a ⊗ₜ[R] m
[PROOFSTEP]
simp
[GOAL]
case add
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
⊢ invFun R A n (↑(toFunAlgHom R A n) (x + y)) = x + y
[PROOFSTEP]

| add x y hx hy =>
  rw [map_add]
  conv_rhs => rw [← hx, ← hy, ← invFun_add]
[GOAL]
case add
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
⊢ invFun R A n (↑(toFunAlgHom R A n) (x + y)) = x + y
[PROOFSTEP]
rw [map_add]
[GOAL]
case add
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
⊢ invFun R A n (↑(toFunAlgHom R A n) x + ↑(toFunAlgHom R A n) y) = x + y
[PROOFSTEP]
conv_rhs => rw [← hx, ← hy, ← invFun_add]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
| x + y
[PROOFSTEP]
rw [← hx, ← hy, ← invFun_add]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
| x + y
[PROOFSTEP]
rw [← hx, ← hy, ← invFun_add]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
| x + y
[PROOFSTEP]
rw [← hx, ← hy, ← invFun_add]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
⊢ ↑(matrixEquivTensor R A n) (stdBasisMatrix i j x) = x ⊗ₜ[R] stdBasisMatrix i j 1
[PROOFSTEP]
have t : ∀ p : n × n, i = p.1 ∧ j = p.2 ↔ p = (i, j) := by aesop
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
⊢ ∀ (p : n × n), i = p.fst ∧ j = p.snd ↔ p = (i, j)
[PROOFSTEP]
aesop
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
t : ∀ (p : n × n), i = p.fst ∧ j = p.snd ↔ p = (i, j)
⊢ ↑(matrixEquivTensor R A n) (stdBasisMatrix i j x) = x ⊗ₜ[R] stdBasisMatrix i j 1
[PROOFSTEP]
simp [ite_tmul, t, stdBasisMatrix]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : A
M : Matrix n n R
⊢ ↑(AlgEquiv.symm (matrixEquivTensor R A n)) (a ⊗ₜ[R] M) = Matrix.map M fun x => a * ↑(algebraMap R A) x
[PROOFSTEP]
simp [matrixEquivTensor, MatrixEquivTensor.toFunAlgHom, algHomOfLinearMapTensorProduct, MatrixEquivTensor.toFunLinear]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : A
M : Matrix n n R
⊢ AddHom.toFun (lift (toFunBilinear R A n)).toAddHom (a ⊗ₜ[R] M) = Matrix.map M fun x => a * ↑(algebraMap R A) x
[PROOFSTEP]
rfl


[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
V : Set (σ → k)
p q : MvPolynomial σ k
hp : p ∈ {p | ∀ (x : σ → k), x ∈ V → ↑(eval x) p = 0}
hq : q ∈ {p | ∀ (x : σ → k), x ∈ V → ↑(eval x) p = 0}
x : σ → k
hx : x ∈ V
⊢ ↑(eval x) (p + q) = 0
[PROOFSTEP]
simp only [hq x hx, hp x hx, add_zero, RingHom.map_add]
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
V : Set (σ → k)
p q : MvPolynomial σ k
hq :
  q ∈
    {
          toAddSubsemigroup :=
            { carrier := {p | ∀ (x : σ → k), x ∈ V → ↑(eval x) p = 0},
              add_mem' :=
                (_ :
                  ∀ {p q : MvPolynomial σ k},
                    p ∈ {p | ∀ (x : σ → k), x ∈ V → ↑(eval x) p = 0} →
                      q ∈ {p | ∀ (x : σ → k), x ∈ V → ↑(eval x) p = 0} →
                        ∀ (x : σ → k), x ∈ V → ↑(eval x) (p + q) = 0) },
          zero_mem' := (_ : ∀ (x : σ → k), x ∈ V → ↑(eval x) 0 = 0) }.toAddSubsemigroup.carrier
x : σ → k
hx : x ∈ V
⊢ ↑(eval x) (p • q) = 0
[PROOFSTEP]
simp only [hq x hx, Algebra.id.smul_eq_mul, mul_zero, RingHom.map_mul]
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
x : σ → k
⊢ IsMaximal (vanishingIdeal {x})
[PROOFSTEP]
have : MvPolynomial σ k ⧸ vanishingIdeal { x } ≃+* k :=
  RingEquiv.ofBijective (Ideal.Quotient.lift _ (eval x) fun p h => (mem_vanishingIdeal_singleton_iff x p).mp h)
    (by
      refine'
        ⟨(injective_iff_map_eq_zero _).mpr fun p hp => _, fun z =>
          ⟨(Ideal.Quotient.mk (vanishingIdeal { x } : Ideal (MvPolynomial σ k))) (C z), by simp⟩⟩
      obtain ⟨q, rfl⟩ := Quotient.mk_surjective p
      rwa [Ideal.Quotient.lift_mk, ← mem_vanishingIdeal_singleton_iff, ← Quotient.eq_zero_iff_mem] at hp )
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
x : σ → k
⊢ Function.Bijective
    ↑(Ideal.Quotient.lift (vanishingIdeal {x}) (eval x)
        (_ : ∀ (p : MvPolynomial σ k), p ∈ vanishingIdeal {x} → ↑(eval x) p = 0))
[PROOFSTEP]
refine'
  ⟨(injective_iff_map_eq_zero _).mpr fun p hp => _, fun z =>
    ⟨(Ideal.Quotient.mk (vanishingIdeal { x } : Ideal (MvPolynomial σ k))) (C z), by simp⟩⟩
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
x : σ → k
z : k
⊢ ↑(Ideal.Quotient.lift (vanishingIdeal {x}) (eval x)
          (_ : ∀ (p : MvPolynomial σ k), p ∈ vanishingIdeal {x} → ↑(eval x) p = 0))
      (↑(Ideal.Quotient.mk (vanishingIdeal {x})) (↑C z)) =
    z
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
x : σ → k
p : MvPolynomial σ k ⧸ vanishingIdeal {x}
hp :
  ↑(Ideal.Quotient.lift (vanishingIdeal {x}) (eval x)
          (_ : ∀ (p : MvPolynomial σ k), p ∈ vanishingIdeal {x} → ↑(eval x) p = 0))
      p =
    0
⊢ p = 0
[PROOFSTEP]
obtain ⟨q, rfl⟩ := Quotient.mk_surjective p
[GOAL]
case intro
k : Type u_1
inst✝ : Field k
σ : Type u_2
x : σ → k
q : MvPolynomial σ k
hp :
  ↑(Ideal.Quotient.lift (vanishingIdeal {x}) (eval x)
          (_ : ∀ (p : MvPolynomial σ k), p ∈ vanishingIdeal {x} → ↑(eval x) p = 0))
      (↑(Ideal.Quotient.mk (vanishingIdeal {x})) q) =
    0
⊢ ↑(Ideal.Quotient.mk (vanishingIdeal {x})) q = 0
[PROOFSTEP]
rwa [Ideal.Quotient.lift_mk, ← mem_vanishingIdeal_singleton_iff, ← Quotient.eq_zero_iff_mem] at hp
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
x : σ → k
this : MvPolynomial σ k ⧸ vanishingIdeal {x} ≃+* k
⊢ IsMaximal (vanishingIdeal {x})
[PROOFSTEP]
rw [← bot_quotient_isMaximal_iff, RingEquiv.bot_maximal_iff this]
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
x : σ → k
this : MvPolynomial σ k ⧸ vanishingIdeal {x} ≃+* k
⊢ IsMaximal ⊥
[PROOFSTEP]
exact bot_isMaximal
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
I : Ideal (MvPolynomial σ k)
⊢ radical I ≤ vanishingIdeal (zeroLocus I)
[PROOFSTEP]
intro p hp x hx
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ radical I
x : σ → k
hx : x ∈ zeroLocus I
⊢ ↑(eval x) p = 0
[PROOFSTEP]
rw [← mem_vanishingIdeal_singleton_iff]
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ radical I
x : σ → k
hx : x ∈ zeroLocus I
⊢ p ∈ vanishingIdeal {x}
[PROOFSTEP]
rw [radical_eq_sInf] at hp
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ sInf {J | I ≤ J ∧ IsPrime J}
x : σ → k
hx : x ∈ zeroLocus I
⊢ p ∈ vanishingIdeal {x}
[PROOFSTEP]
refine'
  (mem_sInf.mp hp)
    ⟨le_trans (le_vanishingIdeal_zeroLocus I) (vanishingIdeal_anti_mono fun y hy => hy.symm ▸ hx), IsMaximal.isPrime' _⟩
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
x : σ → k
⊢ IsPrime (vanishingIdeal {x})
[PROOFSTEP]
infer_instance
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
V : Set (σ → k)
p : MvPolynomial σ k
hp : p ∈ PrimeSpectrum.vanishingIdeal (pointToPoint '' V)
x : σ → k
hx : x ∈ V
⊢ IsPrime (vanishingIdeal {x})
[PROOFSTEP]
infer_instance
[GOAL]
k : Type u_1
inst✝ : Field k
σ : Type u_2
V : Set (σ → k)
p : MvPolynomial σ k
hp : p ∈ PrimeSpectrum.vanishingIdeal (pointToPoint '' V)
x : σ → k
hx : x ∈ V
⊢ { asIdeal := vanishingIdeal {x}, IsPrime := (_ : IsPrime (vanishingIdeal {x})) } ∈ pointToPoint '' V
[PROOFSTEP]
exact ⟨x, ⟨hx, rfl⟩⟩
[GOAL]
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ IsMaximal I ↔ ∃ x, I = vanishingIdeal {x}
[PROOFSTEP]
cases nonempty_fintype σ
[GOAL]
case intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
⊢ IsMaximal I ↔ ∃ x, I = vanishingIdeal {x}
[PROOFSTEP]
refine'
  ⟨fun hI => _, fun h =>
    let ⟨x, hx⟩ := h
    hx.symm ▸ MvPolynomial.vanishingIdeal_singleton_isMaximal⟩
[GOAL]
case intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
⊢ ∃ x, I = vanishingIdeal {x}
[PROOFSTEP]
letI : I.IsMaximal := hI
[GOAL]
case intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this : IsMaximal I := hI
⊢ ∃ x, I = vanishingIdeal {x}
[PROOFSTEP]
letI : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
[GOAL]
case intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this✝ : IsMaximal I := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
⊢ ∃ x, I = vanishingIdeal {x}
[PROOFSTEP]
let ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C
[GOAL]
case intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this✝ : IsMaximal I := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := RingHom.comp (Ideal.Quotient.mk I) C
⊢ ∃ x, I = vanishingIdeal {x}
[PROOFSTEP]
have hϕ : Function.Bijective ϕ :=
  ⟨quotient_mk_comp_C_injective _ _ I hI.ne_top,
    IsAlgClosed.algebraMap_surjective_of_isIntegral' ϕ
      (MvPolynomial.comp_C_integral_of_surjective_of_jacobson _ Quotient.mk_surjective)⟩
[GOAL]
case intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this✝ : IsMaximal I := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := RingHom.comp (Ideal.Quotient.mk I) C
hϕ : Function.Bijective ↑ϕ
⊢ ∃ x, I = vanishingIdeal {x}
[PROOFSTEP]
obtain ⟨φ, hφ⟩ := Function.Surjective.hasRightInverse hϕ.2
[GOAL]
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this✝ : IsMaximal I := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := RingHom.comp (Ideal.Quotient.mk I) C
hϕ : Function.Bijective ↑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ↑ϕ
⊢ ∃ x, I = vanishingIdeal {x}
[PROOFSTEP]
let x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))
[GOAL]
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this✝ : IsMaximal I := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := RingHom.comp (Ideal.Quotient.mk I) C
hϕ : Function.Bijective ↑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ↑ϕ
x : σ → k := fun s => φ (↑(Ideal.Quotient.mk I) (X s))
⊢ ∃ x, I = vanishingIdeal {x}
[PROOFSTEP]
have hx : ∀ s : σ, ϕ (x s) = (Ideal.Quotient.mk I) (X s) := fun s => hφ ((Ideal.Quotient.mk I) (X s))
[GOAL]
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this✝ : IsMaximal I := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := RingHom.comp (Ideal.Quotient.mk I) C
hϕ : Function.Bijective ↑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ↑ϕ
x : σ → k := fun s => φ (↑(Ideal.Quotient.mk I) (X s))
hx : ∀ (s : σ), ↑ϕ (x s) = ↑(Ideal.Quotient.mk I) (X s)
⊢ ∃ x, I = vanishingIdeal {x}
[PROOFSTEP]
refine' ⟨x, (IsMaximal.eq_of_le (by infer_instance) hI.ne_top _).symm⟩
[GOAL]
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this✝ : IsMaximal I := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := RingHom.comp (Ideal.Quotient.mk I) C
hϕ : Function.Bijective ↑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ↑ϕ
x : σ → k := fun s => φ (↑(Ideal.Quotient.mk I) (X s))
hx : ∀ (s : σ), ↑ϕ (x s) = ↑(Ideal.Quotient.mk I) (X s)
⊢ IsMaximal (vanishingIdeal {x})
[PROOFSTEP]
infer_instance
[GOAL]
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this✝ : IsMaximal I := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := RingHom.comp (Ideal.Quotient.mk I) C
hϕ : Function.Bijective ↑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ↑ϕ
x : σ → k := fun s => φ (↑(Ideal.Quotient.mk I) (X s))
hx : ∀ (s : σ), ↑ϕ (x s) = ↑(Ideal.Quotient.mk I) (X s)
⊢ vanishingIdeal {x} ≤ I
[PROOFSTEP]
intro p hp
[GOAL]
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this✝ : IsMaximal I := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := RingHom.comp (Ideal.Quotient.mk I) C
hϕ : Function.Bijective ↑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ↑ϕ
x : σ → k := fun s => φ (↑(Ideal.Quotient.mk I) (X s))
hx : ∀ (s : σ), ↑ϕ (x s) = ↑(Ideal.Quotient.mk I) (X s)
p : MvPolynomial σ k
hp : p ∈ vanishingIdeal {x}
⊢ p ∈ I
[PROOFSTEP]
rw [← Quotient.eq_zero_iff_mem, map_mvPolynomial_eq_eval₂ (Ideal.Quotient.mk I) p, eval₂_eq']
[GOAL]
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this✝ : IsMaximal I := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := RingHom.comp (Ideal.Quotient.mk I) C
hϕ : Function.Bijective ↑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ↑ϕ
x : σ → k := fun s => φ (↑(Ideal.Quotient.mk I) (X s))
hx : ∀ (s : σ), ↑ϕ (x s) = ↑(Ideal.Quotient.mk I) (X s)
p : MvPolynomial σ k
hp : p ∈ vanishingIdeal {x}
⊢ (Finset.sum (support p) fun d =>
      ↑(RingHom.comp (Ideal.Quotient.mk I) C) (coeff d p) *
        Finset.prod Finset.univ fun i => ↑(Ideal.Quotient.mk I) (X i) ^ ↑d i) =
    0
[PROOFSTEP]
rw [mem_vanishingIdeal_singleton_iff, eval_eq'] at hp
[GOAL]
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : IsMaximal I
this✝ : IsMaximal I := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := RingHom.comp (Ideal.Quotient.mk I) C
hϕ : Function.Bijective ↑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ↑ϕ
x : σ → k := fun s => φ (↑(Ideal.Quotient.mk I) (X s))
hx : ∀ (s : σ), ↑ϕ (x s) = ↑(Ideal.Quotient.mk I) (X s)
p : MvPolynomial σ k
hp✝ : ↑(eval x) p = 0
hp : (Finset.sum (support p) fun d => coeff d p * Finset.prod Finset.univ fun i => x i ^ ↑d i) = 0
⊢ (Finset.sum (support p) fun d =>
      ↑(RingHom.comp (Ideal.Quotient.mk I) C) (coeff d p) *
        Finset.prod Finset.univ fun i => ↑(Ideal.Quotient.mk I) (X i) ^ ↑d i) =
    0
[PROOFSTEP]
simpa only [ϕ.map_sum, ϕ.map_mul, ϕ.map_prod, ϕ.map_pow, ϕ.map_zero, hx] using congr_arg ϕ hp
[GOAL]
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ vanishingIdeal (zeroLocus I) = radical I
[PROOFSTEP]
rw [I.radical_eq_jacobson]
[GOAL]
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ vanishingIdeal (zeroLocus I) = jacobson I
[PROOFSTEP]
refine' le_antisymm (le_sInf _) fun p hp x hx => _
[GOAL]
case refine'_1
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ ∀ (b : Ideal (MvPolynomial σ k)), b ∈ {J | I ≤ J ∧ IsMaximal J} → vanishingIdeal (zeroLocus I) ≤ b
[PROOFSTEP]
rintro J ⟨hJI, hJ⟩
[GOAL]
case refine'_1.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : IsMaximal J
⊢ vanishingIdeal (zeroLocus I) ≤ J
[PROOFSTEP]
obtain ⟨x, hx⟩ := (isMaximal_iff_eq_vanishingIdeal_singleton J).1 hJ
[GOAL]
case refine'_1.intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : IsMaximal J
x : σ → k
hx : J = vanishingIdeal {x}
⊢ vanishingIdeal (zeroLocus I) ≤ J
[PROOFSTEP]
refine' hx.symm ▸ vanishingIdeal_anti_mono fun y hy p hp => _
[GOAL]
case refine'_1.intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : IsMaximal J
x : σ → k
hx : J = vanishingIdeal {x}
y : σ → k
hy : y ∈ {x}
p : MvPolynomial σ k
hp : p ∈ I
⊢ ↑(eval y) p = 0
[PROOFSTEP]
rw [← mem_vanishingIdeal_singleton_iff, Set.mem_singleton_iff.1 hy, ← hx]
[GOAL]
case refine'_1.intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : IsMaximal J
x : σ → k
hx : J = vanishingIdeal {x}
y : σ → k
hy : y ∈ {x}
p : MvPolynomial σ k
hp : p ∈ I
⊢ p ∈ J
[PROOFSTEP]
refine' hJI hp
[GOAL]
case refine'_2
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ jacobson I
x : σ → k
hx : x ∈ zeroLocus I
⊢ ↑(eval x) p = 0
[PROOFSTEP]
rw [← mem_vanishingIdeal_singleton_iff x p]
[GOAL]
case refine'_2
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ jacobson I
x : σ → k
hx : x ∈ zeroLocus I
⊢ p ∈ vanishingIdeal {x}
[PROOFSTEP]
refine'
  (mem_sInf.mp hp)
    ⟨le_trans (le_vanishingIdeal_zeroLocus I) (vanishingIdeal_anti_mono fun y hy => hy.symm ▸ hx),
      MvPolynomial.vanishingIdeal_singleton_isMaximal⟩