mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : I₁ = ⊥
⊢ Injective ⇑p₁

Tactic:
rw [LieIdeal.map_eq_bot_iff] at this

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 : p₁.ker ≤ p₂.ker
⊢ Injective ⇑p₁
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case h
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 := ⋯
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := ⋯
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
y : ↥N
hy : y ∈ (dx ^ (k + 1)).ker
⊢ ((ad R L) x ^ (k + 1)) (N.subtype y) = 0

Tactic:
clear hk

Goal state after:
case h
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
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
y : ↥N
hy : y ∈ (dx ^ (k + 1)).ker
⊢ ((ad R L) x ^ (k + 1)) (N.subtype y) = 0
Module: Mathlib.LinearAlgebra.Lagrange

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

Tactic:
simp [eval_finsetSum, eval_prod]

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)
i j : I
⊢ ⁅y, v.end (i, j)⁆ = (fμ i - fμ j) • v.end (i, j)

Tactic:
rw [instLieRingModule_eq, v.lie_end_of_apply_eq_smul fμ y hyv]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
⊢ (eval₂Hom f g).comp C = f

Tactic:
ext1 r

Goal state after:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
r : R
⊢ ((eval₂Hom f g).comp C) r = f r
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 : Rˣ
⊢ i ∈ (↑G).toFinset → eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)

Tactic:
hi

Goal state after:
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 : Rˣ
hi : i ∈ (↑G).toFinset
⊢ eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)
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 : Rˣ
hi : i ∈ (↑G).toFinset
⊢ 0 = eval (↑i) (X ^ Fintype.card ↥G - 1)

Tactic:
replace hi : i ∈ G := by simpa using hi

Goal state after:
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 : Rˣ
hi : i ∈ G
⊢ 0 = eval (↑i) (X ^ Fintype.card ↥G - 1)
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 : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
⊢ eval x (C (nodalWeight s v i) * (nodal s v / (X - C (v i)))) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)

Tactic:
eval_mul,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
⊢ eval x (C (nodalWeight s v i)) * eval x (nodal s v / (X - C (v i))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
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
x : F
hx : ∀ i ∈ s, x ≠ v i
⊢ ∑ i ∈ s, eval x (C (r i) * Lagrange.basis s v i) =
    ∑ i ∈ s, eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)

Tactic:
eval_mul,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
⊢ ∑ x_1 ∈ s, eval x (C (r x_1)) * eval x (Lagrange.basis s v x_1) =
    ∑ i ∈ s, eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)
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:
trace_eq_matrix_trace _ v,

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
⊢ ((toMatrix v v) (s * y)).trace = ∑ i, fμ i * μ i
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
⊢ homogeneousSubmodule σ R n = AddMonoidAlgebra.supported R R {d | (weight fun x ↦ 1) d = n}

Tactic:
exact weightedHomogeneousSubmodule_eq_finsupp_supported R 1 n

Goal state after:
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✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
⊢ ↑(((decompose 𝒜) r) i) ∈ RingHom.ker (projZeroRingHom 𝒜)

Tactic:
change (decompose 𝒜 (decompose 𝒜 r _ : A) 0 : A) = 0

Goal state after:
ι : 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
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) i)) 0) = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : 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 : σ →₀ ℕ
⊢ i ∈ φ.coeff.support → ((fun s a ↦ f a * s.prod fun n e ↦ g n ^ e) i (φ.coeff i)).IsHomogeneous (n * m)

Tactic:
hi

Goal state after:
σ : 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
⊢ ((fun s a ↦ f a * s.prod fun n e ↦ g n ^ e) i (φ.coeff i)).IsHomogeneous (n * m)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg
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 : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weight w) x = m
⊢ 0 = coeff x p

Tactic:
zero_coeff

Goal state after:
case neg
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 : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weight w) x = m
⊢ 0 = 0
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
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Polynomial.map (↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ))))
      (Polynomial.map (MvPolynomial.map (algebraMap R A)) (charpoly.univ R ιM)) =
    Polynomial.map (MvPolynomial.map (algebraMap R A))
      (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM))

Tactic:
simp only [Polynomial.map_map]

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
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Polynomial.map
      ((↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ)))).comp
        (MvPolynomial.map (algebraMap R A)))
      (charpoly.univ R ιM) =
    Polynomial.map ((MvPolynomial.map (algebraMap R A)).comp ↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case e'_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ ↑(x m) = (weightedHomogeneousComponent w m) ↑(x m)

Tactic:
rw [IsWeightedHomogeneous.weightedHomogeneousComponent_same (x m).prop]

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

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

Tactic:
hi

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : i ∈ Finset.range n
⊢ constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case inr.inr
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 : ℕ
⊢ i < r → χ.coeff i = 0

Tactic:
hi

Goal state after:
case inr.inr
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
⊢ χ.coeff i = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
s : Finset m
hz : ∀ x ∉ ↑s, A.row x = 0
B : Matrix m (↥s) R := of fun i a ↦ if ↑a = i then 1 else 0
hBdef : B = of fun i a ↦ if ↑a = i then 1 else 0
hB : B * A.submatrix Subtype.val id = A
⊢ A.rank = (B * A.submatrix Subtype.val id).rank

Tactic:
rw [hB]

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

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Fintype n
inst✝ : CommSemiring R
A : Matrix m n R
⊢ A.rank = finrank R ↥(span R (range A.col))

Tactic:
rw [rank, Matrix.range_mulVecLin]

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

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥A.mulVecLin.ker =
    finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥(Aᵀ * A).mulVecLin.ker

Tactic:
ker_mulVecLin_transpose_mul_self

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥A.mulVecLin.ker =
    finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥A.mulVecLin.ker
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case intro
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Finite m
A : Matrix m n R
val✝ : Fintype m
⊢ finrank R ↥(span R (range Aᵀ.col)) = finrank R ↥(span R (range A.row))

Tactic:
col_transpose

Goal state after:
case intro
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Finite m
A : Matrix m n R
val✝ : Fintype m
⊢ finrank R ↥(span R (range A.row)) = finrank R ↥(span R (range A.row))
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case h
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
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
z' : Q := (LieSubmodule.Quotient.mk' E) z
n : ℕ
hn : (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z) = (LieSubmodule.Quotient.mk' E) 0
⊢ ((toEnd K (↥U) Q) v ^ n) z' = 0

Tactic:
rw [map_zero] at hn

Goal state after:
case h
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
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
z' : Q := (LieSubmodule.Quotient.mk' E) z
n : ℕ
hn : (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z) = 0
⊢ ((toEnd K (↥U) Q) v ^ n) z' = 0
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
a : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ ⁅x, ⁅y, a z⁆⁆ - ⁅x, ⁅z, a y⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆ - ⁅y, ⁅z, a x⁆⁆ - ⁅y, a ⁅x, z⁆⁆) +
            (⁅z, ⁅x, a y⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - ⁅z, a ⁅x, y⁆⁆) -
          (⁅x, ⁅y, a z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆) - ⁅z, a ⁅x, y⁆⁆ - a (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)) +
        (⁅x, ⁅z, a y⁆⁆ - ⁅z, ⁅x, a y⁆⁆ - ⁅y, a ⁅x, z⁆⁆ - a (⁅x, ⁅z, y⁆⁆ - ⁅z, ⁅x, y⁆⁆)) -
      (⁅y, ⁅z, a x⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - a (⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆)) =
    0

Tactic:
leibniz_lie z x,

Goal state after:
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
a : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ ⁅x, ⁅y, a z⁆⁆ - ⁅x, ⁅z, a y⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆ - ⁅y, ⁅z, a x⁆⁆ - ⁅y, a ⁅x, z⁆⁆) +
            (⁅⁅z, x⁆, a y⁆ + ⁅x, ⁅z, a y⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - ⁅z, a ⁅x, y⁆⁆) -
          (⁅x, ⁅y, a z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆) - ⁅z, a ⁅x, y⁆⁆ - a (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)) +
        (⁅x, ⁅z, a y⁆⁆ - (⁅⁅z, x⁆, a y⁆ + ⁅x, ⁅z, a y⁆⁆) - ⁅y, a ⁅x, z⁆⁆ - a (⁅x, ⁅z, y⁆⁆ - ⁅z, ⁅x, y⁆⁆)) -
      (⁅y, ⁅z, a x⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - a (⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆)) =
    0
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x y : Derivation R A' A' × Derivation R A A
hx : x ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}
hy : y ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}
hxx : ∀ (a : A), ((compAlgebraMapL R A A' A') x.1) a = ((Algebra.ofId A A').toLinearMap.compDer x.2) a
hyy : ∀ (a : A), ((compAlgebraMapL R A A' A') y.1) a = ((Algebra.ofId A A').toLinearMap.compDer y.2) a
⊢ ⁅x, y⁆ ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}

Tactic:
ext z

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x y : Derivation R A' A' × Derivation R A A
hx : x ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}
hy : y ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}
hxx : ∀ (a : A), ((compAlgebraMapL R A A' A') x.1) a = ((Algebra.ofId A A').toLinearMap.compDer x.2) a
hyy : ∀ (a : A), ((compAlgebraMapL R A A' A') y.1) a = ((Algebra.ofId A A').toLinearMap.compDer y.2) a
z : A
⊢ ((compAlgebraMapL R A A' A') ⁅x, y⁆.1) z = ((Algebra.ofId A A').toLinearMap.compDer ⁅x, y⁆.2) z