mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case inl
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
x : n →₀ R
i : n
x✝¹ x✝ : i ∈ x.support
⊢ 0 ≤ star (x i) * 1 i i * x i

pp: case inr
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
x : n →₀ R
i : n
x✝¹ : i ∈ x.support
j : n
x✝ : j ∈ x.support
hij : i ≠ j
⊢ 0 ≤ star (x i) * 1 i j * x j

Tactic:
<;>

Goal state after:
case inl
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
x : n →₀ R
i : n
x✝¹ x✝ : i ∈ x.support
⊢ 0 ≤ star (x i) * 1 i i * x i

case inr
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
x : n →₀ R
i : n
x✝¹ : i ∈ x.support
j : n
x✝ : j ∈ x.support
hij : i ≠ j
⊢ 0 ≤ star (x i) * 1 i j * x j
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case inl
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℕ
x : n →₀ R
i : n
x✝¹ x✝ : i ∈ x.support
⊢ 0 ≤ star (x i) * ↑d i i * x i

pp: case inr
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℕ
x : n →₀ R
i : n
x✝¹ : i ∈ x.support
j : n
x✝ : j ∈ x.support
hij : i ≠ j
⊢ 0 ≤ star (x i) * ↑d i j * x j

Tactic:
<;>

Goal state after:
case inl
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℕ
x : n →₀ R
i : n
x✝¹ x✝ : i ∈ x.support
⊢ 0 ≤ star (x i) * ↑d i i * x i

case inr
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℕ
x : n →₀ R
i : n
x✝¹ : i ∈ x.support
j : n
x✝ : j ∈ x.support
hij : i ≠ j
⊢ 0 ≤ star (x i) * ↑d i j * x j
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case inl
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n →₀ R
i : n
x✝¹ x✝ : i ∈ x.support
⊢ 0 ≤ star (x i) * ↑d i i * x i

pp: case inr
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n →₀ R
i : n
x✝¹ : i ∈ x.support
j : n
x✝ : j ∈ x.support
hij : i ≠ j
⊢ 0 ≤ star (x i) * ↑d i j * x j

Tactic:
<;>

Goal state after:
case inl
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n →₀ R
i : n
x✝¹ x✝ : i ∈ x.support
⊢ 0 ≤ star (x i) * ↑d i i * x i

case inr
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n →₀ R
i : n
x✝¹ : i ∈ x.support
j : n
x✝ : j ∈ x.support
hij : i ≠ j
⊢ 0 ≤ star (x i) * ↑d i j * x j
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case inl
n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
⊢ 0 ≤ Finsupp.sum 0 fun i xi ↦ Finsupp.sum 0 fun j xj ↦ star xi * M i j * xj

pp: case inr
n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n →₀ R
hx : x ≠ 0
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * M i j * xj

Tactic:
<;>

Goal state after:
case inl
n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
⊢ 0 ≤ Finsupp.sum 0 fun i xi ↦ Finsupp.sum 0 fun j xj ↦ star xi * M i j * xj

case inr
n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n →₀ R
hx : x ≠ 0
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * M i j * xj
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 : A.IsSymm
k : ℤ
⊢ (A ^ k)ᵀ = A ^ k

Tactic:
transpose_zpow,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A.IsSymm
k : ℤ
⊢ Aᵀ ^ k = A ^ k
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case refine_2.refine_1
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ i ∈ x.support

pp: case refine_2.refine_2
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ ∀ i_1 ∈ x.support, 0 ≤ star (x i) * diagonal d i i_1 * x i_1

pp: case refine_2.refine_3
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ i ∈ x.support

pp: case refine_2.refine_4
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ 0 < star (x i) * diagonal d i i * x i

Tactic:
<;>

Goal state after:
case refine_2.refine_1
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ i ∈ x.support

case refine_2.refine_2
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ ∀ i_1 ∈ x.support, 0 ≤ star (x i) * diagonal d i i_1 * x i_1

case refine_2.refine_3
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ i ∈ x.support

case refine_2.refine_4
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ 0 < star (x i) * diagonal d i i * x i
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case e'_1
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype n
inst✝³ : StarOrderedRing R'
inst✝² : Finite m
inst✝¹ : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst✝ : Invertible D
⊢ B = Bᴴᴴ

pp: case e'_2
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype n
inst✝³ : StarOrderedRing R'
inst✝² : Finite m
inst✝¹ : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst✝ : Invertible D
⊢ B = Bᴴᴴ

Tactic:
<;>

Goal state after:
case e'_1
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype n
inst✝³ : StarOrderedRing R'
inst✝² : Finite m
inst✝¹ : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst✝ : Invertible D
⊢ B = Bᴴᴴ

case e'_2
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype n
inst✝³ : StarOrderedRing R'
inst✝² : Finite m
inst✝¹ : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst✝ : Invertible D
⊢ B = Bᴴᴴ
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 ι
i j : ↥b.support
hij : i ≠ j
⊢ b.cartanMatrix i j = 0 ↔ P.root ↑i + P.root ↑j ∉ range ⇑P.root

Tactic:
rw [b.cartanMatrix_eq_neg_chainTopCoeff hij, neg_eq_zero, Int.natCast_eq_zero,
    P.chainTopCoeff_eq_zero_iff]
  replace hij := b.linearIndependent_pair_of_ne hij.symm
  tauto

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: case refine_1
ι : 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
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ ∃ x, ∃ (_ : x ∈ genWeightSpace L ⇑(b.baseSupp i)), ¬x = 0

Tactic:
exact ⟨b.e i, (mem_genWeightSpace _ _ _).mpr fun x ↦ ⟨1, by simp⟩, (b.sl2 i).e_ne_zero⟩

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) = ascPochhammer ℕ (n + 1) + (↑n + 1) * (ascPochhammer ℕ n).comp (X + 1)

Tactic:
ascPochhammer_succ_left

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: case refine_1.succ.inl
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
h : eval r (ascPochhammer R n) = 0
⊢ ∃ k < n + 1, ↑k = -r

Tactic:
obtain ⟨rn, hrn, rrn⟩ := ih h

Goal state after:
case refine_1.succ.inl
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
h : eval r (ascPochhammer R n) = 0
rn : ℕ
hrn : rn < n
rrn : ↑rn = -r
⊢ ∃ k < n + 1, ↑k = -r
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ * (x - y) = 1

Tactic:
exact inv_mul_cancel₀ (sub_ne_zero_of_ne hxy)

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case mp
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
⊢ (f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i) → f = (interpolate s v) r

pp: case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
⊢ f = (interpolate s v) r → f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i

Tactic:
<;>

Goal state after:
case mp
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
⊢ (f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i) → f = (interpolate s v) r

case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
⊢ f = (interpolate s v) r → f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
u : Bool → Fin n → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun b i ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ))) (MvPolynomial.X (i, b))
hdet :
  ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1).mapMatrix
        (projVandermonde (fun i ↦ MvPolynomial.X (i, true)) fun i ↦ MvPolynomial.X (i, false))).det =
    (MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1)
      (∏ i,
        ∏ i_1 > i,
          (MvPolynomial.X (i_1, true) * MvPolynomial.X (i, false) -
            MvPolynomial.X (i, true) * MvPolynomial.X (i_1, false)))
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
convert! hdet

Goal state after:
case e'_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
u : Bool → Fin n → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun b i ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ))) (MvPolynomial.X (i, b))
hdet :
  ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1).mapMatrix
        (projVandermonde (fun i ↦ MvPolynomial.X (i, true)) fun i ↦ MvPolynomial.X (i, false))).det =
    (MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1)
      (∏ i,
        ∏ i_1 > i,
          (MvPolynomial.X (i_1, true) * MvPolynomial.X (i, false) -
            MvPolynomial.X (i, true) * MvPolynomial.X (i_1, false)))
⊢ projVandermonde v w =
    (MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1).mapMatrix
      (projVandermonde (fun i ↦ MvPolynomial.X (i, true)) fun i ↦ MvPolynomial.X (i, false))

case e'_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
u : Bool → Fin n → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun b i ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ))) (MvPolynomial.X (i, b))
hdet :
  ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1).mapMatrix
        (projVandermonde (fun i ↦ MvPolynomial.X (i, true)) fun i ↦ MvPolynomial.X (i, false))).det =
    (MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1)
      (∏ i,
        ∏ i_1 > i,
          (MvPolynomial.X (i_1, true) * MvPolynomial.X (i, false) -
            MvPolynomial.X (i, true) * MvPolynomial.X (i_1, false)))
⊢ ∏ i, ∏ j > i, (v j * w i - v i * w j) =
    (MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1)
      (∏ i,
        ∏ i_1 > i,
          (MvPolynomial.X (i_1, true) * MvPolynomial.X (i, false) -
            MvPolynomial.X (i, true) * MvPolynomial.X (i_1, false)))
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ i, ∏ j > i, (↑↑j - ↑↑i) = ↑(n.succ.factorial * n.superFactorial)

Tactic:
Fin.prod_univ_succAbove _ 0

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ (∏ j > 0, (↑↑j - ↑↑0)) * ∏ i, ∏ j > succAbove 0 i, (↑↑j - ↑↑(succAbove 0 i)) = ↑(n.succ.factorial * n.superFactorial)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: 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
⊢ ∑ x ∈ s, C (r x / ∏ j ∈ s.erase x, (v x - v j)) * (⇑derivative)^[k] (∏ j ∈ s.erase x, (X - C (v j))) =
    ∑ x ∈ s,
      ↑k.factorial * C (r x / ∏ j ∈ s.erase x, (v x - v j)) *
        ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase x), ∏ j ∈ t, (X - C (v j))

Tactic:
mul_comm (k.factorial : F[X]),

Goal state after:
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
⊢ ∑ x ∈ s, C (r x / ∏ j ∈ s.erase x, (v x - v j)) * (⇑derivative)^[k] (∏ j ∈ s.erase x, (X - C (v j))) =
    ∑ x ∈ s,
      C (r x / ∏ j ∈ s.erase x, (v x - v j)) * ↑k.factorial *
        ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase x), ∏ j ∈ t, (X - C (v j))
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case hC
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
x✝ : R
⊢ ((bind₂ C).comp C) x✝ = ((RingHom.id (MvPolynomial σ R)).comp C) x✝

pp: case hX
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((bind₂ C) (X i✝)) = coeff m✝ ((RingHom.id (MvPolynomial σ R)) (X i✝))

Tactic:
<;>

Goal state after:
case hC
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
x✝ : R
⊢ ((bind₂ C).comp C) x✝ = ((RingHom.id (MvPolynomial σ R)).comp C) x✝

case hX
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((bind₂ C) (X i✝)) = coeff m✝ ((RingHom.id (MvPolynomial σ R)) (X i✝))
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case hC
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
x✝ : R
⊢ (((bind₂ g).comp (bind₂ f)).comp C) x✝ = ((bind₂ ((bind₂ g).comp f)).comp C) x✝

pp: case hX
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ (((bind₂ g).comp (bind₂ f)) (X i✝)) = coeff m✝ ((bind₂ ((bind₂ g).comp f)) (X i✝))

Tactic:
<;>

Goal state after:
case hC
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
x✝ : R
⊢ (((bind₂ g).comp (bind₂ f)).comp C) x✝ = ((bind₂ ((bind₂ g).comp f)).comp C) x✝

case hX
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ (((bind₂ g).comp (bind₂ f)) (X i✝)) = coeff m✝ ((bind₂ ((bind₂ g).comp f)) (X i✝))
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (map f).comp C = C.comp f

Tactic:
by
  ext1
  apply map_C

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case hC
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
x✝ : R
⊢ (((eval₂Hom f g).comp (bind₂ h)).comp C) x✝ = ((eval₂Hom ((eval₂Hom f g).comp h) g).comp C) x✝

pp: case hX
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
i✝ : σ
⊢ ((eval₂Hom f g).comp (bind₂ h)) (X i✝) = (eval₂Hom ((eval₂Hom f g).comp h) g) (X i✝)

Tactic:
<;>

Goal state after:
case hC
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
x✝ : R
⊢ (((eval₂Hom f g).comp (bind₂ h)).comp C) x✝ = ((eval₂Hom ((eval₂Hom f g).comp h) g).comp C) x✝

case hX
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
i✝ : σ
⊢ ((eval₂Hom f g).comp (bind₂ h)) (X i✝) = (eval₂Hom ((eval₂Hom f g).comp h) g) (X i✝)
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ((bind₁ f) φ).vars = (∑ x ∈ φ.support, (bind₁ f) ((monomial x) (coeff x φ))).vars

Tactic:
← map_sum,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ((bind₁ f) φ).vars = ((bind₁ f) (∑ x ∈ φ.support, (monomial x) (coeff x φ))).vars
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
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : p ≠ 0
⊢ weightedTotalDegree' w p = ↑(weightedTotalDegree w p)

Tactic:
rw [Ne, ← weightedTotalDegree'_eq_bot_iff w p, ← Ne, WithBot.ne_bot_iff_exists] at hp

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : ∃ a, ↑a = weightedTotalDegree' w p
⊢ weightedTotalDegree' w p = ↑(weightedTotalDegree w p)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case pos
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
h : coeff d φ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0

pp: case neg
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
h : ¬coeff d φ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0

Tactic:
<;>

Goal state after:
case pos
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
h : coeff d φ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0

case neg
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
h : ¬coeff d φ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0
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
φ : MvPolynomial σ R
n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : (weight w) d ≠ n
aux : ¬coeff d φ ≠ 0
⊢ coeff d φ = 0

Tactic:
Classical.not_not

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : (weight w) d ≠ n
aux : coeff d φ = 0
⊢ coeff d φ = 0
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 : ι
r : A
hr : r ∈ ⊥
⊢ ↑(((decompose 𝒜) r) i) ∈ ⊥

Tactic:
simp only [Ideal.mem_bot] at 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 : ι
r : A
hr : r = 0
⊢ ↑(((decompose 𝒜) r) i) ∈ ⊥