mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * e' * e₂ = 0

pp: case refine_4
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ e₂ * ((1 - e₂) * e') = 0

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * e' * e₂ = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ e₂ * ((1 - e₂) * e') = 0

Tactic:
·

Goal state after:
case refine_4
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ e₂ * ((1 - e₂) * e') = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝ : Subsingleton R
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

pp: case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝ : Nontrivial R
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
·

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝ : Subsingleton R
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.inl
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝¹ : Nontrivial R
h✝ : Subsingleton S
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

pp: case inr.inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝¹ : Nontrivial R
h✝ : Nontrivial S
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝¹ : Nontrivial R
h✝ : Subsingleton S
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.inr.zero
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
h✝¹ : Nontrivial R
h✝ : Nontrivial S
e : Fin 0 → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin 0), e i ∈ f.range
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

pp: case inr.inr.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
h✝¹ : Nontrivial R
h✝ : Nontrivial S
n : ℕ
e : Fin (n + 1) → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
·

Goal state after:
case inr.inr.zero
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
h✝¹ : Nontrivial R
h✝ : Nontrivial S
e : Fin 0 → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin 0), e i ∈ f.range
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ = e₂

Tactic:
by
  have : (e₁ - e₂) ^ 3 = (e₁ - e₂) := by
    simp only [pow_succ, pow_zero, mul_sub, one_mul, sub_mul, he₁.eq, he₂.eq,
      H'.eq, mul_assoc]
    simp only [← mul_assoc, he₂.eq]
    abel
  obtain ⟨n, hn⟩ := H
  have : (e₁ - e₂) ^ (2 * n + 1) = (e₁ - e₂) := by
    clear hn; induction n <;> simp [mul_add, add_assoc, pow_add _ (2 * _) 3, ← pow_succ, *]
  rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) → M = 0

pp: case mpr
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ M = 0 → ∀ (i j : n), M i j = 0

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) → M = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ M = 0 → ∀ (i j : n), M i j = 0

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ M = 0 → ∀ (i j : n), M i j = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: 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, single i q (if i = q then 1 - z else M i p * x * z)
i : n
⊢ (N * M * single p q x + N - 1) i q ∈ ↑I.toAddSubmonoid

pp: 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, single i q (if i = q then 1 - z else M i p * x * z)
i j : n
qj : q ≠ j
⊢ (N * M * single p q x + N - 1) i j ∈ ↑I.toAddSubmonoid

Tactic:
·

Goal state after:
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, single i q (if i = q then 1 - z else M i p * x * z)
i : n
⊢ (N * M * single p q x + N - 1) i q ∈ ↑I.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: 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, single i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : i = q
⊢ (N * M * single p q x + N - 1) i q ∈ ↑I.toAddSubmonoid

pp: 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, single i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : ¬i = q
⊢ (N * M * single p q x + N - 1) i q ∈ ↑I.toAddSubmonoid

Tactic:
·

Goal state after:
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, single i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : i = q
⊢ (N * M * single p q x + N - 1) i q ∈ ↑I.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ l, ↑l ≤ ↑k ∧ x ∈ ((f - μ • 1) ^ l).ker) → x ∈ ((f - μ • 1) ^ k).ker

pp: case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ x ∈ ((f - μ • 1) ^ k).ker → ∃ l, ↑l ≤ ↑k ∧ x ∈ ((f - μ • 1) ^ l).ker

Tactic:
·

Goal state after:
case mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ l, ↑l ≤ ↑k ∧ x ∈ ((f - μ • 1) ^ l).ker) → x ∈ ((f - μ • 1) ^ k).ker
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: 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, single i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : ¬i = q
⊢ (N * M * single p q x + N - 1) i q ∈ ↑I.toAddSubmonoid

Tactic:
·

Goal state after:
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, single i q (if i = q then 1 - z else M i p * x * z)
i : n
iq : ¬i = q
⊢ (N * M * single p q x + N - 1) i q ∈ ↑I.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ x ∈ ((f - μ • 1) ^ k).ker → ∃ l, ↑l ≤ ↑k ∧ x ∈ ((f - μ • 1) ^ l).ker

Tactic:
·

Goal state after:
case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ x ∈ ((f - μ • 1) ^ k).ker → ∃ l, ↑l ≤ ↑k ∧ x ∈ ((f - μ • 1) ^ l).ker
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: 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, single i q (if i = q then 1 - z else M i p * x * z)
i j : n
qj : q ≠ j
⊢ (N * M * single p q x + N - 1) i j ∈ ↑I.toAddSubmonoid

Tactic:
·

Goal state after:
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, single i q (if i = q then 1 - z else M i p * x * z)
i j : n
qj : q ≠ j
⊢ (N * M * single p q x + N - 1) i j ∈ ↑I.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case inl
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
i' j' : n
hi : i ≠ i'
⊢ c (Matrix.single i j x i' j') (Matrix.single i j y i' j')

pp: case inr
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
j' : n
⊢ c (Matrix.single i j x i j') (Matrix.single i j y i j')

Tactic:
·

Goal state after:
case inl
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
i' j' : n
hi : i ≠ i'
⊢ c (Matrix.single i j x i' j') (Matrix.single i j y i' j')
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case inr.inl
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
j' : n
hj : j ≠ j'
⊢ c (Matrix.single i j x i j') (Matrix.single i j y i j')

pp: case inr.inr
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
⊢ c (Matrix.single i j x i j) (Matrix.single i j y i j)

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
j' : n
hj : j ≠ j'
⊢ c (Matrix.single i j x i j') (Matrix.single i j y i j')
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
⊢ (matrix n c).ofMatrix x y → c x y

pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
⊢ c x y → (matrix n c).ofMatrix x y

Tactic:
·

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
⊢ (matrix n c).ofMatrix x y → c x y
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
⊢ c x y → (matrix n c).ofMatrix x y

Tactic:
·

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
⊢ c x y → (matrix n c).ofMatrix x y
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
⊢ (matrix n c.ofMatrix) x y → c x y

pp: case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
⊢ c x y → (matrix n c.ofMatrix) x y

Tactic:
·

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
⊢ (matrix n c.ofMatrix) x y → c x y
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
⊢ c x y → (matrix n c.ofMatrix) x y

Tactic:
·

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
⊢ c x y → (matrix n c.ofMatrix) x y
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
⊢ c.ofMatrix x y → Relation.Map (⇑c) (fun x ↦ x i j) (fun x ↦ x i j) x y

pp: case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
⊢ Relation.Map (⇑c) (fun x ↦ x i j) (fun x ↦ x i j) x y → c.ofMatrix x y

Tactic:
·

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
⊢ c.ofMatrix x y → Relation.Map (⇑c) (fun x ↦ x i j) (fun x ↦ x i j) x y
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case he
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∀ (i : Fin 2), IsIdempotentElem (o i)

pp: case he₁
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∀ (i j : Fin 2), i ≠ j → (1 - o i) * (1 - o j) = 0

pp: case he₂
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∏ i, o i = 0

Tactic:
·

Goal state after:
case he
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∀ (i : Fin 2), IsIdempotentElem (o i)
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
⊢ Relation.Map (⇑c) (fun x ↦ x i j) (fun x ↦ x i j) x y → c.ofMatrix x y

Tactic:
·

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
⊢ Relation.Map (⇑c) (fun x ↦ x i j) (fun x ↦ x i j) x y → c.ofMatrix x y
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case he₁
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∀ (i j : Fin 2), i ≠ j → (1 - o i) * (1 - o j) = 0

pp: case he₂
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∏ i, o i = 0

Tactic:
·

Goal state after:
case he₁
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∀ (i j : Fin 2), i ≠ j → (1 - o i) * (1 - o j) = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x) → ∃ y, ((f - μ • 1) ^ k) y = x

pp: case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ y, ((f - μ • 1) ^ k) y = x) → ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x

Tactic:
·

Goal state after:
case mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x) → ∃ y, ((f - μ • 1) ^ k) y = x
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ ↑(equivMatrix.symm I) → r ∈ {x | ∃ N ∈ I, N i j = x}

pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ {x | ∃ N ∈ I, N i j = x} → r ∈ ↑(equivMatrix.symm I)

Tactic:
·

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ ↑(equivMatrix.symm I) → r ∈ {x | ∃ N ∈ I, N i j = x}
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ y, ((f - μ • 1) ^ k) y = x) → ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x

Tactic:
·

Goal state after:
case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ y, ((f - μ • 1) ^ k) y = x) → ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ {x | ∃ N ∈ I, N i j = x} → r ∈ ↑(equivMatrix.symm I)

Tactic:
·

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ {x | ∃ N ∈ I, N i j = x} → r ∈ ↑(equivMatrix.symm I)
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ matrix n I ≤ matrix n J → I ≤ J

pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ I ≤ J → matrix n I ≤ matrix n J

Tactic:
·

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ matrix n I ≤ matrix n J → I ≤ J
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ I ≤ J → matrix n I ≤ matrix n J

Tactic:
·

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ I ≤ J → matrix n I ≤ matrix n J
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case he₂
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∏ i, o i = 0

Tactic:
·

Goal state after:
case he₂
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∏ i, o i = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ (matrix n I).jacobson ≤ matrix n I.jacobson

pp: case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ matrix n I.jacobson ≤ (matrix n I).jacobson

Tactic:
·

Goal state after:
case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ (matrix n I).jacobson ≤ matrix n I.jacobson
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ matrix n I.jacobson ≤ (matrix n I).jacobson

Tactic:
·

Goal state after:
case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ matrix n I.jacobson ≤ (matrix n I).jacobson