mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ∀ (k : ι), P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k
⊢ (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ eval n (ascPochhammer ℕ 0) = n.ascFactorial 0

Tactic:
by

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

Goal state before:
pp: n t : ℕ
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)

Tactic:
by

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

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

Tactic:
by

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
⊢ (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix

Tactic:
by

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

Goal state before:
pp: a b : ℕ
⊢ eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: S : Type u
inst✝² : Semiring S
n : ℕ
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
⊢ (ascPochhammer S n).natDegree = n

Tactic:
by

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 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
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
this : ∀ (k : ι), P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k
x✝ : ↥b.support
⊢ ∀ (x : ι), x ∈ b.support ↔ ?m.483 x

Tactic:
by

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 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
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
this : ∀ (k : ι), P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k
⊢ (fun k ↦ P.pairingIn ℤ j ↑k) = g' ᵥ* b.cartanMatrix

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝ : Semiring S
n : ℕ
⊢ eval 1 (ascPochhammer S n) = ↑n !

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝ : Semiring S
r n : ℕ
⊢ ↑r ! * eval (↑r + 1) (ascPochhammer S n) = ↑(r + n)!

Tactic:
by

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

Goal state before:
pp: r : ℕ
⊢ 0 * eval (0 + 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)

Tactic:
by

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

Goal state before:
pp: r k : ℕ
⊢ (k + 1) * eval (k + 1 + 1) (ascPochhammer ℕ r) = (k + 1 + r) * eval (k + 1) (ascPochhammer ℕ r)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ descPochhammer R 1 = X

Tactic:
by

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

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

Tactic:
by

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 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
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
⊢ (fun k ↦ P.pairingIn ℤ j ↑k) = g' ᵥ* b.cartanMatrix

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
n : ℕ
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
⊢ (descPochhammer R n).Monic

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
T : Type v
inst✝ : Ring T
f : R →+* T
n : ℕ
⊢ map f (descPochhammer R n) = descPochhammer T n

Tactic:
by

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 g : ι → ℤ
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
hg : (fun k ↦ P.pairingIn ℤ j ↑k) = g' ᵥ* b.cartanMatrix
this : Injective fun v ↦ v ᵥ* b.cartanMatrix
⊢ (fun v ↦ v ᵥ* b.cartanMatrix) f' = (fun v ↦ v ᵥ* b.cartanMatrix) g'

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
⊢ eval 0 (descPochhammer R n) = if n = 0 then 1 else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ eval 0 (descPochhammer R 0) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
h : n ≠ 0
⊢ eval 0 (descPochhammer R n) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
h : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
⊢ descPochhammer R (n + 1) = descPochhammer R n * (X - ↑n)

Tactic:
by

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
⊢ Injective fun i k ↦ P.pairingIn ℤ i ↑k

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
this : ∃ d ∈ p, ∀ (i : ι ⊕ ↑{(i, j) | i ≠ j}), (f i) d ≠ 0
⊢ ∃ d ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)

Tactic:
obtain ⟨d, hp, hf⟩ := this

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
d : ι → K
hp : d ∈ p
hf : ∀ (i : ι ⊕ ↑{(i, j) | i ≠ j}), (f i) d ≠ 0
⊢ ∃ d ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
this : ∃ d ∈ p, ∀ (i : ι ⊕ ↑{(i, j) | i ≠ j}), (f i) d ≠ 0
⊢ ∃ d ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
i j : ι
h : i ≠ j
⊢ ∃ k ∈ b.support, P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
n : ℕ
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (descPochhammer R n).natDegree = n

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
i j : ι
h : i ≠ j
k : ι
hk : k ∈ b.support
hk' : P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k
⊢ ¬(fun i ↦ ↑(P.pairingIn ℤ i k)) i = (fun i ↦ ↑(P.pairingIn ℤ i k)) j

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
⊢ ∃ d ∈ span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i)), (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)

Tactic:
by

Goal state after:
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:
by

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 ι
ι₂ : 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
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
m : M
hm : m ∈ range ⇑P.root
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
k : ↥b.support
this : ∀ (j : ↥b.support), (P.reflection ↑k ≪≫ₗ f) (P.root ↑j) = (f ≪≫ₗ P₂.reflection ↑(e k)) (P.root ↑j)
j : ↥b.support
⊢ ↑(P.reflection ↑k ≪≫ₗ f) (b.toWeightBasis j) = ↑(f ≪≫ₗ P₂.reflection ↑(e k)) (b.toWeightBasis j)

Tactic:
by

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

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

Tactic:
by

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 ι
ι₂ : 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
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
m : M
hm : m ∈ range ⇑P.root
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
k : ↥b.support
this : ∀ (j : ↥b.support), (P.reflection ↑k ≪≫ₗ f) (P.root ↑j) = (f ≪≫ₗ P₂.reflection ↑(e k)) (P.root ↑j)
⊢ P.reflection ↑k ≪≫ₗ f = f ≪≫ₗ P₂.reflection ↑(e k)

Tactic:
by

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 ι
ι₂ : 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
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
m : M
hm : m ∈ range ⇑P.root
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
k j : ↥b.support
this : P₂.pairing ↑(e j) ↑(e k) = P.pairing ↑j ↑k
⊢ (P.reflection ↑k ≪≫ₗ f) (P.root ↑j) = (f ≪≫ₗ P₂.reflection ↑(e k)) (P.root ↑j)

Tactic:
by

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

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

Tactic:
by

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 ι
ι₂ : 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
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
m : M
hm : m ∈ range ⇑P.root
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
k : ↥b.support
⊢ P.reflection ↑k ≪≫ₗ f = f ≪≫ₗ P₂.reflection ↑(e k)

Tactic:
by

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 ι
ι₂ : 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
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
this : ∀ (k : ↥b.support), P.reflection ↑k ≪≫ₗ f = f ≪≫ₗ P₂.reflection ↑(e k)
i j : ι
x✝ : f (P.root j) ∈ range ⇑P₂.root
k : ι₂
hk : P₂.root k = f (P.root j)
⊢ P₂.root ((P₂.reflectionPerm k) k) = f (P.root ((P.reflectionPerm j) j))

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 ι
ι₂ : 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
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
this : ∀ (k : ↥b.support), P.reflection ↑k ≪≫ₗ f = f ≪≫ₗ P₂.reflection ↑(e k)
i j k : ι
l : ι₂
hl : P₂.root l = f (P.root j)
hk : k ∈ b.support
⊢ f ((P.reflection k) (P.root j)) = (P₂.reflection ↑(e ⟨k, hk⟩)) (f (P.root j))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
⊢ eval (-r) (ascPochhammer R 0) = (-1) ^ 0 * eval r (descPochhammer R 0)

Tactic:
by

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 ι
ι₂ : 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
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
m : M
hm : m ∈ range ⇑P.root
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
⊢ f m ∈ range ⇑P₂.root

Tactic:
by

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

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

Tactic:
by

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₂
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₂
⊢ LieSubalgebra.map (LieEquiv.prodComm R L₂ L₁).toLieHom (prod eι.symm b₂ b₁) = prod eι b₁ b₂

Tactic:
by

Goal state after: