mathlib-initiative/mathlib-tactics huggingface dataset:
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
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι}, b.IsPos i → P.root k = P.root i + -↑w • P.root j → LinearIndependent R ![P.root j, P.root i] → b.IsPos k
i k : ι
hi : b.IsPos i
hk : P.root k = P.root i + (-↑w - 1) • P.root j
hij : LinearIndependent R ![P.root j, P.root i]
⊢ P.root k = P.root i - (w + 1) • P.root j

Tactic:
by rw [hk]; module

Goal state after:
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 j : ι
hi : b.IsPos i
hj : j ∈ b.support
hij : i ≠ j
⊢ P.root ((P.reflectionPerm j) i) = P.root i + -P.pairingIn ℤ i j • P.root j

Tactic:
root_reflectionPerm,

Goal state after:
ι : 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 j : ι
hi : b.IsPos i
hj : j ∈ b.support
hij : i ≠ j
⊢ (P.reflection j) (P.root i) = P.root i + -P.pairingIn ℤ i j • P.root j
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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι}, b.IsPos i → b.height i = ↑n → p i
i : ι
h₀ : b.IsPos i
hN : b.height i = ↑n + 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk : P.root k = P.root i - P.root j
hkn : b.height k = ↑n
hkpos : b.IsPos k
⊢ P.root i = P.root k + P.root j

Tactic:
by rw [hk]; module

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
⊢ False

Tactic:
have hlz : LimZero (f * g) := by simpa

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
⊢ False
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case inr.h.h.h
x : ℝ
a b : CauSeq ℚ abs
h✝ : mk a < mk b
c : CauSeq ℚ abs
⊢ mk a + mk c < mk b + mk c

Tactic:
simp only [mk_lt, ← mk_add] at *
      change Pos _ at *
      rwa [add_sub_add_right_eq_sub]

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
⊢ a₁ ⊓ b₁ ≈ a₂ ⊓ b₂

Tactic:
by
  intro ε ε0
  obtain ⟨ai, hai⟩ := ha ε ε0
  obtain ⟨bi, hbi⟩ := hb ε ε0
  exact
    ⟨ai ⊔ bi, fun i hi =>
      (abs_min_sub_min_le_max (a₁ i) (b₁ i) (a₂ i) (b₂ i)).trans_lt
        (max_lt (hai i (sup_le_iff.mp hi).1) (hbi i (sup_le_iff.mp hi).2))⟩

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
f : CauSeq ℚ abs
⊢ (∃ i, ∀ j ≥ i, x ≤ ↑(↑f j)) → x ≤ mk f

Tactic:
intro h
  induction x using Real.ind_mk
  apply le_of_not_gt
  rw [mk_lt]
  rintro ⟨K, K0, hK⟩
  obtain ⟨i, H⟩ := exists_forall_ge_and h (exists_forall_ge_and hK (f.cauchy₃ <| half_pos K0))
  apply not_lt_of_ge (H _ le_rfl).1
  rw [← mk_const, mk_lt]
  refine ⟨_, half_pos K0, i, fun j ij => ?_⟩
  have := add_le_add (H _ ij).2.1 (le_of_lt (abs_lt.1 <| (H _ le_rfl).2.2 _ ij).1)
  rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≤ c
hb : a ≈ b
⊢ a ≤ b ⊓ c

Tactic:
· replace hc := le_of_eq_of_le (Setoid.symm hb) hc
    refine le_of_eq_of_le hb (Or.inr ?_)
    exact Setoid.symm (CauSeq.inf_eq_left hc)

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

Goal state before:
pp: case inl
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
a b : α
h✝ : ¬ia = ib
⊢ single ia ja a ⊙ single ib jb b = 0

Tactic:
simp only [single]

Goal state after:
case inl
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
a b : α
h✝ : ¬ia = ib
⊢ ((of fun i' j' ↦ if ia = i' ∧ ja = j' then a else 0) ⊙ of fun i' j' ↦ if ib = i' ∧ jb = j' then b else 0) = 0
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: case inr
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
a b : α
h✝ : ¬ja = jb
⊢ single ia ja a ⊙ single ib jb b = 0

Tactic:
simp only [single]

Goal state after:
case inr
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
a b : α
h✝ : ¬ja = jb
⊢ ((of fun i' j' ↦ if ia = i' ∧ ja = j' then a else 0) ⊙ of fun i' j' ↦ if ib = i' ∧ jb = j' then b else 0) = 0
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
A : Matrix n n α
h : (-A).IsHermitian
⊢ A.IsHermitian

Tactic:
← neg_neg A

