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

Goal state before:
pp: case refine_2
ι : 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 : ι
this✝ : InvolutiveNeg ι := P.indexNeg
this :
  ∀ (z : ℤ),
    z ∈ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) ↔ z ∈ Icc (-↑(chainBotCoeff i (-j))) ↑(chainTopCoeff i (-j))
⊢ chainTopCoeff i j ≤ chainBotCoeff i ((P.reflectionPerm j) j)

Tactic:
simpa using this (-P.chainTopCoeff i j)

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

Goal state before:
pp: case inl
ι : 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
pos : 0 < f
⊢ ∑ j ∈ b.support, f j ≠ 0

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
neg : f < 0
⊢ ∑ j ∈ b.support, f j ≠ 0

Tactic:
· refine (Finset.sum_pos' (fun i _ ↦ pos.le i) ?_).ne'
    by_contra! contra
    replace contra (j : ι) : f j = 0 := by
      by_cases hj : j ∈ f.support
      · exact le_antisymm (contra j (hf₀ hj)) (pos.le j)
      · simpa using hj
    exact P.ne_zero i <| by simp [hf₂, contra]

Goal state after:
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
neg : f < 0
⊢ ∑ j ∈ b.support, f j ≠ 0
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
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
this : ∀ (x : ↑(⇑P.root '' s)), a x • ↑x ≠ 0 → x ∈ {ri}
⊢ P.root j = ↑(a ri) • P.root i

Tactic:
simp [← ha, ← Fintype.sum_subset this, ri, Nat.cast_smul_eq_nsmul]

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
⊢ b.IsPos k

Tactic:
isPos_iff'

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✝³ : 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
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ k ≥ i, abv (↑g k - ↑g i) < ε / 2
⊢ abv (f j - f i) < ε

Tactic:
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi _ ij).1 h₁)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ k ≥ i, abv (↑g k - ↑g i) < ε / 2
this : abv (f j - ↑g j + (↑g i - f i)) < ε / 2 / 2 + ε / 2 / 2
⊢ abv (f j - f i) < ε
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ { cauchy := ⟦f⟧ }.lt { cauchy := ⟦g⟧ } ↔ f < g

Tactic:
rw [lt_def]; rfl

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

Goal state before:
pp: x y : ℚ
⊢ ↑x < ↑y ↔ x < y

Tactic:
rw [← mk_const, ← mk_const, mk_lt]
  exact const_lt

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

Goal state before:
pp: x a : ℝ
⊢ ∀ (b : ℝ), a ≤ a ⊔ b

Tactic:
b

Goal state after:
x a b : ℝ
⊢ a ≤ a ⊔ b
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ ∀ (b : ℝ), b ≤ a ⊔ b

Tactic:
b

Goal state after:
x a b : ℝ
⊢ b ≤ a ⊔ b
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ ∀ (b c : ℝ), a ≤ c → b ≤ c → a ⊔ b ≤ c

Tactic:
b

Goal state after:
x a b : ℝ
⊢ ∀ (c : ℝ), a ≤ c → b ≤ c → a ⊔ b ≤ c
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ ∀ (b : ℝ), a ⊓ b ≤ a

Tactic:
b

Goal state after:
x a b : ℝ
⊢ a ⊓ b ≤ a
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ ∀ (b : ℝ), a ⊓ b ≤ b

Tactic:
b

Goal state after:
x a b : ℝ
⊢ a ⊓ b ≤ b
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ ∀ (b c : ℝ), a ≤ b → a ≤ c → a ≤ b ⊓ c

Tactic:
b

Goal state after:
x a b : ℝ
⊢ ∀ (c : ℝ), a ≤ b → a ≤ c → a ≤ b ⊓ c
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ ∀ (y z : ℝ), (a ⊔ y) ⊓ (a ⊔ z) ≤ a ⊔ y ⊓ z

Tactic:
b

Goal state after:
x a b : ℝ
⊢ ∀ (z : ℝ), (a ⊔ b) ⊓ (a ⊔ z) ≤ a ⊔ b ⊓ z
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix n p R
h : Bᴴ * (Aᴴ * (A * B)) = 0
⊢ A * B = 0

Tactic:
← Matrix.mul_assoc,

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix n p R
h : Bᴴ * Aᴴ * (A * B) = 0
⊢ A * B = 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ ∀ (b : ℝ), a ≤ b ∨ b ≤ a

Tactic:
b

Goal state after:
x a b : ℝ
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝² : AddMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : DecidableEq n
d : n → α
⊢ (diagonal d).IsHermitian ↔ ∀ (i : n), IsSelfAdjoint (d i)

Tactic:
simp [isSelfAdjoint_iff, IsHermitian, conjTranspose, diagonal_transpose, diagonal_map]

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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ A * ↑hx'.unit⁻¹ • (X ^ n.succ).det • 1 = Y ^ n.succ * (↑hy'.unit⁻¹ • (Y ^ n.succ).adjugate * A)

Tactic:
← Matrix.mul_assoc,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ A * ↑hx'.unit⁻¹ • (X ^ n.succ).det • 1 = Y ^ n.succ * ↑hy'.unit⁻¹ • (Y ^ n.succ).adjugate * A
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
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ ↑n)ᴴ = Aᴴ ^ ↑n

Tactic:
by rw [zpow_natCast, zpow_natCast, conjTranspose_pow]

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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
⊢ (cartanMatrixIn S b).Nondegenerate

Tactic:
obtain ⟨B, hB⟩ : ∃ B : P.InvariantForm, B.form.Nondegenerate :=
    ⟨P.toInvariantForm, P.rootForm_nondegenerate⟩
  replace hB : ((2 : R) • B.form.toMatrix b.toWeightBasis).Nondegenerate := by
    rwa [Matrix.Nondegenerate.smul_iff two_ne_zero, LinearMap.BilinForm.nondegenerate_toMatrix_iff]
  have aux : (Matrix.diagonal fun i : b.support ↦ B.form (P.root i) (P.root i)).Nondegenerate := by
    rw [Matrix.nondegenerate_iff_det_ne_zero, Matrix.det_diagonal, Finset.prod_ne_zero_iff]
    aesop
  rw [← cartanMatrixIn_mul_diagonal_eq (S := S), Matrix.Nondegenerate.mul_iff_right aux,
    Matrix.nondegenerate_iff_det_ne_zero, ← (algebraMap S R).mapMatrix_apply,
    ← RingHom.map_det, ne_eq, FaithfulSMul.algebraMap_eq_zero_iff] at hB
  rwa [Matrix.nondegenerate_iff_det_ne_zero]

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

Goal state before:
pp: case inr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
hx : f x = μ • x
hne : x ≠ 0
⊢ ((aeval f) p) x = eval μ p • x

Tactic:
· exact aeval_apply_of_hasEigenvector ⟨mem_eigenspace_iff.mpr hx, hne⟩

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

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
w : M
H : w ∈ (f.genEigenspace μ) 1
ne0 : w ≠ 0
⊢ eval μ (minpoly R f) • w = 0

Tactic:
← aeval_apply_of_hasEigenvector ⟨H, ne0⟩

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
w : M
H : w ∈ (f.genEigenspace μ) 1
ne0 : w ≠ 0
⊢ ((aeval f) (minpoly R f)) w = 0
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
S : Type u_5
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra S R
P✝ : RootPairing ι R M N
inst✝¹⁵ : P✝.IsValuedIn S
b✝ : P✝.Base
inst✝¹⁴ : P✝.IsCrystallographic
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
inst✝² : Finite ι₂
inst✝¹ : P₂.IsRootSystem
inst✝ : P₂.IsReduced
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
f : M ≃ₗ[R] M₂ := b.toWeightBasis.equiv b₂.toWeightBasis e
m : M
h : f m ∈ range ⇑P₂.root
⊢ ∀ (i j : ↥b₂.support), b.cartanMatrix (e.symm i) (e.symm j) = b₂.cartanMatrix i j

Tactic:
simp [(he _ _).symm]

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

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
a : S
ha : a ∈ Set.Ici (↑(n + 1) - 1)
⊢ ∀ ⦃b : S⦄,
    b ∈ Set.Ici (↑(n + 1) - 1) →
      a ≤ b → (fun x ↦ eval x (descPochhammer S (n + 1))) a ≤ (fun x ↦ eval x (descPochhammer S (n + 1))) b

Tactic:
b

Goal state after:
case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
a : S
ha : a ∈ Set.Ici (↑(n + 1) - 1)
b : S
⊢ b ∈ Set.Ici (↑(n + 1) - 1) →
    a ≤ b → (fun x ↦ eval x (descPochhammer S (n + 1))) a ≤ (fun x ↦ eval x (descPochhammer S (n + 1))) b
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₂
y : ↥(prod eι b₁ b₂)
hy : y ∈ prodCartan eι b₁ b₂
x : ↥H₁
⊢ ⁅(↑y).1, ↑x⁆ = 0

Tactic:
have := b₁.isLieAbelian_cartan
  induction hy using lieSpan_induction with
  | mem u hu =>
    obtain ⟨i, rfl⟩ := hu
    suffices ⁅b₁.h' i, x⁆ = 0 by simpa [Subtype.ext_iff, Basis.h'] using this
    apply trivial_lie_zero
  | zero => simp
  | add u v hu hv hu' hv' => simp [hu', hv']
  | smul t u hu hu' => simp [hu']
  | lie u v hu hv hu' hv' => simp [hu', hv']

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✝ : Nontrivial L₂
this✝⁴ : Fintype ι₁
this✝³ : Fintype ι₂
this✝² : H₁.IsCartanSubalgebra
this✝¹ : H₂.IsCartanSubalgebra
this✝ : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
this : ∀ (x : ↥H₁ × ↥H₂) (hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂), ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂
x : ↥H₁ × ↥H₂
⊢ (↑x.1, ↑x.2) ∈ prod eι b₁ b₂

Tactic:
simp [contra]

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
this : ∀ (f : Dual ℚ ↥E), f = 0
⊢ s = 0

Tactic:
suffices ∀ ν, s.HasEigenvalue ν → ν = 0 from hs_ss.eq_zero_iff_forall_eigenvalue.mpr this
    intro ν hν
    have : Nontrivial (s.eigenspace ν) :=
      Submodule.nontrivial_iff_ne_bot.mpr (hasEigenvalue_iff.mp hν)
    replace hν : ν ∈ E := Submodule.subset_span ⟨⟨ν, ⟨0, finrank_pos⟩⟩, rfl⟩
    have : Subsingleton E := (subsingleton_dual_iff ℚ).mp ⟨by aesop⟩
    simpa using! Subsingleton.elim (⟨ν, hν⟩ : E) 0

Goal state after:
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 := 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
⊢ y ∈ (dx ^ (k + 1)).ker → ((ad R L) x ^ (k + 1)) (N.subtype y) = 0

Tactic:
generalize k + 1 = k

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
k : ℕ
⊢ y ∈ (dx ^ k).ker → ((ad R L) x ^ k) (N.subtype y) = 0
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun d ↦ d.support.biUnion fun i ↦ (f i).vars) ⊆ φ.vars.biUnion fun i ↦ (f i).vars

Tactic:
intro j
    simp_rw [Finset.mem_biUnion]
    rintro ⟨d, hd, ⟨i, hi, hj⟩⟩
    exact ⟨i, (mem_vars_iff_mem_support _).mpr ⟨d, hd, hi⟩, hj⟩

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)) →
        (∀ i ∈ insert a s, IsWeightedHomogeneous w (φ i) (n i)) →
          IsWeightedHomogeneous w (∏ i ∈ insert a s, φ i) (∑ i ∈ insert a s, n i)

Tactic:
intro i s his IH h

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (∏ i ∈ insert i s, φ i) (∑ i ∈ insert i s, n i)
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
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h : ∀ x ∈ I, ∀ y ∈ DI, ((killingForm R L) x) y = 0
DDI : LieIdeal R L := ⁅DI, DI⁆
⊢ LieModule.traceForm R (↥DI) L = 0

Tactic:
ext ⟨x, hx⟩ ⟨y, hy⟩

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
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h : ∀ x ∈ I, ∀ y ∈ DI, ((killingForm R L) x) y = 0
DDI : LieIdeal R L := ⁅DI, DI⁆
x : L
hx : x ∈ DI
y : L
hy : y ∈ DI
⊢ ((LieModule.traceForm R (↥DI) L) ⟨x, hx⟩) ⟨y, hy⟩ = (0 ⟨x, hx⟩) ⟨y, hy⟩
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
x✝ : A
h : x✝ ∈ Subtype.val '' Subtype.val ⁻¹' ↑I
this : Subtype.val '' Subtype.val ⁻¹' ↑I = ofPred (IsHomogeneousElem 𝒜) ∩ ↑I
⊢ IsHomogeneousElem 𝒜 x✝

Tactic:
exact (cast congr(_ ∈ $this) h).1

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 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (InfSet.sInf ℐ)

Tactic:
rw [sInf_eq_iInf]
  exact iInf₂ h

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: case neg
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
j : n
h : ¬i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

Tactic:
· simp only [h, ↓reduceIte, map_zero, zero_sub, (isHomogeneous_X _ _).neg]

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)) →
        (∀ i ∈ insert a s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ insert a s, φ i).IsHomogeneous (∑ i ∈ insert a s, n i)

Tactic:
intro i s his IH h

Goal state after:
case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, (φ i_1).IsHomogeneous (n i_1)
⊢ (∏ i ∈ insert i s, φ i).IsHomogeneous (∑ i ∈ insert i s, n i)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
⊢ (weightedHomogeneousComponent w n) φ = 0

Tactic:
classical
  rw [weightedHomogeneousComponent_apply, sum_eq_zero]
  intro d hd
  rw [Finset.mem_filter] at hd
  exfalso
  apply lt_irrefl n
  nth_rw 1 [← hd.2]
  exact lt_of_le_of_lt (le_weightedTotalDegree w hd.1) h

Goal state after:
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 n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = n then coeff x p else 0) = coeff x 0

Tactic:
if_neg

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 n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ 0 = coeff x 0

case neg.hnc
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬(weight w) x = n