mathlib-initiative/mathlib-tactics huggingface dataset:
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
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : 1 + ↑q.natDegree ≤ ↑q.natDegree
⊢ False

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
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : 1 + q.degree ≤ q.degree
⊢ q ≠ 0

Tactic:
]

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
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : 1 + ↑q.natDegree ≤ ↑q.natDegree
⊢ False

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
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : 1 + q.degree ≤ q.degree
⊢ q ≠ 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
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
l : ↥b.support
hl : p l
hx : P.root ↑l ∈ ⇑P.root ∘ Subtype.val '' {i | p i}
hk : (P.coroot' ↑k) (P.root ↑l) ≠ 0
⊢ ¬P.pairing ↑l ↑k = 0

Tactic:
]

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
l : ↥b.support
hl : p l
hx : P.root ↑l ∈ ⇑P.root ∘ Subtype.val '' {i | p i}
hk : (P.coroot' ↑k) (P.root ↑l) ≠ 0
⊢ ¬P.pairing ↑l ↑k = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ ¬1 = ⊥

Tactic:
]

Goal state after:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ ¬1 = ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0)) =
    LinearMap.ker (eval₂ (algebraMap K (End K V)) f (q.leadingCoeff • X + C (q.coeff 0)))

Tactic:
]

Goal state after:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0)) =
    LinearMap.ker (eval₂ (algebraMap K (End K V)) f (q.leadingCoeff • X + C (q.coeff 0)))
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker ((aeval f) q) = LinearMap.ker ((aeval f) q)

pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ q.degree = 1

Tactic:
]

Goal state after:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ q.degree = 1
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Field R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
⊢ (spectrum R ((toLinAlgEquiv (Pi.basisFun R n)) A)).Finite

Tactic:
]

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : Field R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
⊢ (spectrum R ((toLinAlgEquiv (Pi.basisFun R n)) A)).Finite
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: case cons
α : Type u_1
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ (f a)! * ∏ x ∈ s, (f x)! ∣ (f a + ∑ x ∈ s, f x)!

Tactic:
]

Goal state after:
case cons
α : Type u_1
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ (f a)! * ∏ x ∈ s, (f x)! ∣ (f a + ∑ x ∈ s, f x)!
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: n : ℕ
⊢ n.succ * ∏ i ∈ range n, (i + 1) = (n + 1) * ∏ x ∈ range n, (x + 1)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: n k : ℕ
⊢ (n + k) * ∏ i ∈ range k, (n + i) = (n + k) * ∏ x ∈ range k, (n + x)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: n k : ℕ
⊢ (n - k) * ∏ i ∈ range k, (n - i) = (n - k) * ∏ x ∈ range k, (n - x)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.BigOperators

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

Tactic:
]

Goal state after:
k : ℕ
n : ℤ
⊢ (∏ i ∈ range k, (n + ↑i) % ↑k !) % ↑k ! = 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
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
hq_notMem : ∀ (k : ↥b.support), P.root ↑k ∉ q → q ≤ LinearMap.ker (P.coroot' ↑k)
⊢ ∀ i ∈ b.support, q ∈ invtSubmodule ↑(P.reflection i)

Tactic:
]

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
hq_notMem : ∀ (k : ↥b.support), P.root ↑k ∉ q → q ≤ LinearMap.ker (P.coroot' ↑k)
⊢ ∀ i ∈ b.support, q ∈ invtSubmodule ↑(P.reflection i)
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
x : ℕ
hx : n % ↑k ! = ↑x
hdivk : ↑k ! ∣ ∏ x_1 ∈ range k, (↑x + ↑x_1)
⊢ ↑k ! ∣ ∏ i ∈ range k, (↑x + ↑i)

Tactic:
]

Goal state after:
k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
x : ℕ
hx : n % ↑k ! = ↑x
hdivk : ↑k ! ∣ ∏ x_1 ∈ range k, (↑x + ↑x_1)
⊢ ↑k ! ∣ ∏ i ∈ range k, (↑x + ↑i)
Module: Mathlib.Data.Nat.Factorial.SuperFactorial

Goal state before:
pp: n : ℕ
⊢ (n + 1) * n ! * sf n = n.succ * n ! * sf n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.SuperFactorial

Goal state before:
pp: n : ℕ
⊢ (n + 1)! * sf n = n.succ ! * sf n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.SuperFactorial

Goal state before:
pp: n : ℕ
⊢ sf 4 * n = sf (2 + 2) * n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.SuperFactorial

Goal state before:
pp: n : ℕ
⊢ (∏ i ∈ range (2 * n), (2 * i + 1)!) ^ 2 * (2 ^ n) ^ 2 * (2 * n)! =
    (∏ i ∈ range (2 * n), (2 * i + 1)!) ^ 2 * (2 ^ n) ^ 2 * (2 * n)!

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), P.root ↑k ∈ q ↔ p k
hq_notMem : ∀ (k : ↥b.support), P.root ↑k ∉ q → q ≤ LinearMap.ker (P.coroot' ↑k)
k : ι
hkb : k ∈ b.support
x : M
hx : x ∈ q
⊢ x - (P.coroot' k) x • P.root k ∈ q

Tactic:
]

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
hq_notMem : ∀ (k : ↥b.support), P.root ↑k ∉ q → q ≤ LinearMap.ker (P.coroot' ↑k)
k : ι
hkb : k ∈ b.support
x : M
hx : x ∈ q
⊢ x - (P.coroot' k) x • P.root k ∈ q
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
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ b.h i ∈ lieSpan K L (range b.h)

Tactic:
]

Goal state after:
ι : 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
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ b.h i ∈ lieSpan K L (range b.h)
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
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
h_mem : ⁅b.e i, b.f i⁆ ∈ H
h_eq : b.h' i = ⟨⁅b.e i, b.f i⁆, h_mem⟩
⊢ ⟨⁅b.e i, b.f i⁆, h_mem⟩ ∈ corootSpace ⇑(Weight.toLinear K (↥H) L ↑(b.baseSupp' i))

Tactic:
]

Goal state after:
ι : 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
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
h_mem : ⁅b.e i, b.f i⁆ ∈ H
h_eq : b.h' i = ⟨⁅b.e i, b.f i⁆, h_mem⟩
⊢ ⟨⁅b.e i, b.f i⁆, h_mem⟩ ∈ corootSpace ⇑(Weight.toLinear K (↥H) L ↑(b.baseSupp' i))
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
this : (reindex b.baseSupportEquiv.symm b.baseSupportEquiv.symm) b.base.cartanMatrix = b.A
⊢ (reindex b.baseSupportEquiv b.baseSupportEquiv).symm b.base.cartanMatrix = b.A

Tactic:
]

Goal state after:
ι : 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
this : (reindex b.baseSupportEquiv.symm b.baseSupportEquiv.symm) b.base.cartanMatrix = b.A
⊢ (reindex b.baseSupportEquiv b.baseSupportEquiv).symm b.base.cartanMatrix = b.A
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
]

Goal state after:
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
⊢ 1 = 1

Tactic:
]

Goal state after:
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
i j : ι
⊢ (rootSystem H).pairing ↑(b.baseSupportEquiv.symm.symm i) ↑(b.baseSupportEquiv.symm.symm j) =
    (algebraMap ℤ K) (b.A i j)

Tactic:
]

Goal state after:
ι : 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
i j : ι
⊢ (rootSystem H).pairing ↑(b.baseSupportEquiv.symm.symm i) ↑(b.baseSupportEquiv.symm.symm j) =
    (algebraMap ℤ K) (b.A i j)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
t : T
⊢ eval t (map f (ascPochhammer S n)) = eval₂ f t (ascPochhammer S n)

Tactic:
]

Goal state after:
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
t : T
⊢ eval t (map f (ascPochhammer S n)) = eval₂ f t (ascPochhammer S n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝² : Semiring S
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
p : R[X]
inst✝ : Algebra R S
x : S
⊢ eval₂ (algebraMap R S) x ((ascPochhammer R n).comp p) = eval₂ (algebraMap R S) x ((ascPochhammer R n).comp p)

Tactic:
]

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
this : f' = g'
⊢ ∑ j ∈ b.support, f j • P.root j = ∑ j ∈ b.support, g j • P.root j

Tactic:
]

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
this : f' = g'
⊢ ∑ j ∈ b.support, f j • P.root j = ∑ j ∈ b.support, g j • P.root j
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
]

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
k : ι
hk : k ∈ b.support
this : f k = g k
⊢ g k • P.root k = g k • P.root k

Tactic:
]

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (ascPochhammer S n) * (k + ↑n) = eval k (ascPochhammer S n) * (k + ↑n)

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (↑n + X + 1) * (ascPochhammer ℕ n).comp (X + 1) = (X + (↑n + 1)) * (ascPochhammer ℕ n).comp (X + 1)
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 + m) * (X + (↑n + ↑m)) = ascPochhammer S (n + m) * (X + (↑n + ↑m))

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ eval n 1 = n.ascFactorial 0

Tactic:
eval_one,

Goal state after:
n : ℕ
⊢ 1 = n.ascFactorial 0
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: n : ℕ
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: n t : ℕ
⊢ (n + t) * n.ascFactorial t = (n + t) * n.ascFactorial t

Tactic:
]

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
n k : ℕ
⊢ ↑(n.ascFactorial k) = ↑(n.ascFactorial k)

Tactic:
]

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

Goal state before:
pp: a b : ℕ
⊢ a.ascFactorial b = a.ascFactorial b

Tactic:
]

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑((a + b - 1).descFactorial b) = ↑((a + b - 1).descFactorial b)

Tactic:
]

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

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

pp: S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
this : (X + ↑n).natDegree = 1
⊢ ascPochhammer S n ≠ 0

Tactic:
]

Goal state after:
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
this : (X + ↑n).natDegree = 1
⊢ ascPochhammer S n ≠ 0
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case zero
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
⊢ 0 < eval s (ascPochhammer S 0)

Tactic:
simp only [ascPochhammer_zero, eval_one]

Goal state after:
case zero
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
⊢ 0 < 1
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n) * (s + ↑n)

Tactic:
]

Goal state after:
case succ
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n) * (s + ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ eval (↑a) (ascPochhammer S b) = eval (↑a) (ascPochhammer S b)

Tactic:
]

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)

Tactic:
]

Goal state after:
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ.inl
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : a ≤ b
⊢ ↑0 = ↑0

pp: S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : a ≤ b
⊢ a - b + b ≤ b

Tactic:
]

Goal state after:
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : a ≤ b
⊢ a - b + b ≤ b
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : a ≤ b
⊢ b ≤ b

Tactic:
]

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

Goal state before:
pp: case succ.inr
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : b ≤ a
⊢ ↑(a.descFactorial (b + 0).succ) = ↑(a.descFactorial (b + 0).succ)

Tactic:
]

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
a : ℕ
⊢ eval 1 (ascPochhammer S a) = eval 1 (ascPochhammer S a)

Tactic:
]

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

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

Tactic:
]

Goal state after:
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
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
k : ℤ
⊢ (algebraMap ℤ R) (eval k (descPochhammer ℤ n)) = eval₂ (algebraMap ℤ R) (↑k) (descPochhammer ℤ n)

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
k : ℤ
⊢ (algebraMap ℤ R) (eval k (descPochhammer ℤ n)) = eval₂ (algebraMap ℤ R) (↑k) (descPochhammer ℤ n)