Goal state after:
α : Type u_1
n : Type u_4
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
A : Matrix n n α
h : (-A).IsHermitian
⊢ (- -A).IsHermitian
Module: Mathlib.LinearAlgebra.Eigenspace.Matrix

Goal state before:
pp: case inr
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
k : ℕ
hk : ∀ (j : n), (b.repr x) j = 0 ∨ d j = μ ∧ k ≠ 0
j : n
hj : d j = μ ∧ k ≠ 0
⊢ ((b.repr x) j * d j) • b j = μ • (b.repr x) j • b j

Tactic:
rw [← hj.1, mul_comm, mul_smul]

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

Goal state before:
pp: case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
this : (X + 1).leadingCoeff = 1
⊢ (ascPochhammer S (n + 1)).Monic

Tactic:
ascPochhammer_succ_left,

Goal state after:
case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
this : (X + 1).leadingCoeff = 1
⊢ (X * (ascPochhammer S n).comp (X + 1)).Monic
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
t : T
⊢ eval t (ascPochhammer T n) = eval₂ f t (ascPochhammer S n)

Tactic:
rw [← ascPochhammer_map f]

Goal state after:
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
t : T
⊢ eval t (map f (ascPochhammer S n)) = eval₂ f t (ascPochhammer S n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝ : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
| ascPochhammer ℕ (n + 1 + 1)

Tactic:
ascPochhammer_succ_left,

Goal state after:
S : Type u
inst✝ : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
| X * (ascPochhammer ℕ (n + 1)).comp (X + 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: n t : ℕ
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)

Tactic:
rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]

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

Goal state before:
pp: case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ descPochhammer ℤ n * (X - ↑n) = (ascPochhammer ℤ (n + 1)).comp (X - ↑n)

Tactic:
ascPochhammer_succ_left,

