mathlib-initiative/mathlib-tactics huggingface dataset:
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✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
⊢ maxGenEigenspace ((toLin b b) (diagonal d)) μ = eigenspace ((toLin b b) (diagonal d)) μ

Tactic:
by
  refine le_antisymm (fun x hx ↦ ?_) eigenspace_le_maxGenEigenspace
  obtain ⟨k, hk⟩ := (mem_maxGenEigenspace _ _ _).mp hx
  replace hk (j : n) : b.repr x j = 0 ∨ d j = μ ∧ k ≠ 0 := by
    have aux : (diagonal d).toLin b b - μ • 1 = (diagonal (d - μ • 1)).toLin b b := by
      rw [Pi.sub_def, ← diagonal_sub]; simp [one_eq_id]
    rw [aux, ← toLin_pow, diagonal_pow, toLin_apply_eq_zero_iff] at hk
    simpa [mulVec_eq_sum, diagonal_apply, sub_eq_zero] using hk j
  have aux (j : n) : (b.repr x j * d j) • b j = μ • (b.repr x j • b j) := by
    rcases hk j with hj | hj
    · simp [hj]
    · rw [← hj.1, mul_comm, mul_smul]
  simp [toLin_apply, mulVec_eq_sum, diagonal_apply, aux, ← Finset.smul_sum]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix n m R
⊢ (Bᴴ * A * B).PosSemidef

Tactic:
have := Fintype.ofFinite m

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix n m R
this : Fintype m
⊢ (Bᴴ * A * B).PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
i j : ι
⊢ 0 ≤ N i j

Tactic:
specialize hμ i j

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
i j : ι
hμ : A i j ≤ if i = j then μ else 0
⊢ 0 ≤ N i j
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
inst✝² : IsDomain R
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
⊢ b.cartanMatrix.map abs = 4 - b.cartanMatrix

Tactic:
by
  ext; simp [abs_cartanMatrix_apply, Matrix.ofNat_apply]

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
χ : ↥root
this : H.IsCartanSubalgebra := isCartanSubalgebra b
n : ι → ℕ
⊢ ∑ i, n i • b.baseSupp i ∈ (Submodule.span ℕ (⇑(rootSystem H).root '' range b.baseSupp')).toAddSubmonoid

Tactic:
Submodule.mem_toAddSubmonoid

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
χ : ↥root
this : H.IsCartanSubalgebra := isCartanSubalgebra b
n : ι → ℕ
⊢ ∑ i, n i • b.baseSupp i ∈ Submodule.span ℕ (⇑(rootSystem H).root '' range b.baseSupp')
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
h : n ≠ 0
⊢ eval 0 (descPochhammer R n) = 0

Tactic:
simp [descPochhammer_eval_zero, h]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
⊢ rectVandermonde v w (n + 1) i = Pi.single (last n) (v i ^ n)

Tactic:
ext j

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
j : Fin (n + 1)
⊢ rectVandermonde v w (n + 1) i j = Pi.single (last n) (v i ^ n) j
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
⊢ projVandermonde v w i = Pi.single (last n) (v i ^ n)

Tactic:
ext j

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
j : Fin (n + 1)
⊢ projVandermonde v w i j = Pi.single (last n) (v i ^ n) j
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#s)
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 0

Tactic:
← card_image_of_injOn hvs

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#(image v s))
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x : F
⊢ (basisDivisor x x).natDegree = 0

Tactic:
by
  rw [basisDivisor_self, natDegree_zero]

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

Goal state before:
pp: ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq : ⟨a i, ⋯⟩ - ⟨a j, ⋯⟩ = ⟨a k, ⋯⟩ - ⟨a l, ⋯⟩
⊢ (algebraMap R K) (f ⟨a (i, j).1, ⋯⟩) - (algebraMap R K) (f ⟨a (i, j).2, ⋯⟩) =
    (algebraMap R K) (f ⟨a (k, l).1, ⋯⟩) - (algebraMap R K) (f ⟨a (k, l).2, ⋯⟩)

Tactic:
← (algebraMap R K).map_sub,

Goal state after:
ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq : ⟨a i, ⋯⟩ - ⟨a j, ⋯⟩ = ⟨a k, ⋯⟩ - ⟨a l, ⋯⟩
⊢ (algebraMap R K) (f ⟨a (i, j).1, ⋯⟩ - f ⟨a (i, j).2, ⋯⟩) =
    (algebraMap R K) (f ⟨a (k, l).1, ⋯⟩) - (algebraMap R K) (f ⟨a (k, l).2, ⋯⟩)
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq : ⟨a i, ⋯⟩ - ⟨a j, ⋯⟩ = ⟨a k, ⋯⟩ - ⟨a l, ⋯⟩
⊢ (algebraMap R K) (f ⟨a (i, j).1, ⋯⟩ - f ⟨a (i, j).2, ⋯⟩) =
    (algebraMap R K) (f ⟨a (k, l).1, ⋯⟩) - (algebraMap R K) (f ⟨a (k, l).2, ⋯⟩)

Tactic:
← (algebraMap R K).map_sub,

Goal state after:
ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq : ⟨a i, ⋯⟩ - ⟨a j, ⋯⟩ = ⟨a k, ⋯⟩ - ⟨a l, ⋯⟩
⊢ (algebraMap R K) (f ⟨a (i, j).1, ⋯⟩ - f ⟨a (i, j).2, ⋯⟩) = (algebraMap R K) (f ⟨a (k, l).1, ⋯⟩ - f ⟨a (k, l).2, ⋯⟩)
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
⊢ ∑ b ∈ s, (⇑derivative)^[k] (C (r b / ∏ j ∈ s.erase b, (v b - v j)) * ∏ j ∈ s.erase b, (X - C (v j))) =
    ↑k.factorial *
      ∑ i ∈ s,
        C (r i / ∏ j ∈ s.erase i, (v i - v j)) * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ j ∈ t, (X - C (v j))

Tactic:
iterate_derivative_C_mul,

Goal state after:
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
⊢ ∑ x ∈ s, C (r x / ∏ j ∈ s.erase x, (v x - v j)) * (⇑derivative)^[k] (∏ j ∈ s.erase x, (X - C (v j))) =
    ↑k.factorial *
      ∑ i ∈ s,
        C (r i / ∏ j ∈ s.erase i, (v i - v j)) * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ j ∈ t, (X - C (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₂
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
I₁ : LieIdeal K L₂ := LieIdeal.map p₂ p₁.ker
⊢ I₁ ≠ ⊤

Tactic:
have : Nontrivial L₂ := IsSimple.nontrivial K L₂

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
I₁ : LieIdeal K L₂ := LieIdeal.map p₂ p₁.ker
this : Nontrivial L₂
⊢ I₁ ≠ ⊤
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ↑(Fintype.card ↑↑G) = ↑(Fintype.card ↥G)

Tactic:
Nat.cast_inj

Goal state after:
case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ Fintype.card ↑↑G = Fintype.card ↥G
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
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : p ≠ 0
⊢ weightedTotalDegree' w p = ↑(weightedTotalDegree w p)

Tactic:
rw [Ne, ← weightedTotalDegree'_eq_bot_iff w p, ← Ne, WithBot.ne_bot_iff_exists] at hp
  obtain ⟨m, hm⟩ := hp
  apply le_antisymm
  · simp only [weightedTotalDegree, weightedTotalDegree', Finset.sup_le_iff, WithBot.coe_le_coe]
    intro b
    exact Finset.le_sup
  · simp only [weightedTotalDegree]
    have hm' : weightedTotalDegree' w p ≤ m := le_of_eq hm.symm
    rw [← hm]
    simpa [weightedTotalDegree'] using hm'

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

Goal state before:
pp: case pos
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : i = 0
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) i)) 0) = 0

Tactic:
rw [h, hr, decompose_zero, zero_apply, ZeroMemClass.coe_zero]

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

Goal state before:
pp: case h.inr
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : d ≠ 0
⊢ coeff d (((finSuccEquiv R N) F).coeff n) = 0

Tactic:
contrapose! hd
    ext i
    rw [Finsupp.coe_zero, Pi.zero_apply]
    by_cases hi : i ∈ d.support
    · have := hF.finSuccEquiv_coeff_isHomogeneous n 0 (add_zero _) hd
      simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum] at this
      rw [Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ zero_le)] at this
      exact this i hi
    · simpa using hi

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst✝¹ : Fintype ιM'
inst✝ : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom
⊢ Function.Injective f

Tactic:
simp only [f, aeval_X_left, AlgHom.toRingHom_eq_coe, AlgHom.id_toRingHom]

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst✝¹ : Fintype ιM'
inst✝ : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom
⊢ Function.Injective (Polynomial.map (RingHom.id (MvPolynomial ι R)))
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ ¬(φ.polyCharpoly b').coeff (φ.nilRankAux b') = 0

Tactic:
apply polyCharpoly_coeff_nilRankAux_ne_zero

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
b : Basis ι R L
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : Nontrivial R
⊢ (φ.polyCharpoly b).coeff (φ.polyCharpoly b).natTrailingDegree ≠ 0

Tactic:
apply polyCharpoly_coeff_nilRankAux_ne_zero

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Semiring K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : AddCommMonoid V'
inst✝² : Module K V'
inst✝¹ : AddCommMonoid V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ lift.{v', v''} (f ∘ₗ g).rank ≤ lift.{v'', v'} g.rank

Tactic:
rw [rank, rank, LinearMap.range_comp]

Goal state after:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Semiring K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : AddCommMonoid V'
inst✝² : Module K V'
inst✝¹ : AddCommMonoid V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ lift.{v', v''} (Module.rank K ↥(Submodule.map f g.range)) ≤ lift.{v'', v'} (Module.rank K ↥g.range)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
a✝ : Nontrivial R
⊢ B * A.det • 1 = A.det • B

Tactic:
Matrix.mul_smul,

Goal state after:
m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
a✝ : Nontrivial R
⊢ A.det • (B * 1) = A.det • B
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
⊢ ∃ V U e, IsUnit V ∧ IsUnit U ∧ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e

Tactic:
have hUdet : IsUnit U.det := (isUnit_iff_isUnit_det _).1 <| isUnit_prod_comp_inverse _

Goal state after:
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
⊢ ∃ V U e, IsUnit V ∧ IsUnit U ∧ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⋯
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⋯
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L := ⋯
hx₀ : x ≠ 0
Q : Type u_2 := ⋯
r : ℕ := ⋯
hr : r < finrank K L
x' : ↥U := ⋯
y' : ↥U := ⋯
u : ↥U := ⋯
χ : K[X][X] := ⋯
ψ : K[X][X] := ⋯
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
⊢ ∀ i_1 ∈ s, eval i_1 (χ.coeff i) = 0

pp: case hcard
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
⊢ (χ.coeff i).natDegree < s.card

Tactic:
case hcard =>
    -- We need to show that `natDegree (coeff χ i) < s.card`
    -- Which follows from our assumptions `i < r` and `r ≤ s.card`
    -- and the fact that the degree of `coeff χ i` is less than or equal to `r - i`.
    apply lt_of_le_of_lt (lieCharpoly_coeff_natDegree _ _ _ _ i (r - i) _)
    · omega
    · dsimp only [r] at hi ⊢
      rw [Nat.add_sub_cancel' hi.le]

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⋯
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⋯
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L := ⋯
hx₀ : x ≠ 0
Q : Type u_2 := ⋯
r : ℕ := ⋯
hr : r < finrank K L
x' : ↥U := ⋯
y' : ↥U := ⋯
u : ↥U := ⋯
χ : K[X][X] := ⋯
ψ : K[X][X] := ⋯
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
⊢ ∀ i_1 ∈ s, eval i_1 (χ.coeff i) = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: l : Type ul
m : Type um
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ A.rank + B.rank ≤ Fintype.card m

Tactic:
rw [Matrix.rank_eq_finrank_range_toLin A el em,
      Matrix.rank_eq_finrank_range_toLin B em en,
      ← Module.finrank_fintype_fun_eq_card R,
      ← LinearMap.finrank_range_add_finrank_ker (Matrix.toLin em el A),
      add_le_add_iff_left]

Goal state after:
l : Type ul
m : Type um
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ finrank R ↥((toLin en em) B).range ≤ finrank R ↥((toLin em el) A).ker
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: case mp
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
h : (d₂₃ R L M) a = 0
x y z : L
this : -(a ⁅x, y⁆) z + (a ⁅x, z⁆) y - (a ⁅y, z⁆) x = 0
⊢ (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆

Tactic:
rw [sub_eq_zero] at this

Goal state after:
case mp
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
h : (d₂₃ R L M) a = 0
x y z : L
this : -(a ⁅x, y⁆) z + (a ⁅x, z⁆) y = (a ⁅y, z⁆) x
⊢ (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ x✝ : Derivation R A A
⊢ { toFun := ⇑(LinearMap.rTensor L ↑(x✝¹ + x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } =
    { toFun := ⇑(LinearMap.rTensor L ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } +
      { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ : R
x✝ : Derivation R A A
⊢ { toFun := ⇑(LinearMap.rTensor L ↑(x✝¹ • x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } =
    (RingHom.id R) x✝¹ • { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }

Tactic:
by ext; simp

Goal state after: