-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem stdBasisMatrix_mem_jacobson_matricesOver (I : Ideal R) :
    ∀ x ∈ I.jacobson, ∀ (i j : n), stdBasisMatrix i j x ∈ (I.matricesOver n).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
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i j : n
⊢ (N * M * stdBasisMatrix p q x + N - 1) i j ∈ I

Tactic:
obtain rfl | qj := eq_or_ne q j

Result:
case h.inl
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i : n
⊢ (N * M * stdBasisMatrix p q x + N - 1) i q ∈ I

case h.inr
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i j : n
qj : q ≠ j
⊢ (N * M * stdBasisMatrix p q x + N - 1) i j ∈ I

Proof state:
case h.inr
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i j : n
qj : q ≠ j
⊢ (N * M * stdBasisMatrix p q x + N - 1) i j ∈ I

Tactic:
simp [N, qj, sum_apply, mul_apply]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : i = q
⊢ (N * M * stdBasisMatrix p q x + N - 1) i q ∈ I

Tactic:
simp [iq, N, zMx, stdBasisMatrix, mul_apply, sum_apply, ite_and, sub_mul]

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
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
⊢ N * M * stdBasisMatrix p q x + N - 1 ∈ matricesOver n I

Tactic:
intro i j

Result:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i j : n
⊢ (N * M * stdBasisMatrix p q x + N - 1) i j ∈ I

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
⊢ ∃ z, z * M * stdBasisMatrix p q x + z - 1 ∈ matricesOver n I

Tactic:
use N

Result:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
⊢ N * M * stdBasisMatrix p q x + N - 1 ∈ matricesOver n I

Proof state:
case h.e'_5
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : ¬i = q
⊢ (N * M * stdBasisMatrix p q x + N - 1) i q = -M i p * x * (z * M q p * x + z - 1)

Tactic:
simp [iq, N, zMx, stdBasisMatrix, mul_apply, sum_apply, ite_and, sub_mul]

Result:
case h.e'_5
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : ¬i = q
⊢ M i p * x - M i p * x * z * M q p * x + -(M i p * x * z) = -(M i p * x * (z * M q p * x + z - 1))

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
⊢ ∀ (x : R),
    (∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I) →
      ∀ (i j : n) (y : Matrix n n R), ∃ z, z * y * stdBasisMatrix i j x + z - 1 ∈ matricesOver n I

Tactic:
intro x xIJ p q M

Result:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
⊢ ∃ z, z * M * stdBasisMatrix p q x + z - 1 ∈ matricesOver n I

Proof state:
case neg
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : ¬i = q
⊢ (N * M * stdBasisMatrix p q x + N - 1) i q ∈ I

Tactic:
convert I.mul_mem_left (-M i p * x) zMx

Result:
case h.e'_5
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : ¬i = q
⊢ (N * M * stdBasisMatrix p q x + N - 1) i q = -M i p * x * (z * M q p * x + z - 1)

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
⊢ ∃ z, z * M * stdBasisMatrix p q x + z - 1 ∈ matricesOver n I

Tactic:
have ⟨z, zMx⟩ := xIJ (M q p)

Result:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
⊢ ∃ z, z * M * stdBasisMatrix p q x + z - 1 ∈ matricesOver n I

Proof state:
case h.e'_5
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i : n, stdBasisMatrix i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : ¬i = q
⊢ M i p * x - M i p * x * z * M q p * x + -(M i p * x * z) = -(M i p * x * (z * M q p * x + z - 1))

Tactic:
simp [sub_add, mul_add, mul_sub, mul_assoc]

Result:
no goals