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

Goal state before:
pp: case refine_1
ι : 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
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ ∀ x ∈ ⇑P.root '' ↑b.support, ∃ f, Function.support f ⊆ ↑b.support ∧ x = ∑ j ∈ b.support, f j • P.root j

pp: case refine_2
ι : 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
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ ∀ (x y : M),
    x ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
      y ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
        (∃ f, Function.support f ⊆ ↑b.support ∧ x = ∑ j ∈ b.support, f j • P.root j) →
          (∃ f, Function.support f ⊆ ↑b.support ∧ y = ∑ j ∈ b.support, f j • P.root j) →
            ∃ f, Function.support f ⊆ ↑b.support ∧ x + y = ∑ j ∈ b.support, f j • P.root j

Tactic:
· rintro - ⟨j, hj, rfl⟩
    exact ⟨Pi.single j 1, by simpa, by aesop (add simp Pi.single_apply)⟩

Goal state after:
case refine_2
ι : 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
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ ∀ (x y : M),
    x ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
      y ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
        (∃ f, Function.support f ⊆ ↑b.support ∧ x = ∑ j ∈ b.support, f j • P.root j) →
          (∃ f, Function.support f ⊆ ↑b.support ∧ y = ∑ j ∈ b.support, f j • P.root j) →
            ∃ f, Function.support f ⊆ ↑b.support ∧ x + y = ∑ j ∈ b.support, f 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
i : ι
hi : i ∈ b.support
⊢ b.height i = 1

Tactic:
by
  classical
  have : P.root i = ∑ j ∈ b.support, (Pi.single i 1 : ι → ℤ) j • P.root j := by
    rw [Finset.sum_eq_single_of_mem i hi (by simp_all)]; simp
  simpa [height_eq_sum this]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : ∑ x, (u * ↑(a x) + v * ↑(b x)) • ↑x = ∑ x, Pi.single ri 1 x • ↑x
aux : P.root i = ∑ x, Pi.single ri 1 x • ↑x
hli : LinearIndependent ℚ Subtype.val
⊢ u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1

Tactic:
exact linearIndependent_iff_injective_fintypeLinearCombination.mp hli huv

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

Goal state before:
pp: case succ
ι : 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
hij : LinearIndependent R ![P.root j, P.root i]
l : ι
hl : P.root l = P.root i + ↑w • P.root j
hk : P.root k = P.root l + P.root j
⊢ b.IsPos k

Tactic:
exact (hw hi hl hij).add (b.isPos_of_mem_support hj) hk

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 : ℕ
ha : IsUnit A.det
h : n ≤ m
⊢ A ^ (m - n + n - n) = A ^ (m - n) * (A ^ n * (A ^ n)⁻¹)

Tactic:
mul_nonsing_inv,

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

case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
ha : IsUnit A.det
h : n ≤ m
⊢ IsUnit (A ^ n).det
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: l✝ : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m l✝ R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l✝), Commute (A i j) x
k : p
l : l✝
⊢ ∑ x, ∑ x_1, X.vec (x, x_1) * (B x k * A x_1 l) = ∑ x, ∑ i, A i l * X i x * B x k

Tactic:
(hA ..).eq,

Goal state after:
l✝ : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m l✝ R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l✝), Commute (A i j) x
k : p
l : l✝
⊢ ∑ x, ∑ x_1, X.vec (x, x_1) * (B x k * A x_1 l) = ∑ x, ∑ x_1, X x_1 x * A x_1 l * B x k
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
μ : R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
i : n
⊢ b i ∈ ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ

Tactic:
apply Submodule.mem_iSup_of_mem (d i)

Goal state after:
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)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
i : n
⊢ b i ∈ ⨆ (_ : d i ∈ Set.range d), eigenspace ((toLin b b) (diagonal d)) (d i)
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
n : ℕ
⊢ A ^ (-(↑n + 1) + 1) = (A ^ n)⁻¹

Tactic:
by
        rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_natCast]

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
α : Type u_5
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : StarRing α
inst✝³ : StarOrderedRing α
inst✝² : Algebra α R
inst✝¹ : StarModule α R
inst✝ : PosSMulStrictMono α R
x : Matrix n n R
hx : x.PosDef
a : α
ha : 0 < a
⊢ (a • x).PosDef

Tactic:
refine ⟨IsSelfAdjoint.smul (IsSelfAdjoint.of_nonneg ha.le) hx.1, fun y hy => ?_⟩
  simpa [← Finsupp.smul_sum] using smul_pos ha (hx.2 hy)

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

Goal state before:
pp: case refine_3
n : Type u_2
inst✝⁷ : Fintype n
R : Type u_5
M : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : TrivialStar R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq n
b : Module.Basis n R M
B : LinearMap.BilinForm R M
hB_symm : B.IsSymm
aux : ∀ (i j : n) (s t : R), t * (B (b i)) (b j) * s = t * (s * (B (b j)) (b i))
h : ((LinearMap.BilinForm.toMatrix b) B).PosDef
v : M
hv : v ≠ 0
⊢ 0 < (LinearMap.BilinMap.toQuadraticMap B) v

Tactic:
rw [B.toQuadraticMap_apply, ← b.linearCombination_repr (x := v)]

Goal state after:
case refine_3
n : Type u_2
inst✝⁷ : Fintype n
R : Type u_5
M : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : TrivialStar R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq n
b : Module.Basis n R M
B : LinearMap.BilinForm R M
hB_symm : B.IsSymm
aux : ∀ (i j : n) (s t : R), t * (B (b i)) (b j) * s = t * (s * (B (b j)) (b i))
h : ((LinearMap.BilinForm.toMatrix b) B).PosDef
v : M
hv : v ≠ 0
⊢ 0 < (B ((Finsupp.linearCombination R ⇑b) (b.repr v))) ((Finsupp.linearCombination R ⇑b) (b.repr v))
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
⊢ (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef

Tactic:
by
  have := Fintype.ofFinite n
  rw [posSemidef_iff_dotProduct_mulVec, IsHermitian.fromBlocks₁₁ _ _ hA.1]
  constructor
  · refine fun h => .of_dotProduct_mulVec_nonneg h.1 fun x => ?_
    have := h.2 (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)
    rwa [dotProduct_mulVec, schur_complement_eq₁₁ B D _ _ hA.1, neg_add_cancel, dotProduct_zero,
      zero_add, ← dotProduct_mulVec] at this
  · refine fun h => ⟨h.1, fun x => ?_⟩
    rw [dotProduct_mulVec, ← Sum.elim_comp_inl_inr x, schur_complement_eq₁₁ B D _ _ hA.1]
    apply le_add_of_nonneg_of_le
    · rw [← dotProduct_mulVec]
      apply (posSemidef_iff_dotProduct_mulVec.mp hA.posSemidef).2
    · rw [← dotProduct_mulVec (star (x ∘ Sum.inr))]
      apply (posSemidef_iff_dotProduct_mulVec.mp h).2

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

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

Tactic:
eval_natCast,

Goal state after:
n t : ℕ
⊢ n.ascFactorial t * (n + ↑t) = n.ascFactorial (t + 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

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:
· 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⟩

Goal state after:
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
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₂
h₁ :
  ↑(LieSubalgebra.map (prod eι b₁ b₂).incl (prodCartan eι b₁ b₂)) =
    ↑(lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})
h₂ :
  (lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}).toSubmodule = span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}
⊢ Submodule.map (LinearMap.fst R L₁ L₂) (span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}) = span R (Set.range b₁.h)

Tactic:
by
    rw [Submodule.map_span]; congr; ext; simp

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₂
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✝ : Nontrivial L₂
this✝³ : Fintype ι₁
this✝² : Fintype ι₂
this✝¹ : H₁.IsCartanSubalgebra
this✝ : H₂.IsCartanSubalgebra
this : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
x : ↥H₁ × ↥H₂
hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂
⊢ ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂

Tactic:
rw [← mem_toLieSubmodule, ← rootSpace_zero_eq, LieModule.mem_genWeightSpace]

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✝ : Nontrivial L₂
this✝³ : Fintype ι₁
this✝² : Fintype ι₂
this✝¹ : H₁.IsCartanSubalgebra
this✝ : H₂.IsCartanSubalgebra
this : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
x : ↥H₁ × ↥H₂
hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂
⊢ ∀ (x_1 : ↥(prodCartan eι b₁ b₂)),
    ∃ k, (((LieModule.toEnd K ↥(prodCartan eι b₁ b₂) ↥(prod eι b₁ b₂)) x_1 - 0 x_1 • 1) ^ k) ⟨(↑x.1, ↑x.2), hx⟩ = 0
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
⊢ (engel R x).normalizer = engel R x

Tactic:
apply le_antisymm _ (le_normalizer _)

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ (engel R x).normalizer ≤ engel R x
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ((bind₁ f) φ).vars = (∑ x ∈ φ.support, (bind₁ f) ((monomial x) (coeff x φ))).vars

Tactic:
rw [← map_sum, ← φ.as_sum]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
A : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ (φ (P * A * Q)).charpoly = (φ₁ P * φ₂ A * φ₃ Q).charpoly

Tactic:
reindexLinearEquiv_mul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
A : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ (φ (P * A * Q)).charpoly = ((reindexLinearEquiv R R e (Equiv.refl ι')) (P * A) * φ₃ Q).charpoly
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ∀ i ∈ (↑G).toFinset, eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)

Tactic:
· intro i hi
    rw [eval_nodal_at_node hi]
    replace hi : i ∈ G := by simpa using hi
    obtain ⟨g, rfl⟩ : ∃ g : G, g.val = i := ⟨⟨i, hi⟩, rfl⟩
    simp [← Units.val_pow_eq_pow_val, ← Subgroup.coe_pow G]

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
hy_range : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
hny_comm : Commute n y
htr_n : (trace K M) (n * y) = 0
⊢ (trace K M) (s * y) = ∑ i, fμ i * μ i

Tactic:
rw [trace_eq_matrix_trace _ v, Matrix.trace]

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
hy_range : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
hny_comm : Commute n y
htr_n : (trace K M) (n * y) = 0
⊢ ∑ i, ((toMatrix v v) (s * y)).diag i = ∑ i, fμ i * μ i
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ weightedTotalDegree (fun i ↦ {i}) p = p.degrees

Tactic:
rw [degrees_def]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ weightedTotalDegree (fun i ↦ {i}) p = p.support.sup fun s ↦ toMultiset s
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_1.succ
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
ih : homogeneousSubmodule σ R 1 ^ n ≤ homogeneousSubmodule σ R n
⊢ homogeneousSubmodule σ R 1 ^ (n + 1) ≤ homogeneousSubmodule σ R (n + 1)

Tactic:
grw [pow_add, pow_one, ih]

Goal state after:
case refine_1.succ
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
ih : homogeneousSubmodule σ R 1 ^ n ≤ homogeneousSubmodule σ R n
⊢ homogeneousSubmodule σ R n * homogeneousSubmodule σ R 1 ≤ homogeneousSubmodule σ R (n + 1)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case convert_6
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ φ.coeff.support
k : σ
⊢ ((fun n e ↦ g n ^ e) k (i k)).IsHomogeneous (n * i k)

Tactic:
apply (hg k).pow

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

Goal state before:
pp: R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
⊢ ∃ i, ((finSuccEquiv R N) F).coeff i ≠ 0

Tactic:
contrapose! hF₀

Goal state after:
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
hF₀ : ∀ (i : ℕ), ((finSuccEquiv R N) F).coeff i = 0
⊢ F = 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
μ : K
k : ℕ
⊢ finrank K ↥((φ.genEigenspace μ) ↑k) ≤ rootMultiplicity μ (charpoly φ)

Tactic:
grw [Submodule.finrank_mono (φ.genEigenspace_le_maximal μ k), finrank_maxGenEigenspace_eq]

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ derivedSeries R L 1
⊢ χ x = 0

Tactic:
derivedSeries_def,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ derivedSeriesOfIdeal R L 1 ⊤
⊢ χ x = 0
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)
⊢ φ.nilRank + (n - φ.nilRank) = finrank R M

Tactic:
simp [n, nilRank_le_card φ bₘ, finrank_eq_card_chooseBasisIndex]

Goal state after: