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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i j k : ι
hi : 0 < b.height i
hj : 0 < b.height j
hk : P.root k = P.root i + P.root j
⊢ 0 < b.height i + b.height j

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i j k : ι
hi : 0 < b.height i
hj : j ∈ b.support
hk : P.root k = P.root i - P.root j
⊢ 0 ≤ b.height i - 1

Tactic:
lia

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

Goal state before:
pp: R₂ : Type u_3
inst✝² : CommRing R₂
n : Type u_5
inst✝¹ : Fintype n
J A : Matrix n n R₂
inst✝ : DecidableEq n
⊢ A ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A

Tactic:
simp only [mem_selfAdjointMatricesSubmodule]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hj : j ∈ b.support
hk : P.root k = P.root i + z • P.root j
this : InvolutiveNeg ι := P.indexNeg
hi : 0 < -1
contra : i = -j
⊢ False

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι}, b.IsPos i → P.root k = P.root i + ↑w • P.root j → LinearIndependent R ![P.root j, P.root i] → b.IsPos k
i k : ι
hi : b.IsPos i
hij : LinearIndependent R ![P.root j, P.root i]
hk : w + 1 ≤ chainTopCoeff j i
⊢ w ≤ chainTopCoeff j i

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι}, b.IsPos i → P.root k = P.root i + -↑w • P.root j → LinearIndependent R ![P.root j, P.root i] → b.IsPos k
i k : ι
hi : b.IsPos i
hij : LinearIndependent R ![P.root j, P.root i]
hk : w + 1 ≤ chainBotCoeff j i
⊢ w ≤ chainBotCoeff j i

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι}, b.IsPos i → b.height i = ↑n → p i
i : ι
h₀ : b.IsPos i
hN : b.height i = ↑n + 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk : P.root k = P.root i - P.root j
⊢ b.height i - 1 = ↑n

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι}, b.IsPos i → b.height i = ↑n → p i
i : ι
h₀ : b.IsPos i
hN : b.height i = ↑n + 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk : P.root k = P.root i - P.root j
hkn : b.height k = ↑n
⊢ 0 ≤ b.height k

Tactic:
lia

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

Goal state before:
pp: case pred
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι}, b.IsPos i → b.height i = -↑n → p i
i : ι
h₀ : 0 < b.height i
hN : b.height i = -↑n - 1
⊢ p i

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : ¬↑m < n
⊢ ↑m = n

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι}, b.IsPos i → (b.height i).natAbs = m → p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
hk : b.IsPos ((P.reflectionPerm j) i)
this✝ : b.height ((P.reflectionPerm j) i) < b.height i
this : ↑(b.height ((P.reflectionPerm j) i)).natAbs = b.height ((P.reflectionPerm j) i)
⊢ (b.height ((P.reflectionPerm j) i)).natAbs < n

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case inr.h.h
x c : ℝ
a b : CauSeq ℚ abs
h✝ : mk a < mk b
⊢ mk a + c < mk b + c

Tactic:
induction c using Real.ind_mk with

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

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
⊢ v x = w x

Tactic:
classical rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Field R
d : n → R
μ : R
⊢ μ ∈ spectrum R ((toLinAlgEquiv (Pi.basisFun R n)) (diagonal d)) ↔ μ ∈ Set.range d

Tactic:
← hasEigenvalue_iff_mem_spectrum

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Field R
d : n → R
μ : R
⊢ HasEigenvalue ((toLinAlgEquiv (Pi.basisFun R n)) (diagonal d)) μ ↔ μ ∈ Set.range d
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℕ
hd : d ≠ 0
a✝ : Nontrivial R
x✝ : n
⊢ 0 < ↑d

Tactic:
simpa [pos_iff_ne_zero]

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℤ
hd : 0 < d
a✝ : Nontrivial R
x✝ : n
⊢ 0 < ↑d

Tactic:
simpa [pos_iff_ne_zero]

Goal state after:
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
i : ι
⊢ 0 < d i * A i i

Tactic:
simpa using hA.2 (x := Finsupp.single i 1) (by simp)

Goal state after:
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✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), P.root ↑k ∈ q ↔ p k
k : ↥b.support
hk : P.root ↑k ∉ q
x : M
hx : x ∈ q
⊢ (P.coroot' ↑k) x = 0

Tactic:
contrapose! hk

Goal state after:
ι : 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✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), P.root ↑k ∈ q ↔ p k
k : ↥b.support
x : M
hx : x ∈ q
hk : (P.coroot' ↑k) x ≠ 0
⊢ P.root ↑k ∈ q
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝ : Semiring S
n k : ℕ
⊢ ↑(eval k (ascPochhammer ℕ n)) = eval₂ (algebraMap ℕ S) (↑k) (ascPochhammer ℕ n)

Tactic:
← eq_natCast (algebraMap ℕ S),

Goal state after:
S : Type u
inst✝ : Semiring S
n k : ℕ
⊢ (algebraMap ℕ S) (eval k (ascPochhammer ℕ n)) = eval₂ (algebraMap ℕ S) (↑k) (ascPochhammer ℕ n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ.inr.inr
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
hkn : n < k
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0

Tactic:
lia

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
h : eval r (ascPochhammer R n) = 0
rn : ℕ
hrn : rn < n
rrn : ↑rn = -r
⊢ rn < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i j : ι
hij : i ≠ j
⊢ Lagrange.basis {i, j} v i = basisDivisor (v i) (v j)

Tactic:
by
  simp only [Lagrange.basis, hij, erase_insert_eq_erase, erase_eq_of_notMem, mem_singleton,
    not_false_iff, prod_singleton]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i ↦ (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
h : (vandermonde v).det = (of fun i j ↦ eval (↑(w' i)) (descPochhammer ℤ ↑j)).det
⊢ ↑n.superFactorial ∣ (vandermonde v).det

Tactic:
use (of (fun (i j : Fin (n + 1)) => (Nat.choose (w' i) (j : ℕ) : ℤ))).det

Goal state after:
case h
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := ⋯
w' : Fin (n + 1) → ℕ := ⋯
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
h : (vandermonde v).det = (of fun i j ↦ eval (↑(w' i)) (descPochhammer ℤ ↑j)).det
⊢ (vandermonde v).det = ↑n.superFactorial * (of fun i j ↦ ↑((w' i).choose ↑j)).det
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm : ((ad R L) x ^ m) y = 0
n : ℕ
hn : ((ad R L) x ^ n) z = 0
ij : ℕ × ℕ
hij : ij.1 + ij.2 = m + n
⊢ m ≤ ij.1 ∨ n ≤ ij.2

Tactic:
lia

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 : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
deg : ℕ
hdeg : ↑deg = P.degree
hP : #s = deg + 1
hdegree : P.degree = ↑(#s - 1)
⊢ #s - 1 < #s

Tactic:
lia

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
x✝ : MvPolynomial σ R
⊢ x✝.IsHomogeneous 0 ↔ x✝ ∈ 1

Tactic:
← MvPolynomial.totalDegree_zero_iff_isHomogeneous,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
x✝ : MvPolynomial σ R
⊢ x✝.totalDegree = 0 ↔ x✝ ∈ 1
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
j : n
⊢ ((monomial (Finsupp.single j 1)) (M i j)).IsHomogeneous 1

Tactic:
apply MvPolynomial.isHomogeneous_monomial _ _

Goal state after:
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
j : n
⊢ Finsupp.degree (Finsupp.single j 1) = 1
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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
tfae_3_to_4 : constantCoeff (charpoly φ) = 0 → LinearMap.det φ = 0
tfae_4_to_5 : LinearMap.det φ = 0 → ⊥ < ker φ
⊢ (∀ (m : M), m ≠ 0 → φ m ≠ 0) → ¬⊥ < ker φ

Tactic:
simp only [not_bot_lt_iff, eq_bot_iff]

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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
tfae_3_to_4 : constantCoeff (charpoly φ) = 0 → LinearMap.det φ = 0
tfae_4_to_5 : LinearMap.det φ = 0 → ⊥ < ker φ
⊢ (∀ (m : M), m ≠ 0 → φ m ≠ 0) → ker φ ≤ ⊥
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 : ℕ
hi : i < n
⊢ i + (n - i) = n

Tactic:
lia

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
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
x : DirectSum M fun i ↦ ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ (weightedHomogeneousComponent w m) ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w)) x) = ↑(x m)

Tactic:
exact weightedHomogeneousComponent_directSum R w x m

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

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
ι : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
inst✝¹⁰ : Module.Finite R L
inst✝⁹ : Free R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R M
inst✝³ : Free R M
inst✝² : Fintype ι
b : Basis ι R L
inst✝¹ : Nontrivial R
inst✝ : DecidableEq ι
⊢ rank R L M = ((↑(toEnd R L M)).polyCharpoly b).natTrailingDegree

Tactic:
by
  apply nilRank_eq_polyCharpoly_natTrailingDegree

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

Goal state before:
pp: R : Type u_1
L : Type u_3
ι : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Fintype ι
b : Basis ι R L
inst✝¹ : Nontrivial R
inst✝ : DecidableEq ι
⊢ rank R L = ((↑(ad R L)).polyCharpoly b).natTrailingDegree

Tactic:
by
  apply nilRank_eq_polyCharpoly_natTrailingDegree

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

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

Tactic:
lia

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

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

Tactic:
lia

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

Goal state before:
pp: R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin✝ : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
this : ((finSuccEquiv R N) F).natDegree ≠ n
⊢ ((finSuccEquiv R N) F).natDegree < n

Tactic:
lia

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ χ x = 0

Tactic:
induction h using Submodule.span_induction with

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : f ∈ skewAdjointSubmodule B
hg : g ∈ skewAdjointSubmodule B
⊢ ⁅f, g⁆ ∈ skewAdjointSubmodule B

Tactic:
rw [mem_skewAdjointSubmodule] at *

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B ⇑f
hg : IsSkewAdjoint B ⇑g
⊢ IsSkewAdjoint B ⇑⁅f, g⁆
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 : LinearMap.charpoly ((toEnd K ↥U ↥E) y') = X ^ r
⊢ Ex ≤ Ey

Tactic:
r,

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
this : LinearMap.charpoly ((toEnd K ↥U ↥E) y') = X ^ finrank K ↥E
⊢ Ex ≤ Ey
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:
r,

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
this : ∀ i < finrank K ↥E, χ.coeff i = 0
⊢ χ = X ^ finrank K ↥E
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
h : A ∈ symplecticGroup l R
⊢ -A ∈ symplecticGroup l R

Tactic:
mem_iff

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
h : A * J l R * Aᵀ = J l R
⊢ -A * J l R * (-A)ᵀ = J l R
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: case h
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
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Tactic:
mem_iff

Goal state after:
case h
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 * J l R * Aᵀ = J l R
⊢ (J l R).det * (A.det * A.det) = (J l R).det
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
⊢ Aᵀ ∈ symplecticGroup l R

Tactic:
mem_iff

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 * J l R * Aᵀ = J l R
⊢ Aᵀ * J l R * Aᵀᵀ = J l R
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
⊢ -(J l R * Aᵀ * J l R * A) = -J l R * (Aᵀ * J l R * A)

Tactic:
by
      simp only [Matrix.mul_assoc, Matrix.neg_mul]

Goal state after: