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
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
this : ¬HasEigenvalue (toLin' b.cartanMatrix) 4
i✝ x✝ : ↥b.support
⊢ (toLin' (4 - b.cartanMatrix) ∘ₗ LinearMap.single ℤ (fun i ↦ ℤ) i✝) 1 x✝ =
    ((-(toLin' b.cartanMatrix - 4 • 1)) ∘ₗ LinearMap.single ℤ (fun i ↦ ℤ) i✝) 1 x✝

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
d : ↥b.support → ℤ
hd : ∀ (i : ↥b.support), 0 < d i
hdS : (Matrix.diagonal d * b.cartanMatrix).PosDef
i : ↥b.support
⊢ b.cartanMatrix i i ≤ if i = i then 2 else 0

Tactic:
simp

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

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
c : R[X]ˣ
m : M
hm : ((aeval f) ↑c) m = 0
⊢ m = 0

Tactic:
by
    simpa [← mul_apply, ← aeval_mul] using congr(c⁻¹.1.aeval f $hm)

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i ∈ ∅, (f i)! ∣ (∑ i ∈ ∅, f i)!

Tactic:
simp

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 : ι
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⟩
x✝ : ↥H
z : L
hz : z ∈ H
⊢ (((toEnd K (↥H) L) ⟨z, hz⟩ - (b.baseSupp i) ⟨z, hz⟩ • 1) ^ 1) (b.e i) = 0

Tactic:
simp

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

Goal state before:
pp: case zero
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
⊢ (ascPochhammer S 0).Monic

Tactic:
simp

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

Goal state before:
pp: case zero
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
⊢ map f (ascPochhammer S 0) = ascPochhammer T 0

Tactic:
simp

Goal state after:
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:
Nat.cast_id

Goal state after:
S : Type u
inst✝ : Semiring S
n k : ℕ
⊢ (algebraMap ℕ S) (eval k (ascPochhammer ℕ n)) = (algebraMap ℕ S) (eval k (ascPochhammer ℕ n))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case zero
S : Type u
inst✝ : Semiring S
⊢ eval 0 (ascPochhammer S 0) = if 0 = 0 then 1 else 0

Tactic:
simp

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

Goal state before:
pp: S : Type u
inst✝ : Semiring S
⊢ eval 0 (ascPochhammer S 0) = 1

Tactic:
simp

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

Goal state before:
pp: case zero
S : Type u
inst✝ : Semiring S
⊢ ascPochhammer ℕ (0 + 1) = ascPochhammer ℕ 0 * (X + ↑0)

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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
⊢ a - b + b ≤ b

Tactic:
rw [tsub_eq_zero_iff_le.mpr h, zero_add]

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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
⊢ ∀ (j : ↥b.support), (P.reflection ↑k ≪≫ₗ f) (P.root ↑j) = (f ≪≫ₗ P₂.reflection ↑(e k)) (P.root ↑j)

Tactic:
intro j

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 ι
ι₂ : 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
⊢ (P.reflection ↑k ≪≫ₗ f) (P.root ↑j) = (f ≪≫ₗ P₂.reflection ↑(e k)) (P.root ↑j)
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
⊢ (P.reflection ↑k ≪≫ₗ f) (P.root ↑j) = (f ≪≫ₗ P₂.reflection ↑(e k)) (P.root ↑j)

Tactic:
suffices P₂.pairing (e j) (e k) = P.pairing j k by simp [reflection_apply, hf, this]

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 ι
ι₂ : 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
⊢ P₂.pairing ↑(e j) ↑(e k) = P.pairing ↑j ↑k
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case h₂
ι : 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 : ι
⊢ ∀ (i j : ι), f (P.root i) ∈ range ⇑P₂.root → j ∈ b.support → f (P.root ((P.reflectionPerm j) i)) ∈ range ⇑P₂.root

Tactic:
intro j

Goal state after:
case h₂
ι : 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 : ι
⊢ ∀ (j_1 : ι), f (P.root j) ∈ range ⇑P₂.root → j_1 ∈ b.support → f (P.root ((P.reflectionPerm j_1) j)) ∈ range ⇑P₂.root
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
⊢ vandermonde (Fin.cons v0 v) 0 j = Fin.cons (fun j ↦ v0 ^ ↑j) (fun i ↦ Fin.cons 1 fun j ↦ v i * vandermonde v i j) 0 j

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j : Fin (n + 1)
i : Fin n
⊢ vandermonde (Fin.cons v0 v) i.succ 0 =
    Fin.cons (fun j ↦ v0 ^ ↑j) (fun i ↦ Fin.cons 1 fun j ↦ v i * vandermonde v i j) i.succ 0

Tactic:
simp

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

Goal state before:
pp: case succ.inr.inl
R : Type u
inst✝ : Ring R
k : ℕ
ih : k < k → eval (-↑k) (ascPochhammer R k) = 0
h : k < k + 1
⊢ eval (-↑k) (ascPochhammer R k) * (-↑k + ↑k) = 0

Tactic:
simp

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₂
this : ∀ (y : L₂), (∃ l, (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) l = (0, y)) → y = 0
x✝ : L₁ × L₂
⊢ x✝ ∈ {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ↔ x✝ ∈ (fun i ↦ (b₁.h i, b₂.h (eι i))) '' univ

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
r : R
⊢ eval r (descPochhammer R 0) = ∏ j ∈ Finset.range 0, (r - ↑j)

Tactic:
simp

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

Goal state before:
pp: case zero
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : ↑0 - 1 ≤ s
⊢ (s - ↑0 + 1) ^ 0 ≤ eval s (descPochhammer S 0)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case zero
K : Type u_2
inst✝ : Field K
n : ℕ
v w : Fin 0 → K
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
simp

Goal state after:
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
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
i₀ : Fin (n + 1)
hi₀ : w i₀ ≠ 0
⊢ ∀ (i j : Fin (n + 1)), v j * w i - v i * w j = -(v i * w j - v j * w i)

Tactic:
simp

Goal state after:
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
i j : Fin n
⊢ W.submatrix succ succ i j = of (fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j) i j

Tactic:
simp only [projVandermonde_apply, val_zero, rev_zero, val_last, val_succ,
      val_castSucc, submatrix_apply, Function.comp_apply, rev_succ,
      W, r, rev_castSucc]

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
i j : Fin n
⊢ of
      (fun i ↦
        Fin.cons (v i ^ 0 * w i ^ n) fun j ↦
          v i ^ (↑j + 1) * w i ^ ↑j.rev - v 0 / w 0 * (v i ^ ↑j * w i ^ (↑j.rev + 1)))
      i.succ j.succ =
    of (fun i j ↦ (v i.succ - v 0 / w 0 * w i.succ) * (v i.succ ^ ↑j * w i.succ ^ ↑j.rev)) i j
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₂
h₁ :
  ↑(LieSubalgebra.map (prod eι b₁ b₂).incl (prodCartan eι b₁ b₂)) =
    ↑(lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})
h₂ :
  (lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}).toSubmodule = span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}
x✝ : L₁
⊢ x✝ ∈ ⇑(LinearMap.fst R L₁ L₂) '' {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ↔ x✝ ∈ Set.range b₁.h

Tactic:
simp

Goal state after:
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
i j : Fin n
⊢ of
      (fun i ↦
        Fin.cons (v i ^ 0 * w i ^ n) fun j ↦
          v i ^ (↑j + 1) * w i ^ ↑j.rev - v 0 / w 0 * (v i ^ ↑j * w i ^ (↑j.rev + 1)))
      i.succ j.succ =
    of (fun i j ↦ (v i.succ - v 0 / w 0 * w i.succ) * (v i.succ ^ ↑j * w i.succ ^ ↑j.rev)) i j

Tactic:
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
i j : Fin n
⊢ v i.succ ^ (↑j + 1) * w i.succ ^ (n - (↑j + 1)) - v 0 / w 0 * (v i.succ ^ ↑j * w i.succ ^ (n - (↑j + 1) + 1)) =
    (v i.succ - v 0 / w 0 * w i.succ) * (v i.succ ^ ↑j * w i.succ ^ (n - (↑j + 1)))
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
⊢ 0 ∉ univ → (-1) ^ ↑0 * W 0 0 * (W.submatrix succ (succAbove 0)).det = 0

Tactic:
simp

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₂
h₁ :
  ↑(LieSubalgebra.map (prod eι b₁ b₂).incl (prodCartan eι b₁ b₂)) =
    ↑(lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})
h₂ :
  (lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}).toSubmodule = span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}
h₃ : Submodule.map (LinearMap.fst R L₁ L₂) (span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}) = span R (Set.range b₁.h)
h₄ : (lieSpan R L₁ (Set.range b₁.h)).toSubmodule = span R (Set.range b₁.h)
h₅ : ↑H₁ = ↑(lieSpan R L₁ (Set.range b₁.h))
⊢ Injective ⇑(prod eι b₁ b₂).incl

Tactic:
simp

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₂
⊢ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) ⊆
    range (prodH eι b₁ b₂) ∪ (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))

Tactic:
simp

Goal state after:
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
⊢ ∀ b ∈ univ, b ≠ 0 → (-1) ^ ↑b * W 0 b * (W.submatrix succ b.succAbove).det = 0

Tactic:
intro j

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
j : Fin n.succ
⊢ j ∈ univ → j ≠ 0 → (-1) ^ ↑j * W 0 j * (W.submatrix succ j.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₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
i j : ι₁
⊢ ⁅prodH eι b₁ b₂ j, prodF eι b₁ b₂ i⁆ = -b₁.A i j • prodF eι b₁ b₂ i

Tactic:
simp [Subtype.ext_iff, b₁.lie_h_f, b₂.lie_h_f, ← hA]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ r j * eval (v i) (Lagrange.basis s v j) = 0

Tactic:
eval_basis_of_ne (mem_erase.mp H).1 hi,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ r j * 0 = 0
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: case zero
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
x : ↥H₁
this : IsLieAbelian ↥H₁
⊢ ⁅(↑0).1, ↑x⁆ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
c : F
f : ↥(degreeLT F #s)
⊢ ∀ (x : ↥s), eval (v ↑x) ↑(c • f) = ((RingHom.id F) c • fun i ↦ eval (v ↑i) ↑f) x

Tactic:
simp

Goal state after: