-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem matricesOver_jacobson_le (I : Ideal R) :
    I.jacobson.matricesOver n ≤ (I.matricesOver n).jacobson

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
⊢ matricesOver n I.jacobson ≤ (matricesOver n I).jacobson

Tactic:
intro M MI

Result:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
⊢ M ∈ (matricesOver n I).jacobson

Proof state:
case h.h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
i : n
a✝ : i ∈ Finset.univ
⊢ ∀ c ∈ Finset.univ, stdBasisMatrix i c (M i c) ∈ (matricesOver n I).jacobson

Tactic:
intro j _

Result:
case h.h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
i : n
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ stdBasisMatrix i j (M i j) ∈ (matricesOver n I).jacobson

Proof state:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
⊢ ∀ c ∈ Finset.univ, ∑ j : n, stdBasisMatrix c j (M c j) ∈ (matricesOver n I).jacobson

Tactic:
intro i _

Result:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
i : n
a✝ : i ∈ Finset.univ
⊢ ∑ j : n, stdBasisMatrix i j (M i j) ∈ (matricesOver n I).jacobson

Proof state:
case h.h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
i : n
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ stdBasisMatrix i j (M i j) ∈ (matricesOver n I).jacobson

Tactic:
apply stdBasisMatrix_mem_jacobson_matricesOver I _ (MI i j)

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
i : n
a✝ : i ∈ Finset.univ
⊢ ∑ j : n, stdBasisMatrix i j (M i j) ∈ (matricesOver n I).jacobson

Tactic:
apply sum_mem

Result:
case h.h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
i : n
a✝ : i ∈ Finset.univ
⊢ ∀ c ∈ Finset.univ, stdBasisMatrix i c (M i c) ∈ (matricesOver n I).jacobson

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
⊢ ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j) ∈ (matricesOver n I).jacobson

Tactic:
apply sum_mem

Result:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
⊢ ∀ c ∈ Finset.univ, ∑ j : n, stdBasisMatrix c j (M c j) ∈ (matricesOver n I).jacobson

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
⊢ M ∈ (matricesOver n I).jacobson

Tactic:
rw [matrix_eq_sum_stdBasisMatrix M]

Result:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matricesOver n I.jacobson
⊢ ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j) ∈ (matricesOver n I).jacobson