Goal state after:
case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ descPochhammer ℤ n * (X - ↑n) = (X * (ascPochhammer ℤ n).comp (X + 1)).comp (X - ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
⊢ eval (r - ↑n + 1) (ascPochhammer R n) * (r - ↑n) = eval (r - ↑n) (ascPochhammer R (n + 1))

Tactic:
ascPochhammer_succ_left,

Goal state after:
case succ
R : Type u
inst✝ : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
⊢ eval (r - ↑n + 1) (ascPochhammer R n) * (r - ↑n) = eval (r - ↑n) (X * (ascPochhammer R n).comp (X + 1))
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case h₂
ι : 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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
i j k : ι
l : ι₂
hl : P₂.root l = f (P.root j)
hk : k ∈ b.support
this : f ((P.reflection k) (P.root j)) = (P₂.reflection ↑(e ⟨k, hk⟩)) (f (P.root j))
⊢ f (P.root ((P.reflectionPerm k) j)) ∈ range ⇑P₂.root

Tactic:
root_reflectionPerm,

Goal state after:
case h₂
ι : 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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
i j k : ι
l : ι₂
hl : P₂.root l = f (P.root j)
hk : k ∈ b.support
this : f ((P.reflection k) (P.root j)) = (P₂.reflection ↑(e ⟨k, hk⟩)) (f (P.root j))
⊢ f ((P.reflection k) (P.root j)) ∈ range ⇑P₂.root
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = ↑((n - k) * n.descFactorial k)

pp: case neg
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : k ≤ n
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = ↑((n - k) * n.descFactorial k)

Tactic:
· rw [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, mul_zero, mul_zero, Nat.cast_zero]

Goal state after:
case neg
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : k ≤ n
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = ↑((n - k) * n.descFactorial k)
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
⊢ ((p j).sum fun e a ↦ (RingHom.id R) a * v i ^ e) = ∑ j_1, vandermonde v i j_1 * (p j).coeff ↑j_1

Tactic:
simp only [Matrix.vandermonde]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
⊢ ((p j).sum fun e a ↦ (RingHom.id R) a * v i ^ e) = ∑ j_1, of (fun i j ↦ v i ^ ↑j) i j_1 * (p j).coeff ↑j_1
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ∃ n, (0 ^ n) x = 0

Tactic:
use 1

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ (0 ^ 1) x = 0
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case h.zero
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
y : ↥N
⊢ y ∈ (dx ^ 0).ker → ((ad R L) x ^ 0) (N.subtype y) = 0

Tactic:
cases y

Goal state after:
case h.zero.mk
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
val✝ : L
property✝ : val✝ ∈ N
⊢ ⟨val✝, property✝⟩ ∈ (dx ^ 0).ker → ((ad R L) x ^ 0) (N.subtype ⟨val✝, property✝⟩) = 0
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
h₁ : ∀ (i j : I), ⁅s, v.end (i, j)⁆ = (μ i - μ j) • v.end (i, j)
h₂ : ∀ (i j : I), ⁅y, v.end (i, j)⁆ = (fμ i - fμ j) • v.end (i, j)
⊢ ∃ r, (aeval ((ad K (End K M)) s)) r = (ad K (End K M)) y

Tactic:
obtain ⟨r, hr⟩ := exists_polynomial_eval_sub_aux μ hμ f

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
h₁ : ∀ (i j : I), ⁅s, v.end (i, j)⁆ = (μ i - μ j) • v.end (i, j)
h₂ : ∀ (i j : I), ⁅y, v.end (i, j)⁆ = (fμ i - fμ j) • v.end (i, j)
r : K[X]
hr : ∀ (i j : I), Polynomial.eval (μ i - μ j) r = (algebraMap ℚ K) (↑f ⟨μ i, ⋯⟩) - (algebraMap ℚ K) (↑f ⟨μ j, ⋯⟩)
⊢ ∃ r, (aeval ((ad K (End K M)) s)) r = (ad K (End K M)) y
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
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
h : (minpoly R f).coeff 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < (minpoly R f).degree
this : (minpoly R f).Monic
⊢ P.Monic

Tactic:
by
      rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R (M₁ × M₂) := b₁.prod b₂
⊢ (f₁.prodMap f₂).charpoly = ((toMatrix b₁ b₁) f₁).charpoly * f₂.charpoly

Tactic:
← charpoly_toMatrix f₂ b₂,

Goal state after:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R (M₁ × M₂) := b₁.prod b₂
⊢ (f₁.prodMap f₂).charpoly = ((toMatrix b₁ b₁) f₁).charpoly * ((toMatrix b₂ b₂) f₂).charpoly
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✝ : SemilatticeSup M
w : σ → M
p : MvPolynomial σ R
⊢ weightedTotalDegree' w p = ⊥ ↔ p = 0

Tactic:
by
  simp only [weightedTotalDegree', Finset.sup_eq_bot_iff, mem_support_iff, WithBot.coe_ne_bot,
    MvPolynomial.eq_zero_iff]
  exact forall_congr' fun _ => Classical.not_not

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst✝ : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ↑n ≤ φ.support.sup fun s ↦ ↑((weight w) s)

Tactic:
simp only [← hφ hd]

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst✝ : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ↑((weight w) d) ≤ φ.support.sup fun s ↦ ↑((weight w) s)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
σ : Type u_5
τ : Type u_6
e : σ → τ
w : τ → ℕ
P : MvPolynomial σ R
he : Function.Injective e
⊢ weightedTotalDegree w ((rename e) P) = weightedTotalDegree (w ∘ e) P

Tactic:
unfold weightedTotalDegree
  rw [support_rename_of_injective he, Finset.sup_image]
  congr; ext; unfold weight; simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
⊢ degree 0 = 0

Tactic:
simp only [degree_apply, Finsupp.support_zero, zero_apply, Finset.sum_const_zero]

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
⊢ ∑ᶠ (m : M), (weightedHomogeneousComponent w m) φ = φ

Tactic:
finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
⊢ ∑ i ∈ Finite.toFinset ⋯, (weightedHomogeneousComponent w i) φ = φ
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
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)

Tactic:
rw [h zero_coeff]

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if n = m then coeff x p else 0) = coeff x (if m = n then p else 0)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case inr.hnc
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
i : σ
hi : ¬d i = 0
⊢ ∃ x, ¬d x = 0 ∧ ¬w x = 0

Tactic:
exact ⟨i, hi, hw i⟩

Goal state after:
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
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
x : ↥W
hx : G x = 0
⊢ ∃ k, (φ ^ k) ↑x = 0

Tactic:
use 1

Goal state after:
case h
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 := ⋯
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⋯
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := ⋯
G : ↥W →ₗ[K] ↥W := ⋯
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := ⋯
e : (↥V × ↥W) ≃ₗ[K] M := ⋯
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := ⋯
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := ⋯
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := ⋯
hψ : ψ = e.symm.conj φ
x : ↥W
hx : G x = 0
⊢ (φ ^ 1) ↑x = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ (homogeneousComponent n) φ = 0

Tactic:
apply homogeneousComponent_eq_zero'
  rw [totalDegree, Finset.sup_lt_iff (lt_of_le_of_lt (Nat.zero_le _) h)] at h
  intro d hd; exact ne_of_lt (h d hd)

Goal state after: