mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ eval (v i) (Lagrange.basis s v i) = 1

Tactic:
rw [Lagrange.basis, eval_prod]
  refine prod_eq_one fun j H => ?_
  rw [eval_basisDivisor_left_of_ne]
  rcases mem_erase.mp H with ⟨hij, hj⟩
  exact mt (hvs hi hj) hij.symm

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case inl
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v r : ι → F
hvs : Set.InjOn v ↑∅
⊢ ((interpolate ∅ v) r).degree < ↑(#∅)

pp: case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ ((interpolate s v) r).degree < ↑(#s)

Tactic:
· rw [interpolate_empty, degree_zero, card_empty]
    exact WithBot.bot_lt_coe _

Goal state after:
case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ ((interpolate s v) r).degree < ↑(#s)
Module: Mathlib.LinearAlgebra.Vandermonde

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

Tactic:
← Fin.sum_univ_eq_sum_range

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
⊢ ∑ i_1, (RingHom.id R) ((p j).coeff ↑i_1) * v i ^ ↑i_1 = ∑ j_1, of (fun i j ↦ v i ^ ↑j) i j_1 * (p j).coeff ↑j_1
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:
rw [← (algebraMap R K).map_sub, ← (algebraMap R K).map_sub, ← map_sub, ← map_sub, heq]

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 ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate s v) r =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

Tactic:
rw [interpolate_eq_sum_interpolate_insert_sdiff _ hvs ⟨i, mem_insert_self i {j}⟩ _,
    sum_insert (notMem_singleton.mpr hij), sum_singleton, basis_pair_left hij,
    basis_pair_right hij, sdiff_insert_insert_of_mem_of_notMem hi (notMem_singleton.mpr hij),
    sdiff_singleton_eq_erase, pair_comm,
    sdiff_insert_insert_of_mem_of_notMem hj (notMem_singleton.mpr hij.symm),
    sdiff_singleton_eq_erase]
  exact insert_subset_iff.mpr ⟨hi, singleton_subset_iff.mpr hj⟩

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
N : LieSubalgebra R L := H.normalizer
⊢ (engel R x).toSubmodule ⊔ H.toSubmodule = H.toSubmodule

Tactic:
rwa [sup_eq_right]

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 r : ι → F
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v ↑(s.erase i)
⊢ (⇑derivative)^[k] (∏ j ∈ s.erase i, (X - C (v j))) = (⇑derivative)^[k] (∏ vj ∈ image v (s.erase i), (X - C vj))

Tactic:
by rw [Finset.prod_image hvs']

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
⊢ ((toMatrix b b) f).charpoly = ((toMatrix (chooseBasis R M) (chooseBasis R M)) f).charpoly

Tactic:
set b' := chooseBasis R M

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
⊢ ((toMatrix b b) f).charpoly = ((toMatrix b' b') f).charpoly
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

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

Tactic:
← charpoly_toMatrix f₁ b₁,

Goal state after:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R (M₁ × M₂) := b₁.prod b₂
⊢ (f₁.prodMap f₂).charpoly = ((toMatrix b₁ b₁) f₁).charpoly * f₂.charpoly
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
⊢ ∃ y, (trace K M) (φ x * y) = 0 ∧ (trace K M) (φ x * y) = ∑ i, fμ i * μ i

Tactic:
have hny_comm : Commute n y := by
    suffices y ∈ K[s] from commute_of_mem_adjoin_singleton_of_commute this hns
    rw [adjoin_singleton_eq_range_aeval]
    obtain ⟨q, hq⟩ : ∃ q : K[X], ∀ i, q.eval (μ i) = fμ i :=
      (Polynomial.exists_eval_eq_iff μ fμ).mpr <| by aesop
    refine ⟨q, v.ext fun i ↦ ?_⟩
    rw [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, aeval_apply_of_mem_apply_eq_smul (hsv i), hq, hyv]

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
⊢ ∃ y, (trace K M) (φ x * y) = 0 ∧ (trace K M) (φ x * y) = ∑ i, fμ i * μ i
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
⊢ weightedHomogeneousSubmodule R w m = AddMonoidAlgebra.supported R R {d | (weight w) d = m}

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
x : MvPolynomial σ R
⊢ x ∈ weightedHomogeneousSubmodule R w m ↔ x ∈ AddMonoidAlgebra.supported R R {d | (weight w) d = m}
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
x : MvPolynomial σ R
⊢ x ∈ weightedHomogeneousSubmodule R w m ↔ x ∈ AddMonoidAlgebra.supported R R {d | (weight w) d = m}

Tactic:
simp [IsWeightedHomogeneous]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
x : MvPolynomial σ R
⊢ (∀ ⦃d : σ →₀ ℕ⦄, ¬coeff d x = 0 → (weight w) d = m) ↔ x ∈ AddMonoidAlgebra.supported R R {d | (weight w) d = m}
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
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
⊢ IsWeightedHomogeneous w ((monomial d) r) m

Tactic:
intro c hc

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
c : σ →₀ ℕ
hc : coeff c ((monomial d) r) ≠ 0
⊢ (weight w) c = m
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)), _root_.IsNilpotent ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)) x)
x : L
hx : x ∈ derivedSeries R L 1
hx_ext : 1 ⊗ₜ[R] x ∈ derivedSeries A (A ⊗[R] L) 1
hbc_inj : Injective ⇑(End.baseChangeHom R A M)
aux : (End.baseChangeHom R A M) ((toEnd R (↥(derivedSeries R L 1)) M) ⟨x, hx⟩) = baseChange A ((toEnd R L M) x)
⊢ _root_.IsNilpotent (baseChange A ((toEnd R L M) x))

Tactic:
← toEnd_baseChange

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)), _root_.IsNilpotent ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)) x)
x : L
hx : x ∈ derivedSeries R L 1
hx_ext : 1 ⊗ₜ[R] x ∈ derivedSeries A (A ⊗[R] L) 1
hbc_inj : Injective ⇑(End.baseChangeHom R A M)
aux : (End.baseChangeHom R A M) ((toEnd R (↥(derivedSeries R L 1)) M) ⟨x, hx⟩) = baseChange A ((toEnd R L M) x)
⊢ _root_.IsNilpotent ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x))
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case e'_3
ι : 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 : Ideal A
coe_mono : Monotone toIdeal
⊢ {J | IsHomogeneous 𝒜 J ∧ J ≤ I} = toIdeal '' {b | b.toIdeal ≤ I}

Tactic:
ext x

Goal state after:
case e'_3
ι : 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 : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ x ∈ {J | IsHomogeneous 𝒜 J ∧ J ≤ I} ↔ x ∈ toIdeal '' {b | b.toIdeal ≤ I}
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 : Ideal A
r : A
hr : r ∈ I
⊢ r ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 r]
  refine Ideal.sum_mem _ ?_
  intro j _
  apply Ideal.subset_span
  use j
  use ⟨r, hr⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
⊢ HasFiniteSupport fun m ↦ (weightedHomogeneousComponent w m) φ

Tactic:
apply ((fun d : σ →₀ ℕ => (weight w) d) '' (φ.support : Set (σ →₀ ℕ))).toFinite.subset

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
⊢ (Function.support fun m ↦ (weightedHomogeneousComponent w m) φ) ⊆ (fun d ↦ (weight w) d) '' ↑φ.support
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
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
⊢ (weightedHomogeneousComponent w m) p = p

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w m) p) = coeff x p
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
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
⊢ (weightedHomogeneousComponent w n) p = 0

Tactic:
ext x

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
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w n) p) = coeff x 0
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
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ n ≤ φ.totalDegree

Tactic:
simp only [← hφ hd, MvPolynomial.totalDegree, Finsupp.sum]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) d ≤ φ.support.sup fun s ↦ ∑ x ∈ s.support, s x
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: case h
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
x✝ : ∀ (m : M), ∃ n, (φ ^ n) m = 0
h : ∀ (m : M), ∃ n, (φ ^ n) m = 0 := x✝
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → ⨆ m, (φ ^ m).ker = (φ ^ b).ker
⊢ φ ^ n = 0

Tactic:
ext x

Goal state after:
case h
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
x✝ : ∀ (m : M), ∃ n, (φ ^ n) m = 0
h : ∀ (m : M), ∃ n, (φ ^ n) m = 0 := x✝
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → ⨆ m, (φ ^ m).ker = (φ ^ b).ker
x : M
⊢ (φ ^ n) x = 0 x
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
⊢ (M.toMvPolynomial i).totalDegree ≤ 1

Tactic:
by
  apply (toMvPolynomial_isHomogeneous _ _).totalDegree_le

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
⊢ (weightedHomogeneousComponent w m) p = if m = n then p else 0

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w m) p) = coeff x (if m = n then p else 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
n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p n
⊢ (weightedHomogeneousComponent w n) p = p

Tactic:
classical 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
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
⊢ ∀ x ∈ W, φ x ∈ W

Tactic:
simp only [W, Submodule.mem_iInf, mem_range]

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
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
⊢ ∀ (x : M), (∀ (i : ℕ), ∃ y, (φ ^ i) y = x) → ∀ (i : ℕ), ∃ y, (φ ^ i) y = φ x
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
hnR : ↑n ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
hF : ((rename f) 0).IsHomogeneous n
h : (rename f) 0 ≠ 0
⊢ False

Tactic:
simp at h

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
μ : K
⊢ finrank K ↥((φ - μ • 1).maxGenEigenspace 0) = rootMultiplicity μ (charpoly φ)

Tactic:
finrank_maxGenEigenspace_zero_eq,

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
μ : K
⊢ (charpoly (φ - μ • 1)).natTrailingDegree = rootMultiplicity μ (charpoly φ)
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✝ : Nontrivial R
x : L
h : (charpoly (φ x)).coeff (charpoly (φ x)).natTrailingDegree = 0
⊢ False

Tactic:
apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr _ h

Goal state after:
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✝ : Nontrivial R
x : L
h : (charpoly (φ x)).coeff (charpoly (φ x)).natTrailingDegree = 0
⊢ charpoly (φ x) ≠ 0
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case inl.inl
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
by_cases h : x = y <;>
    simp [Pso, indefiniteDiagonal, h, one_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ IsUnit A.det

Tactic:
isUnit_iff_exists_inv

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ ∃ b, A.det * b = 1
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝⁵ : DecidableEq l
inst✝⁴ : Fintype l
inst✝³ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
F : Type u_3
S : Type u_4
inst✝² : CommRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
hA : A ∈ symplecticGroup l R
f : F
⊢ A.map ⇑f * J l S * Aᵀ.map ⇑f = J l S

Tactic:
← map_J _ f,

Goal state after:
l : Type u_1
R : Type u_2
inst✝⁵ : DecidableEq l
inst✝⁴ : Fintype l
inst✝³ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
F : Type u_3
S : Type u_4
inst✝² : CommRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
hA : A ∈ symplecticGroup l R
f : F
⊢ A.map ⇑f * (J l R).map ⇑f * Aᵀ.map ⇑f = (J l R).map ⇑f
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
⊢ span R ((fun a ↦ f (of.symm Aᵀ a)) '' Set.univ) = span R ((fun a ↦ of.symm (A.submatrix r id)ᵀ a) '' Set.univ)

Tactic:
transpose_submatrix

Goal state after:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
⊢ span R ((fun a ↦ f (of.symm Aᵀ a)) '' Set.univ) = span R ((fun a ↦ of.symm (Aᵀ.submatrix id r) a) '' Set.univ)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : Subsingleton R
A : Matrix m n R
⊢ A.eRank = 1

Tactic:
by
  simp [eRank]

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

Goal state before:
pp: R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ eRank 0 = 0

Tactic:
by
  simp [eRank]

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

Goal state before:
pp: m : Type um
n₀ : Type un₀
R : Type uR
m₀ : Type um
n : Type un
inst✝ : Semiring R
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ (A.submatrix ⇑em ⇑en).cRank = A.cRank

Tactic:
by
  simpa [-lift_cRank_submatrix] using A.lift_cRank_submatrix em en

Goal state after: