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

Goal state before:
pp: case h₂
ι : 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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
i j k : ι
l : ι₂
hl : P₂.root l = f (P.root j)
hk : k ∈ b.support
this : f ((P.reflection k) (P.root j)) = (P₂.reflection ↑(e ⟨k, hk⟩)) (f (P.root j))
⊢ (P₂.reflection ↑(e ⟨k, hk⟩)) (P₂.root l) ∈ range ⇑P₂.root

Tactic:
← root_reflectionPerm

Goal state after:
case h₂
ι : 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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
i j k : ι
l : ι₂
hl : P₂.root l = f (P.root j)
hk : k ∈ b.support
this : f ((P.reflection k) (P.root j)) = (P₂.reflection ↑(e ⟨k, hk⟩)) (f (P.root j))
⊢ P₂.root ((P₂.reflectionPerm ↑(e ⟨k, hk⟩)) l) ∈ range ⇑P₂.root
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₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅R⁆ L₁ := (LieHom.fst R L₁ L₂).comp L.incl
h₁ : range b₁.e = range (⇑p₁ ∘ prodE eι b₁ b₂)
h₂ : range b₁.f = range (⇑p₁ ∘ prodF eι b₁ b₂)
⊢ lieSpan R L₁ (range b₁.e ∪ range b₁.f) ≤ p₁.range

Tactic:
map_top,

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₂
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₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅R⁆ L₁ := (LieHom.fst R L₁ L₂).comp L.incl
h₁ : range b₁.e = range (⇑p₁ ∘ prodE eι b₁ b₂)
h₂ : range b₁.f = range (⇑p₁ ∘ prodF eι b₁ b₂)
⊢ lieSpan R L₁ (range b₁.e ∪ range b₁.f) ≤ LieSubalgebra.map p₁ ⊤
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₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
h₁ : range b₂.e = range (⇑p₂ ∘ prodE eι b₁ b₂)
h₂ : range b₂.f = range (⇑p₂ ∘ prodF eι b₁ b₂)
⊢ lieSpan R L₂ (range b₂.e ∪ range b₂.f) ≤ p₂.range

Tactic:
map_top,

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₂
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₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
h₁ : range b₂.e = range (⇑p₂ ∘ prodE eι b₁ b₂)
h₂ : range b₂.f = range (⇑p₂ ∘ prodF eι b₁ b₂)
⊢ lieSpan R L₂ (range b₂.e ∪ range b₂.f) ≤ LieSubalgebra.map p₂ ⊤
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ eval (v i) ((interpolate (insert i (t \ s)) v) r) * eval (v i) (Lagrange.basis s v i) +
      ∑ x ∈ s.erase i, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) =
    r i

Tactic:
eval_basis_self (hvt.mono hst) hi',

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ eval (v i) ((interpolate (insert i (t \ s)) v) r) * 1 +
      ∑ x ∈ s.erase i, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) =
    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)
⊢ s = 0

Tactic:
let I := (ν : K) × Fin (finrank K (s.eigenspace ν))

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 ν))
⊢ s = 0
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
⊢ (interpolate s v) r = ∑ i ∈ s, C (r i / ∏ j ∈ s.erase i, (v i - v j)) * ∏ j ∈ s.erase i, (X - C (v j))

Tactic:
simp [Lagrange.basis, basisDivisor, div_eq_mul_inv, prod_mul_distrib, ← map_prod,
    ← prod_inv_distrib, mul_assoc]

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✝¹ : 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
⊢ p₁.ker ⊓ p₂.ker = ⊥

Tactic:
_root_.eq_bot_iff

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝¹¹ : Finite ι₁
inst✝¹⁰ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁹ : LieRing L₁
inst✝⁸ : LieRing L₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
L : LieSubalgebra K (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅K⁆ L₁ := (LieHom.fst K L₁ L₂).comp L.incl
p₂ : ↥L →ₗ⁅K⁆ L₂ := (LieHom.snd K L₁ L₂).comp L.incl
⊢ p₁.ker ⊓ p₂.ker ≤ ⊥
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(((decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
⊢ (GradedRing.proj 𝒜 j) (↑(((decompose 𝒜) r) k) * x) ∈ I

Tactic:
GradedRing.proj_apply,

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(((decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
⊢ ↑(((decompose 𝒜) (↑(((decompose 𝒜) r) k) * x)) j) ∈ I
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
M : n × n → S
⊢ ((mvPolynomialX n n R).map (eval₂ f M)).charpoly =
    ((mvPolynomialX n n R).map (eval₂ f fun p ↦ of (Function.curry M) p.1 p.2)).charpoly

Tactic:
simp only [of_apply, Function.curry_apply, Prod.mk.eta]

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✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ I ≤ (homogeneousHull 𝒜 I).toIdeal

Tactic:
intro r hr
  classical
  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.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 𝒜
x : A
i : ι
hi : 0 < i
hx : x ∈ 𝒜 i
⊢ (proj 𝒜 0) x = 0

Tactic:
GradedRing.proj_apply,

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 𝒜
x : A
i : ι
hi : 0 < i
hx : x ∈ 𝒜 i
⊢ ↑(((decompose 𝒜) x) 0) = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
⊢ ((rename f) φ).IsHomogeneous n ↔ φ.IsHomogeneous n

Tactic:
refine ⟨fun h d hd ↦ ?_, rename_isHomogeneous⟩

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) d = n
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
⊢ F ≠ 0

Tactic:
contrapose hFn

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : F = 0
⊢ ((finSuccEquiv R N) F).coeff n = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case h
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
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
⊢ constantCoeff (((finSuccEquiv R N) F).coeff n) ≠ 0

Tactic:
contrapose hFn

Goal state after:
case h
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
⊢ ((finSuccEquiv R N) F).coeff n = 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
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
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : Nontrivial R
b : Basis ι R L
⊢ φ.nilRank = (φ.polyCharpoly b).natTrailingDegree

Tactic:
apply nilRankAux_basis_indep

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
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
ι : Type u_8
inst✝ : Fintype ι
b : Basis ι R M
⊢ φ.nilRank ≤ Fintype.card ι

Tactic:
by
  apply Polynomial.natTrailingDegree_le_of_ne_zero
  rw [← Module.finrank_eq_card_basis b, ← polyCharpoly_natDegree φ (chooseBasis R L),
    Polynomial.coeff_natDegree, (polyCharpoly_monic _ _).leadingCoeff]
  apply one_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
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 :
  (eval ⇑((chooseBasis R L).repr x)) ((φ.polyCharpoly (chooseBasis R L)).coeff (charpoly (φ x)).natTrailingDegree) =
    (eval ⇑((chooseBasis R L).repr x)) 0
⊢ False

Tactic:
polyCharpoly_coeff_eval,

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 = (eval ⇑((chooseBasis R L).repr x)) 0
⊢ False
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
A B : Matrix n n R
hA : A ∈ skewAdjointMatricesSubmodule J
hB : B ∈ skewAdjointMatricesSubmodule J
⊢ ⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J

Tactic:
simp only [mem_skewAdjointMatricesSubmodule] at *

Goal state after:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
A B : Matrix n n R
hA : J.IsSkewAdjoint A
hB : J.IsSkewAdjoint B
⊢ J.IsSkewAdjoint ⁅A, B⁆
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
n : Type w
inst✝⁴ : CommRing R
inst✝³ : Fintype n
J : Matrix n n R
inst✝² : DecidableEq n
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h : ∀ (A : Matrix n n R), (e A)ᵀ = e Aᵀ
⊢ LieSubalgebra.map e.toLieEquiv.toLieHom (skewAdjointMatricesLieSubalgebra J) = skewAdjointMatricesLieSubalgebra (e J)

Tactic:
by
    ext A
    suffices J.IsSkewAdjoint (e.symm A) ↔ (e J).IsSkewAdjoint A by
      simpa [-LieSubalgebra.mem_map, LieSubalgebra.mem_map_submodule]
    simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, ← h,
      ← Function.Injective.eq_iff e.injective, map_mul, AlgEquiv.apply_symm_apply, map_neg]

Goal state after:
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} := ⟨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
this : ∀ i < (lieCharpoly K (↥E) x' u).natDegree, χ.coeff i = 0
⊢ (lieCharpoly K (↥E) x' u).natDegree ≤ (lieCharpoly K (↥E) x' u).natTrailingDegree

Tactic:
exact le_natTrailingDegree (lieCharpoly_monic K E x' u).ne_zero this

Goal state after:
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} := ⟨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
this : ∀ i < r, χ.coeff i = 0
⊢ χ = X ^ r

Tactic:
simp_rw [r, ← lieCharpoly_natDegree K E x' u] at this ⊢
    rw [(lieCharpoly_monic K E x' u).eq_X_pow_iff_natDegree_le_natTrailingDegree]
    exact le_natTrailingDegree (lieCharpoly_monic K E x' u).ne_zero this

Goal state after:
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} := ⟨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, r ≤ s.card ∧ ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0

Tactic:
let t := (constantCoeff ψ).roots.toFinset

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} := ⟨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
t : Finset K := (constantCoeff ψ).roots.toFinset
⊢ ∃ s, r ≤ s.card ∧ ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 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
a b : L →ₗ[R] L →ₗ[R] M
ha : a ∈ {c | ∀ (x : L), (c x) x = 0}
hb : b ∈ {c | ∀ (x : L), (c x) x = 0}
x : L
⊢ ((a + b) x) x = 0

Tactic:
simp [ha x, hb x]

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

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
x y z : ⨁ (i : ι), L i
i✝ : ι
⊢ (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ y z)) i✝ =
    (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x y) z +
        zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ y (zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x z))
      i✝

Tactic:
simp only [zipWith_apply, add_apply]

Goal state after:
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
x y z : ⨁ (i : ι), L i
i✝ : ι
⊢ ⁅x i✝, ⁅y i✝, z i✝⁆⁆ = ⁅⁅x i✝, y i✝⁆, z i✝⁆ + ⁅y i✝, ⁅x i✝, z i✝⁆⁆
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ (decomposeAux f) (single m r) = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m r, ⋯⟩

Tactic:
by
  refine (lift_single _ _ _).trans ?_
  refine (DirectSum.of_smul R _ _ _).symm.trans ?_
  apply DirectSum.of_eq_of_gradedMonoid_eq
  refine Sigma.subtype_ext rfl ?_
  refine (smul_single' _ _ _).trans ?_
  rw [mul_one]
  rfl

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

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ (ofProd c)
      (⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).1⁆,
        (↑↑c ((ofProd c).symm (x + y)).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).2⁆ -
          ⁅((ofProd c).symm z).1, ((ofProd c).symm (x + y)).2⁆) =
    (ofProd c)
      ((⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆) +
        (⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆))

Tactic:
refine Equiv.congr_arg ?_

Goal state after:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ (⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).1⁆,
      (↑↑c ((ofProd c).symm (x + y)).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).2⁆ -
        ⁅((ofProd c).symm z).1, ((ofProd c).symm (x + y)).2⁆) =
    (⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
        (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
          ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆) +
      (⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆,
        (↑↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆ -
          ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆)