mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.BilinearForm

Goal state before:
pp: M₂ : Type u_4
inst✝⁵ : AddCommGroup M₂
A : Type u_5
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Module A M₂
ι : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
B : BilinForm A M₂
b : Basis ι A M₂
⊢ B.Nondegenerate ↔ ((toMatrix b) B).det ≠ 0

Tactic:
← Matrix.nondegenerate_iff_det_ne_zero,

Goal state after:
M₂ : Type u_4
inst✝⁵ : AddCommGroup M₂
A : Type u_5
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Module A M₂
ι : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
B : BilinForm A M₂
b : Basis ι A M₂
⊢ B.Nondegenerate ↔ ((toMatrix b) B).Nondegenerate
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
i : ι
h₀ : b.IsPos i
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
⊢ p i

Tactic:
generalize hN : (b.height i).natAbs = N
  induction N using Nat.strongRecOn generalizing i with
  | ind n ih =>
    obtain ⟨j, hj, hj'⟩ := h₀.exists_mem_support_pos_pairingIn
    rw [P.zero_lt_pairingIn_iff'] at hj'
    rcases eq_or_ne i j with rfl | hij; · exact h₁ i hj
    have hk := h₀.reflectionPerm hj hij
    have : (b.height (P.reflectionPerm j i)).natAbs < n := by
      suffices b.height (P.reflectionPerm j i) < b.height i by
        have : (b.height (P.reflectionPerm j i)).natAbs = b.height (P.reflectionPerm j i) :=
          Int.natAbs_of_nonneg <| (isPos_iff' _).mp hk
        lia
      have := P.reflection_apply_root' ℤ (i := j) (j := i)
      rw [← root_reflectionPerm, sub_eq_add_neg, ← neg_smul] at this
      rw [b.height_add_zsmul this]
      replace hj : 0 < b.height j := (isPos_iff _).mp <| isPos_of_mem_support hj
      aesop
    simpa using h₂ (P.reflectionPerm j i) j
      (ih (m := (b.height (P.reflectionPerm j i)).natAbs) this hk rfl) hj

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
⊢ f.Pos ∨ (-f).Pos

Tactic:
refine (le_total 0 (f i)).imp ?_ ?_ <;>
    refine fun h => ⟨K, K0, i, fun j ij => ?_⟩ <;>
    have := (hi _ ij).1

Goal state after:
case inr.refine_1
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
⊢ K ≤ ↑f j

case inr.refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
⊢ K ≤ ↑(-f) j
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑(-f) j

Tactic:
rwa [abs_of_nonpos] at this

Goal state after:
case inr.refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ ↑f j ≤ 0
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ ↑a j - ↑b j ≤ 0

Tactic:
sub_nonpos,

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ ↑a j ≤ ↑b j
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Mul R
inst✝² : Star R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ star A.vec ⬝ᵥ B.vec = (Aᴴ * B).trace

Tactic:
star_vec,

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Mul R
inst✝² : Star R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ (A.map star).vec ⬝ᵥ B.vec = (Aᴴ * B).trace
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
⊢ (A.map f).IsHermitian ↔ A.IsHermitian

Tactic:
rw [IsHermitian, IsHermitian, ← conjTranspose_map f hf, map_injective hinj |>.eq_iff]

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

Goal state before:
pp: α : Type u_1
n : Type u_4
R : Type u_5
inst✝⁵ : Monoid R
inst✝⁴ : Star R
inst✝³ : Star α
inst✝² : MulAction R α
inst✝¹ : StarModule R α
A : Matrix n n α
k : R
inst✝ : Invertible k
h : (k • A).IsHermitian
hk : IsSelfAdjoint k
⊢ A.IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_smul, hk.star_eq] at h
  simpa using! congr(⅟k • $h)

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

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
d : n → R
μ : R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
⊢ (∃ i, d i = μ) → HasEigenvalue ((toLin b b) (diagonal d)) μ

Tactic:
rintro ⟨i, rfl⟩
    exact this i

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : 0 ≤ m
hn : 0 ≤ n
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
obtain ⟨k, rfl⟩ := eq_ofNat_of_zero_le hm
  obtain ⟨l, rfl⟩ := eq_ofNat_of_zero_le hn
  rw [← Int.natCast_add, zpow_natCast, zpow_natCast, zpow_natCast, pow_add]

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (-[m+1] * ↑n) = (A ^ -[m+1]) ^ ↑n

Tactic:
by
    rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast,
        inv_pow']

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

Goal state before:
pp: case refine_2
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ ∀ (p q : R[X]),
    ((aeval f) p) x = eval μ p • x → ((aeval f) q) x = eval μ q • x → ((aeval f) (p + q)) x = eval μ (p + q) • x

pp: case refine_3
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ ∀ (n : ℕ) (a : R),
    ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x →
      ((aeval f) (C a * X ^ (n + 1))) x = eval μ (C a * X ^ (n + 1)) • x

Tactic:
· intro p q hp hq; simp [hp, hq, add_smul]

Goal state after:
case refine_3
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ ∀ (n : ℕ) (a : R),
    ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x →
      ((aeval f) (C a * X ^ (n + 1))) x = eval μ (C a * X ^ (n + 1)) • x
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: R : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
f : End R M
inst✝² : IsDomain R
inst✝¹ : Module.Finite R M
inst✝ : IsTorsionFree R M
⊢ {μ | f.HasEigenvalue μ}.Finite

Tactic:
by
  have h : minpoly R f ≠ 0 := minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := R) f)
  refine ((minpoly R f).rootSet_finite R).subset ?_
  simp [Set.subset_def, hasEigenvalue_iff_isRoot, mem_rootSet, h]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
hrn : ∃ k < n, ↑k = -r
⊢ eval r (ascPochhammer R n) = 0

Tactic:
obtain ⟨rn, hrn, rnn⟩ := hrn
    convert! ascPochhammer_eval_neg_coe_nat_of_lt hrn
    simp [rnn]

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
hy : y ∈ prodCartan eι b₁ b₂
x : ↥H₁
⊢ ⁅(↑y).1, ↑x⁆ = 0

Tactic:
have := b₁.isLieAbelian_cartan

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
hy : y ∈ prodCartan eι b₁ b₂
x : ↥H₁
this : IsLieAbelian ↥H₁
⊢ ⁅(↑y).1, ↑x⁆ = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
⊢ ((interpolate (insert i (t \ s)) v) r).degree + (Lagrange.basis s v i).degree < ↑(#t)

Tactic:
have hs : 1 ≤ #s := Nonempty.card_pos ⟨_, hi⟩

Goal state after:
case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs✝ : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
⊢ ((interpolate (insert i (t \ s)) v) r).degree + (Lagrange.basis s v i).degree < ↑(#t)
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
hy : y ∈ prodCartan eι b₁ b₂
x : ↥H₂
⊢ ⁅(↑y).2, ↑x⁆ = 0

Tactic:
suffices (prodSymmEquiv eι b₁ b₂).symm y ∈ prodCartan eι.symm b₂ b₁ from
    lie_fst_eq_zero_of_mem_prodCartan eι.symm b₂ b₁ this x
  replace hy :
      (prodSymmEquiv eι b₁ b₂).symm y ∈ (prodCartan eι b₁ b₂).map (prodSymmEquiv eι b₁ b₂).symm :=
    mem_image_of_mem (prodSymmEquiv eι b₁ b₂).symm hy
  rw [prodCartan, map_lieSpan] at hy
  rw [prodCartan]
  convert hy
  ext; simp; grind

Goal state after:
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this✝ : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
this : ∑ i, f ⟨μ i, ⋯⟩ • ⟨μ i, ⋯⟩ = 0
⊢ ∑ i, f ⟨μ i, ⋯⟩ ^ 2 = 0

Tactic:
by
    simpa only [map_sum, map_zero, map_smul, sq] using! f.congr_arg this

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
k : ℕ
⊢ f ^ k = (aeval f) (X ^ k %ₘ f.charpoly)

Tactic:
by
  rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]

Goal state after:
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
r : K[X]
hr : (aeval ((ad K (End K M)) s)) r = (ad K (End K M)) y
p : K[X]
hp : (aeval ((ad K (End K M)) (φ x))) p = (ad K (End K M)) s
⊢ (aeval ((ad K (End K M)) (φ x))) (r.comp p) = (ad K (End K M)) y

Tactic:
aeval_comp,

Goal state after:
L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
r : K[X]
hr : (aeval ((ad K (End K M)) s)) r = (ad K (End K M)) y
p : K[X]
hp : (aeval ((ad K (End K M)) (φ x))) p = (ad K (End K M)) s
⊢ (aeval ((aeval ((ad K (End K M)) (φ x))) p)) r = (ad K (End K M)) y
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n

Tactic:
rw [← hm hd, ← hn hd]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
a✝ : j ∈ DFinsupp.support ((decompose 𝒜) r)
⊢ ↑(((decompose 𝒜) r) j) ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
apply Ideal.subset_span

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
a✝ : j ∈ DFinsupp.support ((decompose 𝒜) r)
⊢ ↑(((decompose 𝒜) r) j) ∈ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n

Tactic:
rw [← hm hd, ← hn hd]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ (homogeneousHull 𝒜 I).toIdeal = ⨆ i, span (⇑(GradedRing.proj 𝒜 i) '' ↑I)

Tactic:
by
  rw [← Ideal.span_iUnion]
  apply congr_arg Ideal.span _
  ext1
  simp only [Set.mem_iUnion, Set.mem_image, mem_ofPred_eq, GradedRing.proj_apply, SetLike.exists,
    exists_prop, SetLike.mem_coe]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (if (weight w) d = (weight w) d then coeff d φ else 0) = coeff d φ

Tactic:
if_pos rfl

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d φ = coeff d φ
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weight w) d ∉ Finite.toFinset ⋯
⊢ (if (weight w) d = (weight w) d then coeff d φ else 0) = 0

Tactic:
if_pos rfl

Goal state after:
case h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weight w) d ∉ Finite.toFinset ⋯
⊢ coeff d φ = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : charpoly φ = X ^ finrank R M
⊢ φ ^ finrank R M = 0

Tactic:
rw [← @aeval_X_pow R, ← h, aeval_self_charpoly φ]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if m = m then coeff x p else 0) = coeff x p

Tactic:
if_pos rfl

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ coeff x p = coeff x p
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : LinearOrder M
inst✝¹ : OrderBot M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
⊢ IsWeightedHomogeneous w p ⊥ ↔ ∀ s ∈ p.support, (weight w) s = ⊥

Tactic:
bot_eq_zero,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : LinearOrder M
inst✝¹ : OrderBot M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
⊢ IsWeightedHomogeneous w p 0 ↔ ∀ s ∈ p.support, (weight w) s = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
x : M
H : ∀ (i : ℕ), ∃ y, (φ ^ i) y = x
n : ℕ
⊢ ∃ y, (φ ^ n) y = φ x

Tactic:
obtain ⟨y, rfl⟩ := H n

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ y_1, (φ ^ i) y_1 = (φ ^ n) y
⊢ ∃ y_1, (φ ^ n) y_1 = φ ((φ ^ n) y)
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
⊢ ∃ r, (eval r) ((polyCharpoly (?m.208 r) b).coeff φ.nilRank) ≠ 0

Tactic:
by
    by_contra! h₀
    apply polyCharpoly_coeff_nilRank_ne_zero φ b
    apply aux.eq_zero_of_forall_eval_eq_zero_of_le_card h₀ (le_trans _ h)
    simp only [n, finrank_eq_card_chooseBasisIndex, Nat.cast_le, Nat.sub_le]

Goal state after: