-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
private lemma jacobson_matricesOver_le (I : TwoSidedIdeal R) :
    (I.matricesOver n).jacobson ≤ I.jacobson.matricesOver n

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

Tactic:
replace Mmem := mul_mem_right _ _ (stdBasisMatrix q p 1) Mmem

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

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

Tactic:
rw [mem_jacobson_iff] at Mmem

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

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
y : R
Mmem : ∃ z, z * y • stdBasisMatrix p p 1 * (M * stdBasisMatrix q p 1) + z - 1 ∈ matricesOver n I
N : Matrix n n R
NxMI : N * y • stdBasisMatrix p p 1 * (M * stdBasisMatrix q p 1) + N - 1 ∈ matricesOver n I
⊢ ∃ z, z * y * M p q + z - 1 ∈ I

Tactic:
use N p p

Result:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
y : R
Mmem : ∃ z, z * y • stdBasisMatrix p p 1 * (M * stdBasisMatrix q p 1) + z - 1 ∈ matricesOver n I
N : Matrix n n R
NxMI : N * y • stdBasisMatrix p p 1 * (M * stdBasisMatrix q p 1) + N - 1 ∈ matricesOver n I
⊢ N p p * y * M p q + N p p - 1 ∈ I

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

Tactic:
intro M Mmem p q

Result:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
Mmem : M ∈ (matricesOver n I).jacobson
p q : n
⊢ (M - 0) p q ∈ I.jacobson

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

Tactic:
have ⟨N, NxMI⟩ := Mmem

Result:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
y : R
Mmem : ∃ z, z * y • stdBasisMatrix p p 1 * (M * stdBasisMatrix q p 1) + z - 1 ∈ matricesOver n I
N : Matrix n n R
NxMI : N * y • stdBasisMatrix p p 1 * (M * stdBasisMatrix q p 1) + N - 1 ∈ matricesOver n I
⊢ ∃ z, z * y * M p q + z - 1 ∈ I

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
Mmem : M ∈ (matricesOver n I).jacobson
p q : n
⊢ (M - 0) p q ∈ I.jacobson

Tactic:
rw [sub_zero, mem_jacobson_iff]

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

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

Tactic:
intro y

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

Proof state:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
y : R
Mmem : ∃ z, z * y • stdBasisMatrix p p 1 * (M * stdBasisMatrix q p 1) + z - 1 ∈ matricesOver n I
N : Matrix n n R
NxMI : N * y • stdBasisMatrix p p 1 * (M * stdBasisMatrix q p 1) + N - 1 ∈ matricesOver n I
⊢ N p p * y * M p q + N p p - 1 ∈ I

Tactic:
simpa [mul_apply, stdBasisMatrix, ite_and] using NxMI p p

Result:
no goals

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

Tactic:
specialize Mmem (y • stdBasisMatrix p p 1)

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