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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm
x : I
⊢ (⇑f ∘ e' ∘ ⇑(Fintype.equivFin I)) x = e x

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm
x : I
⊢ f (e' ((Fintype.equivFin I) x)) = e x
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this : Nonempty { l // ↑l ≤ k }
m n : { i // ↑i ≤ k }
h : m ≤ n
⊢ ((f - μ • 1) ^ ↑m).ker ≤ ((f - μ • 1) ^ ↑n).ker

Tactic:
simpa using

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this : Nonempty { l // ↑l ≤ k }
m n : { i // ↑i ≤ k }
h : m ≤ n
⊢ ((f - μ • 1) ^ ↑m).ker ≤ ((f - μ • 1) ^ ↑n).ker
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
I J : Ideal R
eq : matrix n I = matrix n J
x : R
this : (∀ (x_1 x_2 : n), x ∈ I) ↔ ∀ (x_1 x_2 : n), x ∈ J
⊢ x ∈ I ↔ x ∈ J

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : Semiring R
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
I J : Ideal R
eq : matrix n I = matrix n J
x : R
this : (∀ (x_1 x_2 : n), x ∈ I) ↔ ∀ (x_1 x_2 : n), x ∈ J
⊢ x ∈ I ↔ x ∈ J
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents (⇑f ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = ⇑f ∘ e
i : I
⊢ e i - e' i ∈ RingHom.ker f

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents (⇑f ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = ⇑f ∘ e
i : I
⊢ f (e i) = f (e' i)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x y : { l // ↑l ≤ k }
h : x ≤ y
⊢ (fun x ↦ ↑↑x) x ≤ (fun x ↦ ↑↑x) y

Tactic:
simpa using

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x y : { l // ↑l ≤ k }
h : x ≤ y
⊢ x ≤ y
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: 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 : (matrix n c) (Matrix.single i j x) (Matrix.single i j y)
⊢ c x y

Tactic:
simpa using

Goal state after:
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 : (matrix n c) (Matrix.single i j x) (Matrix.single i j y)
⊢ c x y
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')

Tactic:
simpa using

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 0 0
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')

Tactic:
simpa using

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 0 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
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:
simpa using

Goal state after:
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 x y
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : Nonempty n
I J : RingCon R
eq : matrix n I = matrix n J
r s : R
this :
  (matrix n I) (Matrix.of fun x x_1 ↦ r) (Matrix.of fun x x_1 ↦ s) =
    (matrix n J) (Matrix.of fun x x_1 ↦ r) (Matrix.of fun x x_1 ↦ s)
⊢ I r s ↔ J r s

Tactic:
simpa using

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : Nonempty n
I J : RingCon R
eq : matrix n I = matrix n J
r s : R
this :
  (matrix n I) (Matrix.of fun x x_1 ↦ r) (Matrix.of fun x x_1 ↦ s) =
    (matrix n J) (Matrix.of fun x x_1 ↦ r) (Matrix.of fun x x_1 ↦ s)
⊢ I r s ↔ J r s
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
w✝ x✝ y✝ z✝ : R
h₁ : ∀ (i j : n), c (single i j w✝) (single i j x✝)
h₂ : ∀ (i j : n), c (single i j y✝) (single i j z✝)
i j : n
⊢ c (single i j (w✝ * y✝)) (single i j (x✝ * z✝))

Tactic:
simpa using

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
w✝ x✝ y✝ z✝ : R
h₁ : ∀ (i j : n), c (single i j w✝) (single i j x✝)
h₂ : ∀ (i j : n), c (single i j y✝) (single i j z✝)
i j : n
⊢ c (single i j (w✝ * y✝)) (single i j (x✝ * z✝))
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
w✝ x✝² y✝ z✝ : R
h₁ : ∀ (i j : n), c (single i j w✝) (single i j x✝²)
h₂ : ∀ (i j : n), c (single i j y✝) (single i j z✝)
x✝¹ x✝ : n
⊢ c (single x✝¹ x✝ (w✝ + y✝)) (single x✝¹ x✝ (x✝² + z✝))

Tactic:
simpa using

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
w✝ x✝² y✝ z✝ : R
h₁ : ∀ (i j : n), c (single i j w✝) (single i j x✝²)
h₂ : ∀ (i j : n), c (single i j y✝) (single i j z✝)
x✝¹ x✝ : n
⊢ c (single x✝¹ x✝ w✝ + single x✝¹ x✝ y✝) (single x✝¹ x✝ x✝² + single x✝¹ x✝ z✝)
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
h : (matrix n c).ofMatrix x y
inhabited_h : Inhabited n
⊢ c x y

Tactic:
simpa using

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
h : (matrix n c).ofMatrix x y
inhabited_h : Inhabited n
⊢ c x y
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ m ∈ ((f ^ n).genEigenspace (μ ^ n)) 1

Tactic:
simpa using

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ (f ^ n) m = μ ^ n • m
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ : R
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
n : ℕ
hn : f ^ n = 0
⊢ μ ^ n = 0

Tactic:
simpa using

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ : R
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
n : ℕ
hn : f ^ n = 0
⊢ μ = 0 ∧ ¬n = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
⊢ μ ∈ spectrum R f

Tactic:
refine spectrum.mem_iff.mpr fun h_unit ↦ ?_

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
⊢ False
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
h : c x y
i' j' i j : n
⊢ c (single i j (x i' j')) (single i j (y i' j'))

Tactic:
simpa using

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
h : c x y
i' j' i j : n
⊢ c (single i j (x i' j')) (single i j (y i' j'))
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : ∀ (i : I), IsIdempotentElem (e i)
he₁ : ∀ (i j : I), i ≠ j → (1 - e i) * (1 - e j) = 0
he₂ : ∏ i, e i = 0
⊢ ∏ i, (1 - (1 - e i)) = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : ∀ (i : I), IsIdempotentElem (e i)
he₁ : ∀ (i j : I), i ≠ j → (1 - e i) * (1 - e j) = 0
he₂ : ∏ i, e i = 0
⊢ ∏ x, e x = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: 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 : R
i j : n
h : c (single i j x) (single i j y)
i' j' : n
⊢ c (single i' j' x) (single i' j' y)

Tactic:
simpa using

Goal state after:
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 : R
i j : n
h : c (single i j x) (single i j y)
i' j' : n
⊢ c (single i' j' x) (single i' j' 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)
i j : n
X Y : Matrix n n R
h : c X Y
i' j' : n
⊢ c (single i' j' ((fun x ↦ x i j) X)) (single i' j' ((fun x ↦ x i j) Y))

Tactic:
simpa using

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 : Matrix n n R
h : c X Y
i' j' : n
⊢ c (single i' j' (X i j)) (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✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
x : R
le : (of fun x_1 x_2 ↦ x) ∈ matrix n J
xI : x ∈ I
⊢ x ∈ J

Tactic:
simpa using

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
x : R
le : (of fun x_1 x_2 ↦ x) ∈ matrix n J
xI : x ∈ I
⊢ x ∈ J
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

Tactic:
intro le x xI
      specialize @le (of fun _ _ => x) (by simp [xI])
      simpa using le

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
k : ℕ
hk : f.maxUnifEigenspaceIndex μ ≤ k
⊢ ↑(f.maxUnifEigenspaceIndex μ) ≤ ↑k

Tactic:
simpa using

Goal state after:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
k : ℕ
hk : f.maxUnifEigenspaceIndex μ ≤ k
⊢ f.maxUnifEigenspaceIndex μ ≤ k
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ ↑(f.maxUnifEigenspaceIndex μ) ≤ ↑(finrank K V)

Tactic:
simpa using

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ f.maxUnifEigenspaceIndex μ ≤ finrank K V
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ
hk : finrank K V ≤ k
⊢ ↑(finrank K V) ≤ ↑k

Tactic:
simpa using

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ
hk : finrank K V ≤ k
⊢ finrank K V ≤ k
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
i j : I
h : some i ≠ some j
⊢ ?m.254 ≠ ?m.255

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
i j : I
h : some i ≠ some j
⊢ ¬?m.254 = ?m.255
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
hi : σ ↑i ∉ s
⊢ f ↑((b i) k) = 0

Tactic:
simpa using

Goal state after:
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
hi : σ ↑i ∉ s
⊢ f ↑((b i) k) = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
h : Commute ((f - μ • 1) ^ l) g
⊢ (g * (f - μ • 1) ^ l) x = 0

Tactic:
Module.End.mul_eq_comp,

Goal state after:
case right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
h : Commute ((f - μ • 1) ^ l) g
⊢ (g ∘ₗ (f - μ • 1) ^ l) x = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
⊢ f (∑ i, e' i - 1) = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
⊢ ∑ x, e x = 1
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
⊢ f e₀ = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
⊢ f e₀ = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
n : ℕ∞
k : ℕ
ih : ∀ ⦃x : M⦄, ↑k ≤ n → ((f - μ • 1) ^ k) x = 0 → ((f - μ • 1) ^ k) (f x) = 0
x : M
hk : ↑(k + 1) ≤ n
hx : ((f - μ • 1) ^ k) ((f - μ • 1) x) = 0
⊢ ((f - μ • 1) ^ k) ((f - μ • 1) (f x)) = 0

Tactic:
simpa using

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
n : ℕ∞
k : ℕ
ih : ∀ ⦃x : M⦄, ↑k ≤ n → ((f - μ • 1) ^ k) x = 0 → ((f - μ • 1) ^ k) (f x) = 0
x : M
hk : ↑(k + 1) ≤ n
hx : ((f - μ • 1) ^ k) ((f - μ • 1) x) = 0
⊢ ((f - μ • 1) ^ k) (f (f x)) - μ • ((f - μ • 1) ^ k) (f x) = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ
hm : k ≤ m
hk : f.HasGenEigenvalue μ k
⊢ ↑k ≤ ↑m

Tactic:
simpa using

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ
hm : k ≤ m
hk : f.HasGenEigenvalue μ k
⊢ k ≤ m
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
hk : 0 < k
⊢ 1 ≤ ↑k

Tactic:
simpa using

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
hk : 0 < k
⊢ 1 ≤ k
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
hk : 0 < k
hμ : f.HasEigenvalue μ
⊢ 0 < ↑k

Tactic:
simpa using

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
hk : 0 < k
hμ : f.HasEigenvalue μ
⊢ 0 < k
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : End R M
hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i
⊢ Submodule.map f (⨆ i ∈ s, N i) ≤ ⨆ i ∈ s, N i

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : End R M
hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i
⊢ ⨆ i ∈ s, Submodule.map f (N i) ≤ ⨆ i ∈ s, N i
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ : R
a✝ : μ₁ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
μ₂ : R
hμ₂ : μ₂ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
hμ₁₂ : (fun x ↦ (f.genEigenspace x) k) μ₁ = (fun x ↦ (f.genEigenspace x) k) μ₂
contra : ¬μ₁ = μ₂
⊢ (f.genEigenspace μ₂) k = ⊥

Tactic:
simpa using

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ : R
a✝ : μ₁ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
μ₂ : R
hμ₂ : μ₂ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
hμ₁₂ : (fun x ↦ (f.genEigenspace x) k) μ₁ = (fun x ↦ (f.genEigenspace x) k) μ₂
contra : ¬μ₁ = μ₂
⊢ (f.genEigenspace μ₂) k = ⊥
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  (((mapBilinear (RingHom.id R) M N M N).compr₂ (trace R (M ⊗[R] N))) f) g =
    (((lsmul R R).compl₁₂ (trace R M) (trace R N)) f) g
⊢ (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g

Tactic:
simp only [compr₂_apply, mapBilinear_apply, compl₁₂_apply, lsmul_apply,
    smul_eq_mul] at h

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h : (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g
⊢ (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: K : Type u_6
V : Type u_7
W : Type u_8
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup W
inst✝² : Module K W
F : Type u_9
inst✝¹ : EquivLike F (End K V) (End K W)
inst✝ : AlgEquivClass F K (End K V) (End K W)
f : F
x : End K V
w✝ : V ≃ₗ[K] W
h : ↑f = LinearEquiv.conjAlgEquiv K w✝
⊢ ?m.65

Tactic:
simpa using

Goal state after:
K : Type u_6
V : Type u_7
W : Type u_8
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup W
inst✝² : Module K W
F : Type u_9
inst✝¹ : EquivLike F (End K V) (End K W)
inst✝ : AlgEquivClass F K (End K V) (End K W)
f : F
x : End K V
w✝ : V ≃ₗ[K] W
h : ↑f = LinearEquiv.conjAlgEquiv K w✝
⊢ ?m.65
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: K : Type u_6
m : Type u_7
n : Type u_8
inst✝⁶ : Field K
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
F : Type u_9
inst✝¹ : EquivLike F (Matrix m m K) (Matrix n n K)
inst✝ : AlgEquivClass F K (Matrix m m K) (Matrix n n K)
f : F
x : Matrix m m K
⊢ (f x).trace = x.trace

Tactic:
simpa using

Goal state after:
K : Type u_6
m : Type u_7
n : Type u_8
inst✝⁶ : Field K
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
F : Type u_9
inst✝¹ : EquivLike F (Matrix m m K) (Matrix n n K)
inst✝ : AlgEquivClass F K (Matrix m m K) (Matrix n n K)
f : F
x : Matrix m m K
⊢ (f x).trace = x.trace