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
f✝ : ι → ℤ
hf✝ : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
⊢ 0 < f

Tactic:
replace hf : ∑ j, f' j • P.root j ∈ AddSubmonoid.closure (P.root '' b.support) := by
    suffices ∑ j, f' j • P.root j = ∑ j ∈ b.support, f j • P.root j by rwa [this]
    rw [← b.support.sum_finset_coe]; rfl

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
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
hf : ∑ j, f' j • P.root ↑j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ 0 < f
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 : ι
⊢ chainTopCoeff i j = 0 ↔ ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j + P.root i ∉ range ⇑P.root

Tactic:
rw [← chainBotCoeff_reflectionPerm_left]
  simp [-chainBotCoeff_reflectionPerm_left, chainBotCoeff_eq_zero_iff]

Goal state after:
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
ε : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2
h₂ : abv (a₂ - b₂) < ε / 2
⊢ abv (a₁ - b₁ + (a₂ - b₂)) < ε

Tactic:
abv_add abv,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2
h₂ : abv (a₂ - b₂) < ε / 2
⊢ abv (a₁ - b₁) + abv (a₂ - b₂) < ε
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
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
⊢ abv ((a₁ - b₁) * b₂ + a₁ * (a₂ - b₂)) < ε

Tactic:
abv_add abv,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
⊢ abv ((a₁ - b₁) * b₂) + abv (a₁ * (a₂ - b₂)) < ε
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 : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f i - f k) < ε / 2

Tactic:
rw [abv_sub abv]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f k - f i) < ε / 2
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
⊢ abv (f j - f i) < ε

Tactic:
obtain ⟨h₁, h₂⟩ := hi _ le_rfl

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 (f i - ↑g i) < ε / 2 / 2
h₂ : ∀ k ≥ i, abv (↑g k - ↑g i) < ε / 2
⊢ abv (f j - f i) < ε
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
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)
⊢ False

Tactic:
rcases abv_pos_of_not_limZero hg' with ⟨a2, ha2, N2, hN2⟩

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
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)
⊢ False
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
⊢ K ≤ ↑f j

Tactic:
obtain ⟨h₁, h₂⟩ := hi _ le_rfl

Goal state after:
case inr.refine_1
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑f j
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
⊢ K ≤ ↑(-f) j

Tactic:
obtain ⟨h₁, h₂⟩ := hi _ le_rfl

Goal state after:
case inr.refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑(-f) j
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
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule ↑(P.reflection i)
i : ι
this✝ : InvolutiveNeg ι := P.indexNeg
this : ∀ (j : ι), P.reflection (-j) = P.reflection j
⊢ q ∈ invtSubmodule ↑(P.reflection i)

Tactic:
refine b.induction_reflect i (by simp_all) hq ?_

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
inst✝ : P.IsReduced
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule ↑(P.reflection i)
i : ι
this✝ : InvolutiveNeg ι := P.indexNeg
this : ∀ (j : ι), P.reflection (-j) = P.reflection j
⊢ ∀ (i j : ι),
    q ∈ invtSubmodule ↑(P.reflection i) → j ∈ b.support → q ∈ invtSubmodule ↑(P.reflection ((P.reflectionPerm j) i))
Module: Mathlib.Algebra.Star.Pi

Goal state before:
pp: I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst✝ : Star α
⊢ star (Sum.elim x y) = Sum.elim (star x) (star y)

Tactic:
ext x; cases x <;> simp only [Pi.star_apply, Sum.elim_inl, Sum.elim_inr]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ⟦f⟧ ≠ 0
⊢ ⟦f⟧ * (⟦f⟧)⁻¹ = 1

Tactic:
by
    simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf
    simp only [mk_eq_mk, hf, not_false_eq_true, inv_mk, mk_mul]
    exact Quotient.sound (CauSeq.mul_inv_cancel hf)

Goal state after:
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
h : f.lim = 0
hf : f ≈ const abv 0
⊢ f.LimZero

Tactic:
exact (limZero_congr hf).mpr (const_limZero.mpr rfl)

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

Goal state before:
pp: case mp
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
a✝ : Nontrivial R
i : n
⊢ 0 < star (v i) * v i → v i ≠ 0

Tactic:
rintro h hv
    simp [hv] at h

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A).IsHermitian ↔ A.IsHermitian

Tactic:
by
  rw [IsHermitian, IsHermitian, conjTranspose_comp', comp .. |>.injective.eq_iff]

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

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix l m R
B : Matrix m n R
⊢ (A * B).vec = (A * B * 1ᵀ).vec

pp: case hB
l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix l m R
B : Matrix m n R
⊢ ∀ (x : R) (i j : n), Commute x (1 i j)

Tactic:
transpose_one,

Goal state after:
l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix l m R
B : Matrix m n R
⊢ (A * B).vec = (A * B * 1).vec

case hB
l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix l m R
B : Matrix m n R
⊢ ∀ (x : R) (i j : n), Commute x (1 i j)
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_1
n : Type u_2
p : Type u_4
R : Type u_3
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq m
A : Matrix m n R
B : Matrix n p R
⊢ (A * B).vec = (1ᵀ * A * B).vec

pp: case hA
m : Type u_1
n : Type u_2
p : Type u_4
R : Type u_3
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq m
A : Matrix m n R
B : Matrix n p R
⊢ ∀ (x : R) (i j : m), Commute (1 i j) x

Tactic:
transpose_one,

Goal state after:
m : Type u_1
n : Type u_2
p : Type u_4
R : Type u_3
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq m
A : Matrix m n R
B : Matrix n p R
⊢ (A * B).vec = (1 * A * B).vec

case hA
m : Type u_1
n : Type u_2
p : Type u_4
R : Type u_3
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq m
A : Matrix m n R
B : Matrix n p R
⊢ ∀ (x : R) (i j : m), Commute (1 i j) x
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
A : Matrix n n R
B : Matrix n m R
hA : A.PosDef
hB : Function.Injective B.mulVec
x : m → R
hx : x ≠ 0
this : B *ᵥ x ≠ 0
⊢ 0 < star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x

Tactic:
simpa only [star_mulVec, dotProduct_mulVec, vecMul_vecMul] using hA.dotProduct_mulVec_pos this

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

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : QuadraticMap.PosDef Q
⊢ Q.toMatrix'.PosDef

Tactic:
rw [← Q.toQuadraticMap_associated ℝ,
    ← (LinearMap.toMatrix₂' ℝ).left_inv (Q.associatedHom ℝ)] at hQ
  exact .of_toQuadraticForm' (isSymm_toMatrix' Q) hQ

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
f : End R M
μ : R
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
⊢ f.HasEigenvalue μ

Tactic:
obtain ⟨v, hv⟩ : ∃ v : M, q.aeval f v ≠ 0 := by
    by_contra! h_contra
    have := minpoly.min R f
      ((monic_X_sub_C μ).of_mul_monic_left (hq ▸ minpoly.monic (Algebra.IsIntegral.isIntegral f)))
      (LinearMap.ext h_contra)
    rw [hq, degree_mul, degree_X_sub_C, degree_eq_natDegree] at this
    · norm_cast at this; grind
    · rintro rfl
      exact minpoly.ne_zero (Algebra.IsIntegral.isIntegral f) (mul_zero (X - C μ) ▸ hq)

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
μ : R
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
v : M
hv : ((aeval f) q) v ≠ 0
⊢ f.HasEigenvalue μ
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
this : (X + 1).leadingCoeff = 1
⊢ (X * (ascPochhammer S n).comp (X + 1)).Monic

Tactic:
Monic.def,

Goal state after:
case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
this : (X + 1).leadingCoeff = 1
⊢ (X * (ascPochhammer S n).comp (X + 1)).leadingCoeff = 1
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
⊢ b.base.cartanMatrix = (reindex b.baseSupportEquiv b.baseSupportEquiv) b.A

Tactic:
by
  suffices b.base.cartanMatrix.reindex b.baseSupportEquiv.symm b.baseSupportEquiv.symm = b.A by
    rwa [← (reindex b.baseSupportEquiv b.baseSupportEquiv).symm_apply_eq]
  ext i j
  apply FaithfulSMul.algebraMap_injective ℤ K
  rw [reindex_apply, submatrix_apply, RootPairing.Base.algebraMap_cartanMatrixIn_apply]
  simp [← Weight.coe_coe]

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

Goal state before:
pp: case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : ascPochhammer S n * (ascPochhammer S m).comp (X + ↑n) = ascPochhammer S (n + m)
⊢ ascPochhammer S n * (ascPochhammer S m * (X + ↑m)).comp (X + ↑n) = ascPochhammer S (n + (m + 1))

Tactic:
Polynomial.mul_X_add_natCast_comp,

Goal state after:
case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : ascPochhammer S n * (ascPochhammer S m).comp (X + ↑n) = ascPochhammer S (n + m)
⊢ ascPochhammer S n * ((ascPochhammer S m).comp (X + ↑n) * (X + ↑n + ↑m)) = ascPochhammer S (n + (m + 1))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
n : ℕ
hn : (descPochhammer R n).Monic
h : (X - 1).leadingCoeff = 1
this : (X - 1).natDegree ≠ 0
⊢ (X * (descPochhammer R n).comp (X - 1)).Monic

Tactic:
Monic.def,

Goal state after:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
n : ℕ
hn : (descPochhammer R n).Monic
h : (X - 1).leadingCoeff = 1
this : (X - 1).natDegree ≠ 0
⊢ (X * (descPochhammer R n).comp (X - 1)).leadingCoeff = 1
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 : L₂), (∃ l, (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) l = (0, y)) → y = 0

Tactic:
intro y

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₂
y : L₂
⊢ (∃ l, (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) l = (0, y)) → y = 0
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ ∑ j, (-1) ^ ↑j * W 0 j * (W.submatrix succ j.succAbove).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
Finset.sum_eq_single 0 _ (by simp)

Goal state after:
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ (-1) ^ ↑0 * W 0 0 * (W.submatrix succ (succAbove 0)).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ ∀ b ∈ univ, b ≠ 0 → (-1) ^ ↑b * W 0 b * (W.submatrix succ b.succAbove).det = 0
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
⊢ Surjective ⇑p₁

Tactic:
have h₁ : range b₁.e = range (p₁ ∘ prodE eι b₁ b₂) := rfl

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₂)
⊢ Surjective ⇑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₂
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₂
⊢ prod eι b₁ b₂ < ⊤

Tactic:
have := Fintype.ofFinite ι₁

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✝ : Nontrivial L₂
this : Fintype ι₁
⊢ prod eι b₁ b₂ < ⊤
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case e'_2
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ (v x✝¹).descFactorial ↑x✝ = (↑x✝).factorial * (v x✝¹).choose ↑x✝

Tactic:
exact Nat.descFactorial_eq_factorial_mul_choose _ _

Goal state after:
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 : L
⊢ ∀ {x_1 y : L} (x_2 : ℕ),
    ((ad R L) x ^ x_2) x_1 = 0 → ∀ (x_3 : ℕ), ((ad R L) x ^ x_3) y = 0 → ∃ k, ((ad R L) x ^ k) ⁅x_1, y⁆ = 0

Tactic:
intro y

Goal state after:
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 : L
⊢ ∀ {y_1 : L} (x_1 : ℕ),
    ((ad R L) x ^ x_1) y = 0 → ∀ (x_2 : ℕ), ((ad R L) x ^ x_2) y_1 = 0 → ∃ k, ((ad R L) x ^ k) ⁅y, y_1⁆ = 0
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ (engel R x).normalizer ≤ engel R x

Tactic:
intro y

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
⊢ y ∈ (engel R x).normalizer → y ∈ engel R x
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case a
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 : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ (dx ^ (k + 1)).ker ≤ Submodule.comap N.subtype (engel R x).toSubmodule

Tactic:
intro y

Goal state after:
case a
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 : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
y : ↥N
⊢ y ∈ (dx ^ (k + 1)).ker → y ∈ Submodule.comap N.subtype (engel R x).toSubmodule