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 : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
pos : 0 < f
contra : ∀ i ∈ b.support, f i ≤ 0
j : ι
⊢ f j = 0

Tactic:
by_cases hj : j ∈ f.support

Goal state after:
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
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
pos : 0 < f
contra : ∀ i ∈ b.support, f i ≤ 0
j : ι
hj : j ∈ Function.support f
⊢ f j = 0

case neg
ι : 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
contra : ∀ i ∈ b.support, f i ≤ 0
j : ι
hj : j ∉ Function.support f
⊢ f j = 0
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 : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
neg : f < 0
contra : ∀ i ∈ b.support, 0 ≤ f i
j : ι
⊢ f j = 0

Tactic:
by_cases hj : j ∈ f.support

Goal state after:
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
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
neg : f < 0
contra : ∀ i ∈ b.support, 0 ≤ f i
j : ι
hj : j ∈ Function.support f
⊢ f j = 0

case neg
ι : 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
contra : ∀ i ∈ b.support, 0 ≤ f i
j : ι
hj : j ∉ Function.support f
⊢ f j = 0
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 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
ha₁ : abv a₁ < max 1 (max K₁ K₂)
hb₂ : abv b₂ < max 1 (max K₁ K₂)
⊢ abv (a₁ * a₂ - b₁ * b₂) < ε

Tactic:
set M := max 1 (max K₁ K₂)

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₁ * a₂ - b₁ * b₂) < ε
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
f : CauSeq β abv
this : mk f = 0 ↔ (f - 0).LimZero
⊢ mk f = 0 ↔ f.LimZero

Tactic:
rwa [sub_zero] at this

Goal state after:
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|
h₁ : K ≤ -↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ ↑f j - ?inr.refine_2✝ ≤ -?inr.refine_2✝

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|
h₁ : K ≤ -↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ α

Tactic:
exact le_trans (le_of_lt (abs_lt.1 <| h₂ _ ij).2) h₁

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

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ mk f ≤ mk g ↔ f ≤ g

Tactic:
simp only [le_def', mk_lt, mk_eq]; rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
| f 1

Tactic:
← one_pow 2,

Goal state after:
R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
| f (1 ^ 2)
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 ↔ ∀ (i j : m) (i' j' : n), star (A j i j' i') = A i j i' j'

Tactic:
by
  simp [IsHermitian.ext_iff]
  grind

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]

Goal state after:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ (n + 1)).det
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 m
inst✝¹ : Finite n
inst✝ : StarOrderedRing R
A : Matrix m n R
this : Fintype n
x : n → R
⊢ 0 ≤ star x ⬝ᵥ (Aᴴ * A) *ᵥ x

Tactic:
← mulVec_mulVec,

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : Fintype m
inst✝¹ : Finite n
inst✝ : StarOrderedRing R
A : Matrix m n R
this : Fintype n
x : n → R
⊢ 0 ≤ star x ⬝ᵥ Aᴴ *ᵥ A *ᵥ 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 m
inst✝¹ : Finite n
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (Aᴴ * A).PosSemidef

Tactic:
have := Fintype.ofFinite n
  refine .of_dotProduct_mulVec_nonneg (isHermitian_conjTranspose_mul_self _) fun x => ?_
  rw [← mulVec_mulVec, dotProduct_mulVec, vecMul_conjTranspose, star_star]
  exact Finset.sum_nonneg fun i _ => star_mul_self_nonneg _

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
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
⊢ μ * ∑ i, d i * |v i| ^ 2 ≤ |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|

Tactic:
← mulVec_mulVec,

Goal state after:
ι : 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
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
⊢ μ * ∑ i, d i * |v i| ^ 2 ≤ |v| ⬝ᵥ diagonal d *ᵥ N *ᵥ |v|
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case refine_2
ι : 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✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
_i : Fintype ι
d : ↥b.support → ℤ := fun i ↦ ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)
hd : d = fun i ↦ ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)
aux : (P.posRootForm ℤ).posForm.IsSymm
⊢ ((LinearMap.BilinForm.toMatrix b.toWeightBasisInt) (P.posRootForm ℤ).posForm).PosDef

Tactic:
← LinearMap.BilinForm.posDef_toQuadraticMap_iff_matrix _ _ aux

Goal state after:
case refine_2
ι : 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✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
_i : Fintype ι
d : ↥b.support → ℤ := fun i ↦ ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)
hd : d = fun i ↦ ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)
aux : (P.posRootForm ℤ).posForm.IsSymm
⊢ (LinearMap.BilinMap.toQuadraticMap (P.posRootForm ℤ).posForm).PosDef
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
x : M
hx : x ∈ q
hk : (P.coroot' ↑k) x ≠ 0
⊢ P.root ↑k ∈ q

Tactic:
hq_mem

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 k
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n : ℕ
hn : (descPochhammer R n).natDegree = n
this : (X - ↑n).natDegree = 1
⊢ (descPochhammer R (n + 1)).natDegree = n + 1

Tactic:
descPochhammer_succ_right,

Goal state after:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n : ℕ
hn : (descPochhammer R n).natDegree = n
this : (X - ↑n).natDegree = 1
⊢ (descPochhammer R n * (X - ↑n)).natDegree = n + 1
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝ : Ring S
n : ℕ
k : S
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - ↑n)

Tactic:
descPochhammer_succ_right,

Goal state after:
S : Type u_1
inst✝ : Ring S
n : ℕ
k : S
⊢ eval k (descPochhammer S n * (X - ↑n)) = eval k (descPochhammer S n) * (k - ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ descPochhammer ℤ (n + 1) = (ascPochhammer ℤ (n + 1)).comp (X - ↑n)

Tactic:
descPochhammer_succ_right,

Goal state after:
case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ descPochhammer ℤ n * (X - ↑n) = (ascPochhammer ℤ (n + 1)).comp (X - ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ (ascPochhammer ℤ n).comp (X - ↑n + 1) * (X - ↑n) = ((ascPochhammer ℤ n).comp (X + 1) * X).comp (X - ↑n)

Tactic:
mul_X_comp,

Goal state after:
case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ (ascPochhammer ℤ n).comp (X - ↑n + 1) * (X - ↑n) = ((ascPochhammer ℤ n).comp (X + 1)).comp (X - ↑n) * (X - ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
n m : ℕ
ih : descPochhammer R n * (descPochhammer R m).comp (X - ↑n) = descPochhammer R (n + m)
⊢ descPochhammer R n * (descPochhammer R (m + 1)).comp (X - ↑n) = descPochhammer R (n + (m + 1))

Tactic:
descPochhammer_succ_right,

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
n m : ℕ
ih : descPochhammer R n * (descPochhammer R m).comp (X - ↑n) = descPochhammer R (n + m)
⊢ descPochhammer R (n + m) * (X - ↑n - ↑m) = descPochhammer R (n + m + 1)

Tactic:
descPochhammer_succ_right,

Goal state after:
case succ
R : Type u
inst✝ : Ring R
n m : ℕ
ih : descPochhammer R n * (descPochhammer R m).comp (X - ↑n) = descPochhammer R (n + m)
⊢ descPochhammer R (n + m) * (X - ↑n - ↑m) = descPochhammer R (n + m) * (X - ↑(n + m))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) = (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))

Tactic:
descPochhammer_succ_right,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) = (-1) ^ (k + 1) * eval r (descPochhammer R k * (X - ↑k))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
⊢ eval (↑n) (descPochhammer R (k + 1)) = ↑(n.descFactorial (k + 1))

Tactic:
descPochhammer_succ_right,

Goal state after:
case succ
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
⊢ eval (↑n) (descPochhammer R k * (X - ↑k)) = ↑(n.descFactorial (k + 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₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
i : ι₁
⊢ ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆ = prodH eι b₁ b₂ i

Tactic:
by simp [Subtype.ext_iff, (b₁.sl2 i).lie_e_f, (b₂.sl2 (eι i)).lie_e_f]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case a
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
⊢ (⇑derivative)^[k] (∏ j ∈ s.erase i, (X - C (v j))) =
    ↑k.factorial * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ j ∈ t, (X - C (v j))

Tactic:
have hvs' := hvs.mono (coe_subset.mpr (erase_subset i s))

Goal state after:
case a
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v ↑(s.erase i)
⊢ (⇑derivative)^[k] (∏ j ∈ s.erase i, (X - C (v j))) =
    ↑k.factorial * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ j ∈ t, (X - C (v j))
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)
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
rw [leadingCoeff, natDegree_eq_of_degree_eq_some hdegree]

Goal state after:
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)
⊢ P.coeff (#s - 1) = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
i j : ChooseBasisIndex R M₁
⊢ (LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ) i j = (LinearMap.toMatrix b b) φ i j

Tactic:
simp [LinearMap.toMatrix]

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
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x ∈ antidiagonal c, coeff x.1 φ * coeff x.2 ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff d φ ≠ 0 → coeff e ψ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0

Tactic:
by_cases h : coeff d φ = 0 <;>
      simp_all only [Ne, not_false_iff, zero_mul, mul_zero]

Goal state after:
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:
by
  rw [degree_eq_weight_one] at hn
  exact isWeightedHomogeneous_monomial 1 d r hn

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ I ≤ (homogeneousHull 𝒜 I).toIdeal

Tactic:
intro r hr

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 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ r ∈ (homogeneousHull 𝒜 I).toIdeal
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
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ (coeLinearMap fun i ↦ weightedHomogeneousSubmodule R w i) x = ∑ᶠ (m : M), ↑(x m)

Tactic:
rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset]

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ (Function.support fun m ↦ ↑(x m)) ⊆ ↑(DFinsupp.support x)
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case e_f.hX
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
⊢ (bind₁ (toMvPolynomial (basis A b) (basis A bₘ.end) (baseChange A φ)))
      (toMvPolynomial (basis A bₘ.end) (basis A bₘ).end (tensorProduct R A M M) ij) =
    (MvPolynomial.map (algebraMap R A)) (toMvPolynomial b bₘ.end φ ij)

Tactic:
← toMvPolynomial_baseChange

Goal state after:
case e_f.hX
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
⊢ (bind₁ (toMvPolynomial (basis A b) (basis A bₘ.end) (baseChange A φ)))
      (toMvPolynomial (basis A bₘ.end) (basis A bₘ).end (tensorProduct R A M M) ij) =
    toMvPolynomial (basis A b) (basis A bₘ.end) (baseChange A φ) ij
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
⊢ (eval (Fin.cons 1 0)) F ≠ 0

Tactic:
have aux : ∀ i ∈ Finset.range n, constantCoeff ((finSuccEquiv R N F).coeff i) = 0 := by
    intro i hi
    rw [Finset.mem_range] at hi
    apply (hF.finSuccEquiv_coeff_isHomogeneous i (n - i) (by lia)).coeff_eq_zero
    simp only [map_zero]
    rw [← Nat.sub_ne_zero_iff_lt] at hi
    exact hi.symm

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
⊢ (eval (Fin.cons 1 0)) F ≠ 0
Module: Mathlib.Algebra.Lie.Matrix

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
⊢ (↑LinearMap.toMatrix').toFun ⁅T, S⁆ = ⁅(↑LinearMap.toMatrix').toFun T, (↑LinearMap.toMatrix').toFun S⁆

Tactic:
change f (T.comp S - S.comp T) = f T * f S - f S * f T

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
⊢ f (T ∘ₗ S - S ∘ₗ T) = f T * f S - f S * f T