mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑(↑n - ↑(chainTopCoeff (⇑α) β))
⊢ rootSpace H✝ ((↑n - ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑0) ≠ ⊥

Tactic:
← Int.cast_smul_eq_zsmul K,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑(↑n - ↑(chainTopCoeff (⇑α) β))
⊢ rootSpace H✝ (↑(↑n - ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑0) ≠ ⊥
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case inr.inr.refine_2
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = 2 * n + 1
H : k * 2 / 2 = ↑(↑(2 * n + 1) - 2 * ↑(chainTopCoeff (⇑α) β)) / 2
hk : k = ↑n + 2⁻¹ - ↑(chainTopCoeff (⇑α) β)
this : rootSpace H✝ ((↑(chainTopCoeff (⇑α) β) - ↑n) • ⇑α + (↑n + 2⁻¹ - ↑(chainTopCoeff (⇑α) β)) • ⇑α) ≠ ⊥
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
← Int.cast_smul_eq_zsmul K,

Goal state after:
case inr.inr.refine_2
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = 2 * n + 1
H : k * 2 / 2 = ↑(↑(2 * n + 1) - 2 * ↑(chainTopCoeff (⇑α) β)) / 2
hk : k = ↑n + 2⁻¹ - ↑(chainTopCoeff (⇑α) β)
this : rootSpace H✝ (↑(↑(chainTopCoeff (⇑α) β) - ↑n) • ⇑α + (↑n + 2⁻¹ - ↑(chainTopCoeff (⇑α) β)) • ⇑α) ≠ ⊥
⊢ k = -1 ∨ k = 0 ∨ k = 1
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
⊢ MulOpposite.op (coweightMap 1) = 1

Tactic:
by
    simp only [MulOpposite.op_eq_one_iff, coweightMap_one, Module.End.one_eq_id]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ β✝ α β : Weight K (↥H) L
⊢ genWeightSpace L (⇑β - β (coroot α) • ⇑α) ≠ ⊥

Tactic:
by_cases hα : α.IsZero
    · simpa [hα.eq] using β.genWeightSpace_ne_bot
    rw [sub_eq_neg_add, apply_coroot_eq_cast α β, ← neg_smul, ← Int.cast_neg,
      Int.cast_smul_eq_zsmul, rootSpace_zsmul_add_ne_bot_iff α β hα]
    lia

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

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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
i : ι
⊢ Bijective ⇑(P.coreflection i)

Tactic:
exact LinearEquiv.bijective (P.coreflection i)

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

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
i : ι
x : N
⊢ (↑(reflection P i)⁻¹).coweightMap x = (↑(reflection P i)).coweightMap x

Tactic:
simp [← coweightEquiv_apply]

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

Goal state before:
pp: case pos
ι : 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
f✝ : ι → ℤ
hf : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
c : ↑↑b.support → ℕ
hc : ∀ (i : ↥b.support), ↑(c i) = f' i
i : ι
hi : i ∈ b.support
⊢ 0 i ≤ f i

Tactic:
change 0 ≤ f' ⟨i, hi⟩
      simp [← hc]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
k : ι
hk : P.root k = P.root j - P.root i
⊢ chainTopCoeff i k = chainTopCoeff i j + 1

Tactic:
by
  let := P.indexNeg
  replace hk : P.root k = P.root j + P.root (-i) := by simpa [sub_eq_add_neg] using hk
  simpa using chainBotCoeff_of_add (by simpa) hk

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

Goal state before:
pp: case inr
ι : 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 : ι
f : ι → ℕ
hf : Function.support f ⊆ ↑b.support
hf' : P.root i = -∑ j ∈ b.support, f j • P.root j
⊢ ∃ f, Function.support f ⊆ ↑b.support ∧ (0 < f ∨ f < 0) ∧ P.root i = ∑ j ∈ b.support, f j • P.root j

Tactic:
refine ⟨-Nat.cast ∘ f, by simpa, Or.inr <| Pi.lt_def.mpr ⟨fun _ ↦ by simp, ?_⟩, by simp [hf']⟩
    by_contra! contra
    replace contra : f = 0 := by ext i; simpa using contra i
    exact P.ne_zero i <| by simp [hf', contra]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i✝ : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
i : ι
⊢ ∃ q, 0 < q ∧ ↑q = 2 / (P.RootForm (P.root i)) (P.root i)

Tactic:
refine ⟨2 / P.RootFormIn ℚ (P.rootSpanMem ℚ i) (P.rootSpanMem ℚ i), ?_, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i✝ : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
i : ι
⊢ 0 < 2 / ((P.RootFormIn ℚ) (P.rootSpanMem ℚ i)) (P.rootSpanMem ℚ i)

case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i✝ : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
i : ι
⊢ ↑(2 / ((P.RootFormIn ℚ) (P.rootSpanMem ℚ i)) (P.rootSpanMem ℚ i)) = 2 / (P.RootForm (P.root i)) (P.root i)
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
⊢ (const abv f.lim - f).LimZero

Tactic:
exact Setoid.symm (equiv_lim f)

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

Goal state before:
pp: f g : Cauchy abs
⊢ { cauchy := f / g } = { cauchy := f } / { cauchy := g }

Tactic:
by
  simp_rw [div_eq_mul_inv, ofCauchy_mul, ofCauchy_inv]

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

Goal state before:
pp: case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ ↑(y✝ - f) j
i : ℕ
H : ∀ j ≥ i, mk y✝ ≤ ↑(↑f j) ∧ K ≤ ↑(y✝ - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2
j : ℕ
ij : j ≥ i
this : K + -(K / 2) ≤ ↑(y✝ - f) j + (↑f j - ↑f i)
⊢ K / 2 ≤ ↑(y✝ - const abs (↑f i)) j

Tactic:
rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this

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

Goal state before:
pp: α : Type u_1
m : Type u_3
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
hA : A.IsHermitian
⊢ A⁻¹.IsHermitian

Tactic:
by simp [IsHermitian, conjTranspose_nonsing_inv, hA.eq]

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ A ^ (- -[n+1]) = (A ^ -[n+1])⁻¹

Tactic:
rw [zpow_negSucc, neg_negSucc, zpow_natCast, nonsing_inv_nonsing_inv]
    rw [det_pow]
    exact h.pow _

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ (A ^ n)⁻¹ = (A ^ n)⁻¹ * (A⁻¹ * A)

Tactic:
nonsing_inv_mul _ h,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ (A ^ n)⁻¹ = (A ^ n)⁻¹ * 1
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
hA : Function.Injective A.mulVec
⊢ (Aᴴ * A).PosDef

Tactic:
by
  classical
  simpa using conjTranspose_mul_mul_same .one hA

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

Goal state before:
pp: case refine_3
n : Type u_2
inst✝⁷ : Fintype n
R : Type u_5
M : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : TrivialStar R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq n
b : Module.Basis n R M
B : LinearMap.BilinForm R M
hB_symm : B.IsSymm
aux : ∀ (i j : n) (s t : R), t * (B (b i)) (b j) * s = t * (s * (B (b j)) (b i))
h : ((LinearMap.BilinForm.toMatrix b) B).PosDef
v : M
hv : v ≠ 0
⊢ 0 < (B ((Finsupp.linearCombination R ⇑b) (b.repr v))) ((Finsupp.linearCombination R ⇑b) (b.repr v))

Tactic:
simpa [Finsupp.linearCombination_apply, map_finsuppSum, Finsupp.mul_sum, aux]
      using h.2 (b.repr.map_ne_zero_iff.mpr hv)

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (inl R L₁ L₂).range = LieIdeal.toLieSubalgebra R (L₁ × L₂) (snd R L₁ L₂).ker

Tactic:
rw [← LieSubalgebra.toSubmodule_inj, range_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule,
    ker_toSubmodule]

Goal state after:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (↑(inl R L₁ L₂)).range = (↑(snd R L₁ L₂)).ker
Module: Mathlib.Algebra.Lie.Prod

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (inr R L₁ L₂).range = LieIdeal.toLieSubalgebra R (L₁ × L₂) (fst R L₁ L₂).ker

Tactic:
rw [← LieSubalgebra.toSubmodule_inj, range_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule,
    ker_toSubmodule]

Goal state after:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (↑(inr R L₁ L₂)).range = (↑(fst R L₁ L₂)).ker
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: k : ℕ
n : ℤ
⊢ (∏ i ∈ range k, (n + ↑i) % ↑k !) % ↑k ! = 0

Tactic:
← Int.emod_add_emod n

Goal state after:
k : ℕ
n : ℤ
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
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
⊢ ↑(#s - 1) < ↑(#s)

Tactic:
rw [Nat.cast_withBot, WithBot.coe_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
⊢ #s - 1 < #s
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case e_f
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
k : Fin n
⊢ v i ^ ↑k * (RingHom.id R) ((p j).coeff ↑k) = v i ^ ↑k * (p j).coeff ↑k

Tactic:
RingHom.id_apply

Goal state after:
case e_f
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
k : Fin n
⊢ v i ^ ↑k * (p j).coeff ↑k = v i ^ ↑k * (p j).coeff ↑k
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
⊢ IsWeightedHomogeneous w p ⊥

Tactic:
intro d hd

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
⊢ (weight w) d = ⊥
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 ((toEnd R (↥(derivedSeries R L 1)) M) ⟨x, hx⟩)

Tactic:
← IsNilpotent.map_iff hbc_inj,

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 ((End.baseChangeHom R A M) ((toEnd R (↥(derivedSeries R L 1)) M) ⟨x, hx⟩))
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
⊢ LieIdeal.killingCompl R L ⊤ ≤ radical R L

Tactic:
← LieIdeal.solvable_iff_le_radical

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
⊢ IsSolvable ↥(LieIdeal.killingCompl R L ⊤)
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 𝒜
κ : Sort u_4
f : κ → Ideal A
s : κ → Set ↥(homogeneousSubmonoid 𝒜)
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ ⨆ i, f i = span (⋃ i, Subtype.val '' s i)

Tactic:
Ideal.span_iUnion

Goal state after:
ι : 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 𝒜
κ : Sort u_4
f : κ → Ideal A
s : κ → Set ↥(homogeneousSubmonoid 𝒜)
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ ⨆ i, f i = ⨆ i, span (Subtype.val '' s i)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
HI : IsHomogeneous 𝒜 I
HJ : IsHomogeneous 𝒜 J
⊢ IsHomogeneous 𝒜 (I * J)

Tactic:
rw [Ideal.IsHomogeneous.iff_exists] at HI HJ ⊢

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
HI : ∃ S, I = span (Subtype.val '' S)
HJ : ∃ S, J = span (Subtype.val '' S)
⊢ ∃ S, I * J = span (Subtype.val '' S)
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 | degree d = n}

Tactic:
degree_eq_weight_one

Goal state after:
σ : 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}
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : degree d = n
⊢ ((monomial d) r).IsHomogeneous n

Tactic:
degree_eq_weight_one

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : (weight fun x ↦ 1) d = n
⊢ ((monomial d) r).IsHomogeneous n
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
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp✝ : IsWeightedHomogeneous w p m
hp : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = m})
A : Submodule R (MvPolynomial σ R) :=
  { carrier := {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
⊢ {d | (weight w) d = m} ⊆ (fun m ↦ AddMonoidAlgebra.single m 1) ⁻¹' ↑A

Tactic:
intro d hd

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp✝ : IsWeightedHomogeneous w p m
hp : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = m})
A : Submodule R (MvPolynomial σ R) :=
  { carrier := {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d = m}
⊢ d ∈ (fun m ↦ AddMonoidAlgebra.single m 1) ⁻¹' ↑A
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
φ : MvPolynomial σ R
⊢ IsWeightedHomogeneous w ((weightedHomogeneousComponent w n) φ) n

Tactic:
intro d hd

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d ((weightedHomogeneousComponent w n) φ) ≠ 0
⊢ (weight w) d = n
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
d : σ →₀ ℕ
hd : degree d ≠ n
⊢ coeff d φ = 0

Tactic:
degree_eq_weight_one

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : (weight fun x ↦ 1) d ≠ n
⊢ coeff d φ = 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
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
⊢ ∀ x ∈ {d ∈ φ.support | (weight w) d = n}, (monomial x) (coeff x φ) = 0

Tactic:
intro d hd

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ {d ∈ φ.support | (weight w) d = n}
⊢ (monomial d) (coeff d φ) = 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
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
⊢ ∀ x ∈ {d ∈ φ.support | (weight w) d = n}, (monomial x) (coeff x φ) = 0

Tactic:
intro d hd

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ {d ∈ φ.support | (weight w) d = n}
⊢ (monomial d) (coeff d φ) = 0