mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
this : InvolutiveNeg ι := P.indexNeg
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root (-i), P.root j]
z : ℤ
⊢ z ∈ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) ↔ P.root j + z • (P.reflection i) (P.root i) ∈ range ⇑P.root

Tactic:
mem_Icc,

Goal state after:
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
this : InvolutiveNeg ι := P.indexNeg
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root (-i), P.root j]
z : ℤ
⊢ -↑(chainTopCoeff i j) ≤ z ∧ z ≤ ↑(chainBotCoeff i j) ↔ P.root j + z • (P.reflection i) (P.root i) ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : LinearIndependent R ![P.root i, P.root j]
h₁ : P.pairing i j = 1
⊢ P.root ((P.reflectionPerm j) i) = P.root i - P.root j

Tactic:
by simpa [h₁] using P.reflection_apply_root j i

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
this : InvolutiveNeg ι := P.indexNeg
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (-j)]
z : ℤ
⊢ z ∈ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) ↔ (P.reflection j) (P.root j) + z • P.root i ∈ range ⇑P.root

Tactic:
mem_Icc,

Goal state after:
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
this : InvolutiveNeg ι := P.indexNeg
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (-j)]
z : ℤ
⊢ -↑(chainTopCoeff i j) ≤ z ∧ z ≤ ↑(chainBotCoeff i j) ↔ (P.reflection j) (P.root j) + z • P.root i ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
⊢ False

Tactic:
suffices P.pairingIn ℤ i i ≤ 0 by simp_all

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✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
⊢ P.pairingIn ℤ i i ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.BilinearForm

Goal state before:
pp: R₂ : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
inst✝² : IsDomain R₂
inst✝¹ : Free R₂ M₂
inst✝ : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
hB : SeparatingLeft B
⊢ B.Nondegenerate

Tactic:
by
  obtain ⟨ι, b⟩ := Module.Free.exists_basis R₂ M₂
  have : Finite ι := Module.Finite.finite_basis b
  have : Fintype ι := Fintype.ofFinite ι
  have : DecidableEq ι := Classical.decEq ι
  rwa [← BilinForm.nondegenerate_toMatrix_iff b, Matrix.nondegenerate_iff_det_ne_zero,
    ← Matrix.separatingLeft_iff_det_ne_zero, separatingLeft_toMatrix_iff]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
⊢ ∃ i, ∀ j ≥ i, ∀ k ≥ i, abv (f j - f k) < ε

Tactic:
refine (hf _ (half_pos ε0)).imp fun i hi j ij k ik => ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : f.LimZero
ε : α
ε0 : ε > 0
G : α
G0 : G > 0
hG : ∀ (i : ℕ), abv (↑g i) < G
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑f j) < ε / G
j : ℕ
ij : j ≥ x✝
⊢ abv (↑(f * g) j) < ε

Tactic:
by
      have := mul_lt_mul'' (H _ ij) (hG j) (abv_nonneg abv _) (abv_nonneg abv _)
      rwa [div_mul_cancel₀ _ (ne_of_gt G0), ← abv_mul] at this

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ (if h : (const abv 0).LimZero then 0 else (const abv 0).inv h) = const abv 0

Tactic:
rw [dif_pos]

Goal state after:
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ 0 = const abv 0

case hc
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ (const abv 0).LimZero
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : n → R
h : 0 ≤ d
x : n →₀ R
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * diagonal d i j * xj

Tactic:
refine Finsupp.sum_nonneg fun i _ ↦ Finsupp.sum_nonneg fun j _ ↦ ?_

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : n → R
h : 0 ≤ d
x : n →₀ R
i : n
x✝¹ : i ∈ x.support
j : n
x✝ : j ∈ x.support
⊢ 0 ≤ star (x i) * diagonal d i j * x 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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
⊢ (cartanMatrixIn S b).Nondegenerate

Tactic:
classical
  obtain ⟨B, hB⟩ : ∃ B : P.InvariantForm, B.form.Nondegenerate :=
    ⟨P.toInvariantForm, P.rootForm_nondegenerate⟩
  replace hB : ((2 : R) • B.form.toMatrix b.toWeightBasis).Nondegenerate := by
    rwa [Matrix.Nondegenerate.smul_iff two_ne_zero, LinearMap.BilinForm.nondegenerate_toMatrix_iff]
  have aux : (Matrix.diagonal fun i : b.support ↦ B.form (P.root i) (P.root i)).Nondegenerate := by
    rw [Matrix.nondegenerate_iff_det_ne_zero, Matrix.det_diagonal, Finset.prod_ne_zero_iff]
    aesop
  rw [← cartanMatrixIn_mul_diagonal_eq (S := S), Matrix.Nondegenerate.mul_iff_right aux,
    Matrix.nondegenerate_iff_det_ne_zero, ← (algebraMap S R).mapMatrix_apply,
    ← RingHom.map_det, ne_eq, FaithfulSMul.algebraMap_eq_zero_iff] at hB
  rwa [Matrix.nondegenerate_iff_det_ne_zero]

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
_i : Fintype ι
d : ↥b.support → ℤ := fun i ↦ ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)
hd : d = fun i ↦ ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)
i : ↥b.support
⊢ 0 < d i

Tactic:
hd,

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
_i : Fintype ι
d : ↥b.support → ℤ := fun i ↦ ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)
hd : d = fun i ↦ ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)
i : ↥b.support
⊢ 0 < (fun i ↦ ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)) i
Module: Mathlib.Data.Nat.Factorial.SuperFactorial

Goal state before:
pp: n : ℕ
⊢ (∏ k ∈ Ico 1 (n + 1), k !) * (n + 1)! = sf n + 1

Tactic:
Nat.factorial_succ,

Goal state after:
n : ℕ
⊢ (∏ k ∈ Ico 1 (n + 1), k !) * ((n + 1) * n !) = sf n + 1
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S),
      eval₂_at_natCast, Nat.cast_id]

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

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

Tactic:
have : natDegree (X - (n : R[X])) = 1 := natDegree_X_sub_C (n : R)
    rw [descPochhammer_succ_right,
        natDegree_mul _ (ne_zero_of_natDegree_gt <| this.symm ▸ Nat.zero_lt_one), hn, this]
    cases n
    · simp
    · refine ne_zero_of_natDegree_gt <| hn.symm ▸ Nat.add_one_pos _

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : k ≤ n
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = ↑(n - k) * ↑(n.descFactorial k)

Tactic:
Nat.cast_sub h

Goal state after:
case neg
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : k ≤ n
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = (↑n - ↑k) * ↑(n.descFactorial k)
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 :
  lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) =
    lieSpan R (↥(prod eι b₁ b₂)) (range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))
hr :
  range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) =
    Subtype.val ⁻¹'
      ({x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ∪ {x | ∃ i, (b₁.e i, b₂.e (eι i)) = x} ∪
        {x | ∃ i, (b₁.f i, b₂.f (eι i)) = x})
⊢ lieSpan R (↥(prod eι b₁ b₂)) (range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) = ⊤

Tactic:
hr

Goal state after:
ι₁ : 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 :
  lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) =
    lieSpan R (↥(prod eι b₁ b₂)) (range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))
hr :
  range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) =
    Subtype.val ⁻¹'
      ({x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ∪ {x | ∃ i, (b₁.e i, b₂.e (eι i)) = x} ∪
        {x | ∃ i, (b₁.f i, b₂.f (eι i)) = x})
⊢ lieSpan R (↥(prod eι b₁ b₂))
      (Subtype.val ⁻¹'
        ({x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ∪ {x | ∃ i, (b₁.e i, b₂.e (eι i)) = x} ∪
          {x | ∃ i, (b₁.f i, b₂.f (eι i)) = x})) =
    ⊤
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
⊢ w 0 ^ n *
      ((∏ x, (v x.succ - v 0 / w 0 * w x.succ)) *
        ∏ i, ∏ j > i, ((v ∘ succ) j * (w ∘ succ) i - (v ∘ succ) i * (w ∘ succ) j)) =
    ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
field_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
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ (w 0 ^ n * ∏ x, (v x.succ * w 0 - v 0 * w x.succ) / w 0) *
      ∏ x, ∏ x_1 > x, ((v ∘ succ) x_1 * (w ∘ succ) x - (v ∘ succ) x * (w ∘ succ) x_1) =
    ∏ x, ∏ x_1 > x, (v x_1 * w x - v x * w x_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
⊢ w 0 ^ n * ((∏ x, (v x.succ * w 0 - v 0 * w x.succ)) / w 0 ^ n) *
      ∏ x, ∏ x_1 > x, (v x_1.succ * w x.succ - v x.succ * w x_1.succ) =
    ∏ x, ∏ x_1 > x, (v x_1 * w x - v x * w x_1)

Tactic:
field_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
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ (∏ x, (w 0 * v x.succ - v 0 * w x.succ)) * ∏ x, ∏ x_1 > x, (w x.succ * v x_1.succ - v x.succ * w x_1.succ) =
    ∏ x, ∏ x_1 > x, (w x * v x_1 - v x * w x_1)
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
f : F[X]
hf : f.degree < ↑(#s)
⊢ ((interpolate s v) fun x ↦ if x ∈ s then eval (v x) f else 0) = f

Tactic:
conv => rhs; rw [eq_interpolate hvs hf]

Goal state after:
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
f : F[X]
hf : f.degree < ↑(#s)
⊢ ((interpolate s v) fun x ↦ if x ∈ s then eval (v x) f else 0) = (interpolate s v) fun i ↦ eval (v i) f
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
n : ℕ
hn : ((ad R L) x ^ n) ⁅x, y⁆ = 0
⊢ ∃ n, ((ad R L) x ^ n) y = 0

Tactic:
use n + 1

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
n : ℕ
hn : ((ad R L) x ^ n) ⁅x, y⁆ = 0
⊢ ((ad R L) x ^ (n + 1)) y = 0
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
n : ℕ
hn : ((ad R L) x ^ n) ⁅x, y⁆ = 0
⊢ ((ad R L) x ^ n) (((ad R L) x) y) = 0

Tactic:
exact hn

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case a
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
hP : P.degree < ↑(#s)
i : ι
hi : i ∈ s
⊢ eval (v i) P * (∏ j ∈ s.erase i, (v i - v j))⁻¹ = eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
field_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₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
⊢ (Matrix.reindex eι.symm eι.symm) b₂.A = b₁.A

Tactic:
simp [← hA]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_3
inst✝ : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (fun d ↦ d) ↑(image x univ)
⊢ ∃ q, ∀ (i : ι), eval (x i) q = y i

Tactic:
set v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0 with v_def

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_3
inst✝ : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (fun d ↦ d) ↑(image x univ)
v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
v_def : v = fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
⊢ ∃ q, ∀ (i : ι), eval (x i) q = y i
Module: Mathlib.Algebra.MvPolynomial.Monad

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

Tactic:
ext : 2 <;> simp

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

Goal state before:
pp: σ : 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
⊢ (bind₂ g).comp (bind₂ f) = bind₂ ((bind₂ g).comp f)

Tactic:
ext : 2 <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
v : ι → R
inst✝ : Nontrivial R
⊢ nodal ∅ v ≠ 0

pp: case inr
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
h : s.Nonempty
⊢ nodal s v ≠ 0

Tactic:
· exact one_ne_zero

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
h : s.Nonempty
⊢ nodal s v ≠ 0
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
K : ℕ →o Submodule R ↥H := { toFun := fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → K n = K m
y : ↥H
⊢ ((ad R L) ↑x ^ n) ↑y = ↑(0 y)

Tactic:
specialize h x x.2 y.2

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H := { toFun := fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → K n = K m
y : ↥H
h : ↑y ∈ engel R ↑x
⊢ ((ad R L) ↑x ^ n) ↑y = ↑(0 y)
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : 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
⊢ (eval₂Hom f g).comp (bind₂ h) = eval₂Hom ((eval₂Hom f g).comp h) g

Tactic:
ext : 2 <;> simp

Goal state after:
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
r : K[X]
hr : (aeval ((ad K (End K M)) s)) r = (ad K (End K M)) y
p : K[X]
hp : (aeval ((ad K (End K M)) (φ x))) p = (ad K (End K M)) s
⊢ (aeval ((ad K (End K M)) s)) r = (ad K (End K M)) y

Tactic:
hr

Goal state after:
L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
r : K[X]
hr : (aeval ((ad K (End K M)) s)) r = (ad K (End K M)) y
p : K[X]
hp : (aeval ((ad K (End K M)) (φ x))) p = (ad K (End K M)) s
⊢ (ad K (End K M)) y = (ad K (End K M)) y