mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case mpr
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
inst✝ : Fintype G
x : k[G]
⊢ (linearCombination k fun x ↦ 1) x.coeff = 0 →
    ((lsmul k k[G]).flip ((leftRegular k G).norm (MonoidAlgebra.single 1 1)) ∘ₗ
          (linearCombination k fun x ↦ 1) ∘ₗ ↑(coeffLinearEquiv k))
        x =
      0

Tactic:
intro h

Goal state after:
case mpr
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
inst✝ : Fintype G
x : k[G]
h : (linearCombination k fun x ↦ 1) x.coeff = 0
⊢ ((lsmul k k[G]).flip ((leftRegular k G).norm (MonoidAlgebra.single 1 1)) ∘ₗ
        (linearCombination k fun x ↦ 1) ∘ₗ ↑(coeffLinearEquiv k))
      x =
    0
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
n : ℕ
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
this : ↑n ∈ S ↔ n ≤ chainTopCoeff i j
⊢ P.root j + n • P.root i ∈ range ⇑P.root ↔ n ≤ chainTopCoeff i j

Tactic:
simpa only [S_def, mem_ofPred_eq, natCast_zsmul] using this

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case inr
ι : 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
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
neg : f < 0
contra : ∀ i ∈ b.support, 0 ≤ f i
⊢ False

Tactic:
replace contra (j : ι) : f j = 0 := by
      by_cases hj : j ∈ f.support
      · exact le_antisymm (neg.le j) (contra j (hf₀ hj))
      · simpa using hj

Goal state after:
case inr
ι : 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
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
neg : f < 0
contra : ∀ (j : ι), f j = 0
⊢ False
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 : CauSeq β abv
hf : ¬f ≈ 0
⊢ ¬f.LimZero

Tactic:
intro h

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f ≈ 0
h : f.LimZero
⊢ False
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
⊢ const x ≤ const y ↔ x ≤ y

Tactic:
by
  rw [le_iff_lt_or_eq]; exact or_congr const_lt const_equiv

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ⟦f⟧ ≠ 0
⊢ (⟦f⟧)⁻¹ * ⟦f⟧ = 1

Tactic:
by
    simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf
    simp only [mk_eq_mk, hf, not_false_eq_true, inv_mk, mk_mul]
    exact Quotient.sound (CauSeq.inv_mul_cancel hf)

Goal state after:
Module: Mathlib.Algebra.Star.Pi

Goal state before:
pp: I : Type u_1
J : Type u_2
α : Type u_3
x✝ : I → α
y : J → α
inst✝ : Star α
x : I ⊕ J
⊢ star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x

Tactic:
cases x

Goal state after:
case inl
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst✝ : Star α
val✝ : I
⊢ star (Sum.elim x y) (Sum.inl val✝) = Sum.elim (star x) (star y) (Sum.inl val✝)

case inr
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst✝ : Star α
val✝ : J
⊢ star (Sum.elim x y) (Sum.inr val✝) = Sum.elim (star x) (star y) (Sum.inr val✝)
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
q : ℚ≥0
⊢ ofRat ↑q.num / ofRat ↑q.den = ↑q.num / ↑q.den

Tactic:
ofRat_natCast

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

Goal state after:
x : ℝ
f : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, x ≤ ↑(↑f j)
⊢ x ≤ mk f
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
⊢ (∀ (i j : n), star (A j i) = A i j) → A.IsHermitian

Tactic:
intro h

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
⊢ A.IsHermitian
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
⊢ Aᵀ.IsHermitian → A.IsHermitian

Tactic:
intro h

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ A.IsHermitian
Module: Mathlib.LinearAlgebra.Eigenspace.Matrix

Goal state before:
pp: 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
i : n
b : Basis n R M
⊢ ((toLin b b) (diagonal d)) (b i) = d i • b i

Tactic:
by simp [diagonal]

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℕ
x : n →₀ R
i : n
x✝¹ : i ∈ x.support
j : n
x✝ : j ∈ x.support
⊢ 0 ≤ star (x i) * ↑d i j * x j

Tactic:
obtain rfl | hij := eq_or_ne i j <;> simp [← diagonal_natCast', star_left_conjugate_nonneg, *]

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs : ⨆ α ∈ s, rootSpace H α = ⊤
χ : Weight K (↥H) L
hχ : χ ∈ root
⊢ Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp') ∨
    -Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')

Tactic:
replace hs : ⇑χ ∈ s :=
    (iSupIndep_genWeightSpace K H L).mem_of_biSup_eq_top hs χ.genWeightSpace_ne_bot

Goal state after:
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
χ : Weight K (↥H) L
hχ : χ ∈ root
hs : ⇑χ ∈ s
⊢ Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp') ∨
    -Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
induction n with
  | zero => rw [descPochhammer_zero, ascPochhammer_zero, one_comp]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]

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

Goal state before:
pp: case refine_1.succ.inl
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
h : eval r (ascPochhammer R n) = 0
⊢ ∃ k < n + 1, ↑k = -r

Tactic:
obtain ⟨rn, hrn, rrn⟩ := ih h
        exact ⟨rn, by lia, rrn⟩

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

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

Tactic:
refine ⟨fun zero' ↦ ?_, fun hrn ↦ ?_⟩
  · induction n with
    | zero => simp only [ascPochhammer_zero, Polynomial.eval_one, one_ne_zero] at zero'
    | succ n ih =>
      rw [ascPochhammer_succ_eval, mul_eq_zero] at zero'
      cases zero' with
      | inl h =>
        obtain ⟨rn, hrn, rrn⟩ := ih h
        exact ⟨rn, by lia, rrn⟩
      | inr h =>
        exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩
  · obtain ⟨rn, hrn, rnn⟩ := hrn
    convert! ascPochhammer_eval_neg_coe_nat_of_lt hrn
    simp [rnn]

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

Goal state before:
pp: S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
s : S
h : ↑n - 1 < s
⊢ 0 < eval s (descPochhammer S n)

Tactic:
by
  rw [← sub_pos, ← sub_add] at h
  rw [descPochhammer_eval_eq_ascPochhammer]
  exact ascPochhammer_pos n (s - n + 1) h

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ eval (v i) (basisDivisor (v i) (v j)) = 1

Tactic:
eval_basisDivisor_left_of_ne

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ 1 = 1

F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ v i ≠ v j
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₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
i j : ι₁
⊢ ⁅prodH eι b₁ b₂ i, prodH eι b₁ b₂ j⁆ = 0

Tactic:
by simp [Subtype.ext_iff, b₁.lie_h_h, b₂.lie_h_h]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case mp
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
⊢ (f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i) → f = (interpolate s v) r

Tactic:
intro h

Goal state after:
case mp
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i
⊢ f = (interpolate s v) r
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
⊢ f = (interpolate s v) r → f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i

Tactic:
intro h

Goal state after:
case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = (interpolate s v) r
⊢ f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) +
      (interpolate (insert j (s \ {i, j})) v) r * basisDivisor (v j) (v i) =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s

Tactic:
pair_comm,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) +
      (interpolate (insert j (s \ {j, i})) v) r * basisDivisor (v j) (v i) =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
⊢ (⇑derivative)^[k] ((interpolate s v) r) =
    ↑k.factorial *
      ∑ i ∈ s,
        C (r i / ∏ j ∈ s.erase i, (v i - v j)) * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ a ∈ t, (X - C (v a))

Tactic:
classical
  simp_rw [interpolate_eq_sum, iterate_derivative_sum, iterate_derivative_C_mul, mul_sum s,
    ← mul_assoc, mul_comm (k.factorial : F[X]), mul_assoc]
  congr! 2 with i hi
  have hvs' := hvs.mono (coe_subset.mpr (erase_subset i s))
  calc
    derivative^[k] (∏ j ∈ s.erase i, (X - C (v j))) =
    derivative^[k] (∏ vj ∈ (s.erase i).image v, (X - C vj)) := by rw [Finset.prod_image hvs']
    _ = k.factorial * ∑ t ∈ ((s.erase i).image v).powersetCard (#s - (k + 1)),
          ∏ va ∈ t, (X - C va) := by
        grind [iterate_derivative_prod_X_sub_C]
    _ = k.factorial * ∑ t ∈ (s.erase i).powersetCard (#s - (k + 1)), ∏ a ∈ t, (X - C (v a)) := by
        rw [powersetCard_eq_filter, powerset_image, eq_comm]
        congrm k.factorial * ?_
        refine sum_nbij (·.image v) (fun a ha ↦ ?hi) ?i_inj (fun t ht ↦ ?i_surj) fun a ha ↦ ?h
        case hi => grind [card_image_of_injOn, hvs'.mono]
        case i_inj => exact (image_injOn_powerset_of_injOn hvs').mono (by grind)
        case i_surj => grind [card_image_of_injOn, hvs'.mono]
        case h => exact eq_comm.mp <| prod_image <| by grind [hvs'.mono]

Goal state after:
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
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
⊢ H.normalizer = H

Tactic:
set N := normalizer H
  apply le_antisymm _ (le_normalizer H)
  calc N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule := ?_
       _ = H := by rwa [sup_eq_right]
  have aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H := by
    intro n hn
    rw [mem_normalizer_iff] at hn
    specialize hn x (h (self_mem_engel R x))
    rwa [← lie_skew, neg_mem_iff (G := L)]
  have aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N := fun n hn ↦ le_normalizer H (aux₁ _ hn)
  let dx : N →ₗ[R] N := (ad R L x).restrict aux₂
  obtain ⟨k, hk⟩ : ∃ a, ∀ b ≥ a, Codisjoint (LinearMap.ker (dx ^ b)) (LinearMap.range (dx ^ b)) :=
    eventually_atTop.mp <| dx.eventually_codisjoint_ker_pow_range_pow
  specialize hk (k + 1) (Nat.le_add_right k 1)
  rw [← Submodule.map_subtype_top N.toSubmodule, Submodule.map_le_iff_le_comap]
  apply hk
  · rw [← Submodule.map_le_iff_le_comap]
    apply le_sup_of_le_left
    rw [Submodule.map_le_iff_le_comap]
    intro y hy
    simp only [Submodule.mem_comap, mem_engel_iff, mem_toSubmodule]
    use k + 1
    clear hk; revert hy
    generalize k + 1 = k
    induction k generalizing y with
    | zero =>
      cases y; intro hy; simp only [pow_zero, Module.End.one_apply]
      exact (AddSubmonoid.mk_eq_zero N.toAddSubmonoid).mp hy
    | succ k ih => solve_by_elim
  · rw [← Submodule.map_le_iff_le_comap]
    apply le_sup_of_le_right
    rw [Submodule.map_le_iff_le_comap]
    rintro _ ⟨y, rfl⟩
    simp only [pow_succ', Module.End.mul_apply, Submodule.mem_comap, mem_toSubmodule]
    apply aux₁
    simp only [Submodule.coe_subtype, SetLike.coe_mem]

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
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
⊢ (minpoly R f).coeff 0 ≠ 0

Tactic:
intro h

Goal state after:
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
⊢ False
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⋯
h : ∀ x ∈ I, ∀ y ∈ DI, ((killingForm R L) x) y = 0
DDI : LieIdeal R L := ⋯
tf_eq_zero : LieModule.traceForm R (↥DI) L = 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
x : L
hx : x ∈ DDI
⊢ IsNilpotent ((ad R L) ↑⟨x, hx⟩)

Tactic:
refine (LieModule.isNilpotent_iff_forall' (R := R)).mp module_nilp
      ⟨⟨x, LieSubmodule.lie_le_left DI DI hx⟩, ?_⟩

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h : ∀ x ∈ I, ∀ y ∈ DI, ((killingForm R L) x) y = 0
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : LieModule.traceForm R (↥DI) L = 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
x : L
hx : x ∈ DDI
⊢ ⟨x, ⋯⟩ ∈ derivedSeries R (↥DI) 1
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
⊢ ↑(((decompose 𝒜) (∑ a ∈ s.support, s a • ↑a)) i) ∈ span s✝

Tactic:
decompose_sum,

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
⊢ ↑((∑ i ∈ s.support, (decompose 𝒜) (s i • ↑i)) i) ∈ span s✝
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 𝒜
κ : Sort u_4
κ' : κ → Sort u_5
s : (i : κ) → κ' i → HomogeneousIdeal 𝒜
⊢ (⨆ i, ⨆ j, s i j).toIdeal = ⨆ i, ⨆ j, (s i j).toIdeal

Tactic:
by
  simp_rw [toIdeal_iSup]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ p.IsHomogeneous 0

Tactic:
rw [← weightedTotalDegree_one,
    ← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsHomogeneous]

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

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

Tactic:
by
  rw [degree_eq_weight_one] at hd
  exact IsWeightedHomogeneous.coeff_eq_zero hφ d hd

Goal state after:
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
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
h : charpoly φ = X ^ finrank R M
m : M
⊢ ∃ n, (φ ^ n) m = 0

Tactic:
by
    use finrank R M
    suffices φ ^ finrank R M = 0 by simp only [this, LinearMap.zero_apply]
    simpa only [h, map_pow, aeval_X] using φ.aeval_self_charpoly

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ∑ x ∈ d.support, d x ≤ ∑ x ∈ d.support, d x

Tactic:
le_rfl

Goal state after:
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
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
tfae_3_to_1 : (∀ (m : M), ∃ n, (φ ^ n) m = 0) → IsNilpotent φ
⊢ charpoly φ = X ^ finrank R M ↔ (charpoly φ).natTrailingDegree = finrank R M

Tactic:
← φ.charpoly_natDegree,

Goal state after:
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
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
tfae_3_to_1 : (∀ (m : M), ∃ n, (φ ^ n) m = 0) → IsNilpotent φ
⊢ charpoly φ = X ^ (charpoly φ).natDegree ↔ (charpoly φ).natTrailingDegree = (charpoly φ).natDegree
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
n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p n
⊢ (weightedHomogeneousComponent w n) p = p

Tactic:
simp [weightedHomogeneousComponent_of_mem hp]

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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
F : K[X]
hF : charpoly φ = minpoly K φ * F
⊢ eval 0 (minpoly K φ) = 0 → eval 0 (minpoly K φ) * eval 0 F = 0

Tactic:
intro h

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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
F : K[X]
hF : charpoly φ = minpoly K φ * F
h : eval 0 (minpoly K φ) = 0
⊢ eval 0 (minpoly K φ) * eval 0 F = 0
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
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ (coeLinearMap fun i ↦ weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun x x_1 ↦ ↑x_1

Tactic:
rw [_root_.DirectSum.coeLinearMap_eq_dfinsuppSum]

Goal state after: