mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this✝ : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
this : li = 3 * lj ∨ lj = 3 * li
⊢ (∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 2 * P.pairing j i ∨ P.pairing j i = 2 * P.pairing i j) ∨
    ∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 3 * P.pairing j i ∨ P.pairing j i = 3 * P.pairing i j

Tactic:
refine Or.inr fun k₁ k₂ ↦ ?_

Goal state after:
case neg.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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this✝ : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
this : li = 3 * lj ∨ lj = 3 * li
k₁ k₂ : ι
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
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 i + -↑w • P.root j ∈ range ⇑P.root

Tactic:
replace hk : P.root i - (w + 1) • P.root j ∈ range P.root := ⟨k, by rw [hk]; module⟩
      rw [neg_smul, ← sub_eq_add_neg, natCast_zsmul]
      simp only [root_sub_nsmul_mem_range_iff_le_chainBotCoeff hij] at hk ⊢
      lia

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 : ℕ → β
hf : IsCauSeq abv f
i : ℕ
h : ∀ j ≥ i, abv (f j - f i) < 1
R : ℕ → α := Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
hR : R = Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
this : ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i
⊢ ∃ r, ∀ (i : ℕ), abv (f i) < r

Tactic:
refine ⟨R i + 1, fun j ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i : ℕ
h : ∀ j ≥ i, abv (f j - f i) < 1
R : ℕ → α := Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
hR : R = Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
this : ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i
j : ℕ
⊢ abv (f j) < R i + 1
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
n : ℕ
⊢ A⁻¹ ^ -[n+1] = (A ^ -[n+1])⁻¹

Tactic:
by rw [zpow_negSucc, zpow_negSucc, inv_pow']

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

Goal state before:
pp: case refine_2.refine_1
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ i ∈ x.support

Tactic:
simp +contextual [diagonal,
      apply_ite, star_left_conjugate_nonneg (h _).le,
      star_left_conjugate_pos (h i), IsRegular.of_ne_zero hxi, Finsupp.mem_support_iff.mpr hxi]

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

Goal state before:
pp: case refine_2.refine_2
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ ∀ i_1 ∈ x.support, 0 ≤ star (x i) * diagonal d i i_1 * x i_1

Tactic:
simp +contextual [diagonal,
      apply_ite, star_left_conjugate_nonneg (h _).le,
      star_left_conjugate_pos (h i), IsRegular.of_ne_zero hxi, Finsupp.mem_support_iff.mpr hxi]

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

Goal state before:
pp: case refine_2.refine_3
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ i ∈ x.support

Tactic:
simp +contextual [diagonal,
      apply_ite, star_left_conjugate_nonneg (h _).le,
      star_left_conjugate_pos (h i), IsRegular.of_ne_zero hxi, Finsupp.mem_support_iff.mpr hxi]

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

Goal state before:
pp: case refine_2.refine_4
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ 0 < star (x i) * diagonal d i i * x i

Tactic:
simp +contextual [diagonal,
      apply_ite, star_left_conjugate_nonneg (h _).le,
      star_left_conjugate_pos (h i), IsRegular.of_ne_zero hxi, Finsupp.mem_support_iff.mpr hxi]

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

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✝¹ : P.IsCrystallographic
inst✝ : CharZero R
i j : ↥b.support
⊢ b.cartanMatrix i j = 0 ↔ P.pairing ↑i ↑j = 0

Tactic:
rw [cartanMatrix, cartanMatrixIn_def, ← (algebraMap_injective ℤ R).eq_iff,
    algebraMap_pairingIn, map_zero]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.SuperFactorial

Goal state before:
pp: n : ℕ
⊢ ∏ x ∈ Ico 1 (n + 1 + 1), x ! = sf n + 1

Tactic:
prod_Ico_succ_top le_add_self,

Goal state after:
n : ℕ
⊢ (∏ k ∈ Ico 1 (n + 1), k !) * (n + 1)! = sf n + 1
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (ascPochhammer S n) * k + eval k (ascPochhammer S n * ↑n) = eval k (ascPochhammer S n) * (k + ↑n)

Tactic:
← Nat.cast_comm,

Goal state after:
S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (ascPochhammer S n) * k + eval k (↑n * ascPochhammer S n) = eval k (ascPochhammer S n) * (k + ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n * X) + eval s (ascPochhammer S n * ↑n)

Tactic:
← Nat.cast_comm,

Goal state after:
case succ
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n * X) + eval s (↑n * ascPochhammer S n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝ : Ring S
n : ℕ
k : S
⊢ eval k (descPochhammer S n) * k - eval k (descPochhammer S n * ↑n) = eval k (descPochhammer S n) * (k - ↑n)

Tactic:
← Nat.cast_comm,

Goal state after:
S : Type u_1
inst✝ : Ring S
n : ℕ
k : S
⊢ eval k (descPochhammer S n) * k - eval k (↑n * descPochhammer S n) = eval k (descPochhammer S n) * (k - ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
← Nat.cast_comm,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ eval (-r) (ascPochhammer R k) * -r + eval (-r) (↑k * ascPochhammer R k) =
    (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) =
    (-1) ^ (k + 1) * (eval r (descPochhammer R k) * r - eval r (descPochhammer R k * ↑k))

Tactic:
← Nat.cast_comm,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) =
    (-1) ^ (k + 1) * (eval r (descPochhammer R k) * r - eval r (↑k * descPochhammer R k))
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (basisDivisor x y).degree = 1

Tactic:
by
  rw [basisDivisor, degree_mul, degree_X_sub_C, degree_C, zero_add]
  exact inv_ne_zero (sub_ne_zero_of_ne hxy)

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case e'_3
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
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
⊢ ∑ x ∈ s.erase i, 1 = ∑ i_1 ∈ s.erase i, (basisDivisor (v i) (v i_1)).natDegree

Tactic:
refine sum_congr rfl fun j hj => (natDegree_basisDivisor_of_ne ?_).symm

Goal state after:
case e'_3
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
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
j : ι
hj : j ∈ s.erase i
⊢ v i ≠ v j
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
⊢ (of fun i j ↦ eval (v i) (p j)) = vandermonde v * of fun i j ↦ (p j).coeff ↑i

Tactic:
by
  ext i j
  simp_rw [Matrix.mul_apply, eval, Matrix.of_apply, eval₂_eq_sum]
  simp only [Matrix.vandermonde]
  have : (p j).support ⊆ range n := supp_subset_range <| Nat.lt_of_le_of_lt (h_deg j) <| Fin.prop j
  rw [sum_eq_of_subset _ (fun j => zero_mul ((v i) ^ j)) this, ← Fin.sum_univ_eq_sum_range]
  congr
  ext k
  rw [mul_comm, Matrix.of_apply, RingHom.id_apply]

Goal state after:
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
h_monic : ∀ (i : Fin n), (p i).Monic
⊢ (vandermonde v).det = (of fun i j ↦ eval (v i) (p j)).det

Tactic:
by
  rw [Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials v p (fun i ↦
      Nat.le_of_eq (h_deg i)), Matrix.det_mul,
      Matrix.det_matrixOfPolynomials p h_deg h_monic, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case e'_2
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ eval (↑(v x✝¹)) (descPochhammer ℤ ↑x✝) = ↑(↑x✝).factorial * of (fun i j ↦ ↑((v i).choose ↑j)) x✝¹ x✝

pp: case e'_3.e'_5
n : ℕ
v : Fin n → ℕ
⊢ ↑(∏ i, (↑i).factorial) = ∏ i, ↑(↑i).factorial

Tactic:
· rw [of_apply, descPochhammer_eval_eq_descFactorial ℤ _ _]
    congr
    exact Nat.descFactorial_eq_factorial_mul_choose _ _

Goal state after:
case e'_3.e'_5
n : ℕ
v : Fin n → ℕ
⊢ ↑(∏ i, (↑i).factorial) = ∏ i, ↑(↑i).factorial
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₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
L : LieSubalgebra K (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅K⁆ L₁ := (LieHom.fst K L₁ L₂).comp L.incl
p₂ : ↥L →ₗ⁅K⁆ L₂ := (LieHom.snd K L₁ L₂).comp L.incl
⊢ Injective ⇑p₁

Tactic:
have disj : Disjoint p₁.ker p₂.ker := by
      rw [disjoint_iff, _root_.eq_bot_iff]
      rintro ⟨⟨x, y⟩, -⟩
      simp [p₁, p₂, Subtype.ext_iff]

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₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
L : LieSubalgebra K (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅K⁆ L₁ := (LieHom.fst K L₁ L₂).comp L.incl
p₂ : ↥L →ₗ⁅K⁆ L₂ := (LieHom.snd K L₁ L₂).comp L.incl
disj : Disjoint p₁.ker p₂.ker
⊢ Injective ⇑p₁
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (eval₂Hom (f.comp (algebraMap R (MvPolynomial τ R))) fun i ↦ f (g i)) φ = (eval₂Hom (f.comp C) fun i ↦ f (g i)) φ

Tactic:
algebraMap_eq

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (eval₂Hom (f.comp C) fun i ↦ f (g i)) φ = (eval₂Hom (f.comp C) fun i ↦ f (g i)) φ
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun d ↦ (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i).vars) ⊆
    φ.support.biUnion fun d ↦ d.support.biUnion fun i ↦ (f i).vars

Tactic:
apply Finset.biUnion_mono
    intro d _hd
    calc
      vars (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i) ≤
          (C (coeff d φ)).vars ∪ (∏ i ∈ d.support, f i ^ d i).vars :=
        vars_mul _ _
      _ ≤ (∏ i ∈ d.support, f i ^ d i).vars := by
        simp only [Finset.empty_union, vars_C, Finset.Subset.refl]
      _ ≤ d.support.biUnion fun i : σ => vars (f i ^ d i) := vars_prod _
      _ ≤ d.support.biUnion fun i : σ => (f i).vars := ?_
    apply Finset.biUnion_mono
    intro i _hi
    apply vars_pow

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
⊢ ∏ i ∈ insert i s, (X - C (v i)) = (X - C (v i)) * ∏ i ∈ s, (X - C (v i))

Tactic:
prod_insert hi

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
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, ⋯⟩)
x✝ : I × I
i j : I
⊢ Polynomial.eval (μ i - μ j) r • v.end (i, j) = ⁅y, v.end (i, j)⁆

Tactic:
hr,

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, ⋯⟩)
x✝ : I × I
i j : I
⊢ ((algebraMap ℚ K) (↑f ⟨μ i, ⋯⟩) - (algebraMap ℚ K) (↑f ⟨μ j, ⋯⟩)) • v.end (i, j) = ⁅y, v.end (i, j)⁆
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
j : ι
hjt : j ∈ t
⊢ (X - C (v i)) * nodal (t.erase j) v = nodal (insert i (t.erase j)) v

Tactic:
nodal_insert_eq_nodal (mem_of_mem_erase.mt hit)

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
j : ι
hjt : j ∈ t
⊢ (X - C (v i)) * nodal (t.erase j) v = (X - C (v i)) * nodal (t.erase j) v
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✝² : Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
inst✝ : StrongRankCondition R
⊢ f.charpoly.natDegree = finrank R M

Tactic:
have := nontrivial_of_invariantBasisNumber

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
inst✝ : StrongRankCondition R
this : ∀ (R : Type ?u.32) [inst : Semiring R] [InvariantBasisNumber R], Nontrivial R
⊢ f.charpoly.natDegree = finrank R M
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₂
⊢ (fromBlocks ((toMatrix b₁ b₁) f₁) 0 0 ((toMatrix b₂ b₂) f₂)).charpoly =
    ((toMatrix b₁ b₁) f₁).charpoly * ((toMatrix b₂ b₂) f₂).charpoly

Tactic:
Matrix.charpoly_fromBlocks_zero₁₂

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₂
⊢ ((toMatrix b₁ b₁) f₁).charpoly * ((toMatrix b₂ b₂) 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
w : σ → M
m : M
a b : MvPolynomial σ R
ha : a ∈ {x | IsWeightedHomogeneous w x m}
hb : b ∈ {x | IsWeightedHomogeneous w x m}
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
⊢ coeff c a ≠ 0 ∨ coeff c b ≠ 0

Tactic:
contrapose! hc

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
a b : MvPolynomial σ R
ha : a ∈ {x | IsWeightedHomogeneous w x m}
hb : b ∈ {x | IsWeightedHomogeneous w x m}
c : σ →₀ ℕ
hc : coeff c a = 0 ∧ coeff c b = 0
⊢ coeff c a + coeff c b = 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
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x ∈ antidiagonal c, coeff x.1 φ * coeff x.2 ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
⊢ (weight w) ((d, e).1 + (d, e).2) = (weight w) d + n

Tactic:
← hψ aux.2,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x ∈ antidiagonal c, coeff x.1 φ * coeff x.2 ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
⊢ (weight w) ((d, e).1 + (d, e).2) = (weight w) d + (weight w) e
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 : ι
r : A
hr : r ∈ span s
⊢ ↑(((decompose 𝒜) r) i) ∈ span s

Tactic:
Ideal.span,

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 : ι
r : A
hr : r ∈ Submodule.span A s
⊢ ↑(((decompose 𝒜) r) 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 𝒜
i : ι
r : A
hr : r = 0
⊢ ↑(((decompose 𝒜) r) i) ∈ ⊥

Tactic:
hr,

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 : ι
r : A
hr : r = 0
⊢ ↑(((decompose 𝒜) 0) i) ∈ ⊥