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

Goal state before:
pp: case inr
ι : 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
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
this :
  ∀ (f : ι → ℤ),
    ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
      Function.support f ⊆ ↑b.support → f ≠ 0 → 0 < f
k : ι
hk : P.root k = ∑ j ∈ b.support, f j • P.root j
hf' : f ≠ 0
hk' : -P.root k ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ 0 < f ∨ f < 0

Tactic:
rw [hk] at hk'

Goal state after:
case inr
ι : 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
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
this :
  ∀ (f : ι → ℤ),
    ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
      Function.support f ⊆ ↑b.support → f ≠ 0 → 0 < f
k : ι
hk : P.root k = ∑ j ∈ b.support, f j • P.root j
hf' : f ≠ 0
hk' : -∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ 0 < f ∨ f < 0
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_span : span ℚ (range v) = ⊤
⊢ Basis ↑(baseOf (⇑P.root) f) ℚ ↥(P.rootSpan ℚ)

Tactic:
replace this : LinearIndependent ℚ v :=
        .of_comp (P.rootSpan ℚ).subtype <| P.linearIndepOn_root_baseOf' f.toRatLinearMap hf
      exact Basis.mk this (by rw [h_span])

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 : ι
h : LinearIndependent R ![P.root i, P.root j]
this : chainBotCoeff i j = 0 ↔ Iic (chainBotCoeff i j) = {0}
h' : P.root j - P.root i ∉ range ⇑P.root
n : ℕ
h'' : P.root j - n • P.root i ∈ range ⇑P.root
⊢ n = 0

Tactic:
replace h' : 1 ∉ {k | P.root j - k • P.root i ∈ range P.root} := by simpa using h'

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 : ι
h : LinearIndependent R ![P.root i, P.root j]
this : chainBotCoeff i j = 0 ↔ Iic (chainBotCoeff i j) = {0}
n : ℕ
h'' : P.root j - n • P.root i ∈ range ⇑P.root
h' : 1 ∉ {k | P.root j - k • P.root i ∈ range ⇑P.root}
⊢ n = 0
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
huv : P.root i = u • P.root j + v • P.root k
l : ι
hl : 0 < g (P.coroot l)
⊢ ∃ c, ∑ x, c x • ↑x = P.root l

Tactic:
← Submodule.mem_span_iff_of_fintype,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
huv : P.root i = u • P.root j + v • P.root k
l : ι
hl : 0 < g (P.coroot l)
⊢ P.root l ∈ span ℕ (⇑P.root '' s)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this✝ : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
this : li = 2 * lj ∨ lj = 2 * li
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 2 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂

Tactic:
rcases this with h₀ | h₀ <;> rcases key k₁ with h₁ | h₁ <;> rcases key k₂ with h₂ | h₂ <;>
    simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk <;>
    aesop

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inr
ι : 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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this✝ : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
this : li = 3 * lj ∨ lj = 3 * li
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
rcases this with h₀ | h₀ <;> rcases key k₁ with h₁ | h₁ <;> rcases key k₂ with h₂ | h₂ <;>
    simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk <;>
    aesop

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ j ≥ i, F ≤ ↑f j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
⊢ F / 2 ≤ ↑(f + g) j

Tactic:
by
      obtain ⟨h₁, h₂⟩ := h j ij
      have := add_le_add h₁ (le_of_lt (abs_lt.1 h₂).1)
      rwa [← sub_eq_add_neg, sub_self_div_two] at this

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b : ℝ), a ≤ a ⊔ b

Tactic:
intro a b
    induction a using Real.ind_mk
    induction b using Real.ind_mk
    rw [← mk_sup, mk_le]
    exact CauSeq.le_sup_left

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✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (const abv f.lim⁻¹ - f * (f.inv hf * const abv f.lim⁻¹)).LimZero

Tactic:
by rw [← mul_assoc]; exact h₁ _ _ _

Goal state after:
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 : IsUnit A.det
n : ℕ
⊢ A ^ (↑n + 1) = A ^ ↑n * A

Tactic:
by simp only [← Nat.cast_succ, pow_succ, zpow_natCast]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
d : n → R
b : Basis n R M
j : n
⊢ b j ∈ eigenspace ((toLin b b) (diagonal d)) (d j)

Tactic:
simp [diagonal_apply]

Goal state after:
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 : IsUnit A.det
m n : ℤ
⊢ A ^ (m * n) = (A ^ n) ^ m

Tactic:
rw [mul_comm, zpow_mul _ h]

Goal state after:
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
n : ℕ
⊢ (A ^ -[n+1])ᵀ = Aᵀ ^ -[n+1]

Tactic:
rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
ι : Type u_5
inst✝ : AddLeftMono R
A : ι → Matrix m m R
s : Finset ι
hs : s.Nonempty
hA : ∀ i ∈ s, (A i).PosDef
⊢ (∑ i ∈ s, A i).PosDef

Tactic:
induction s using Finset.induction_on with
  | empty => simp at hs
  | insert i hi hins H =>
      rw [Finset.sum_insert hins]
      by_cases h : ¬ hi.Nonempty
      · simp_all
      · exact PosDef.add (hA _ <| Finset.mem_insert_self i hi) <|
          H (not_not.mp h) fun _ _hi => hA _ (Finset.mem_insert_of_mem _hi)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
inst✝⁴ : Fintype n
K : Type u_5
inst✝³ : Field K
inst✝² : PartialOrder K
inst✝¹ : StarRing K
inst✝ : DecidableEq n
M : Matrix n n K
hM : M.PosDef
h : ¬IsUnit M
⊢ ∃ a, a ≠ 0 ∧ M *ᵥ a = 0

Tactic:
by
    obtain ⟨a, b, ha⟩ := Function.not_injective_iff.mp <| mulVec_injective_iff_isUnit.not.mpr h
    exact ⟨a - b, by simp [sub_eq_zero, ha, mulVec_sub]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case mp
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
⊢ ((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) →
    (D - Bᴴ * A⁻¹ * B).PosSemidef

Tactic:
refine fun h => .of_dotProduct_mulVec_nonneg h.1 fun x => ?_

Goal state after:
case mp
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → R'
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hv₀ : |v| ≠ 0
h₁ : 0 < ∑ j, ∑ i, |v i| * (d i * A i j) * |v j|
h₂ : Q = ∑ i, |v i| * (d i * μ) * |v i|
⊢ ∑ j, ∑ i, |v| i * (diagonal d * (μ • 1 - A)) i j * |v| j < Q

Tactic:
simpa [mul_sub, sub_mul, Matrix.one_apply, h₂]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
i : ι
x✝ : i ∈ Finset.univ
h₀ : 0 ≤ ρ - μ
h₁ : μ ≤ ρ - μ
h₂ : 0 ≤ d i
h₃ : (ρ - μ) * |v i| ≤ (N *ᵥ |v|) i
⊢ (N *ᵥ |v|) i * (d i * |v i|) = (N *ᵥ |v|) i * (diagonal d *ᵥ |v|) i

Tactic:
by simp [mulVec_eq_sum, diagonal_apply, mul_comm]

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

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

Tactic:
rw [← ascPochhammer_map f]
  exact eval_map f t

Goal state after:
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
  suffices h : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - (n : ℤ[X])) by
    apply_fun Polynomial.map (algebraMap ℤ R) at h
    simpa [descPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
      Polynomial.map_intCast] using h
  induction n with
  | zero => simp [descPochhammer]
  | succ n ih =>
    conv_lhs =>
      rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
          X_comp, natCast_comp]
    rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
⊢ (s.sup fun b ↦ ((interpolate (insert b (t \ s)) v) r * Lagrange.basis s v b).degree) < ↑(#t)

Tactic:
simp_rw [Nat.cast_withBot, Finset.sup_lt_iff (WithBot.bot_lt_coe #t), degree_mul]

Goal state after:
case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
⊢ ∀ b ∈ s, ((interpolate (insert b (t \ s)) v) r).degree + (Lagrange.basis s v b).degree < ↑(#t)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
H : ∑ j ∈ s, eval (v i) (Lagrange.basis s v j) = 1
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) =
    r i * ∑ j ∈ s, eval (v i) (Lagrange.basis s v j)

Tactic:
mul_sum

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
H : ∑ j ∈ s, eval (v i) (Lagrange.basis s v j) = 1
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) =
    ∑ i_1 ∈ s, r i * eval (v i) (Lagrange.basis s v i_1)
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : τ → S
g : σ → MvPolynomial τ R
i✝ : σ
⊢ ((aeval f).comp (bind₁ g)) (X i✝) = (aeval fun i ↦ (aeval f) (g i)) (X i✝)

Tactic:
apply aeval_bind₁

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α : Type u_6} (x : MvPolynomial α R), id <$> x = x

Tactic:
by intros; simp [(· <$> ·)]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β γ : Type u_6} (g : α → β) (h : β → γ) (x : MvPolynomial α R), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
by intros; simp [(· <$> ·)]

Goal state after:
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
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
h : ∀ (a : R), motive (C a * p) ⋯
⊢ motive p hp

Tactic:
by simpa using h 1

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_1.succ
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
ih : homogeneousSubmodule σ R 1 ^ n ≤ homogeneousSubmodule σ R n
⊢ homogeneousSubmodule σ R n * homogeneousSubmodule σ R 1 ≤ homogeneousSubmodule σ R (n + 1)

Tactic:
apply homogeneousSubmodule_mul

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
⊢ (((finSuccEquiv R N) φ).coeff i).IsHomogeneous j

Tactic:
intro d hd
  rw [finSuccEquiv_coeff_coeff] at hd
  have h' : (weight 1) (Finsupp.cons i d) = i + j := by
    simpa [Finset.sum_subset_zero_on_sdiff (g := d.cons i)
     (d.cons_support (y := i)) (by simp) (fun _ _ ↦ rfl), ← h] using hφ hd
  simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum_cons,
    add_right_inj] at h' ⊢
  exact h'

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)

Tactic:
· rw [h zero_coeff]
    simp only [show n = m ↔ m = n from eq_comm]
    split_ifs with h1
    · rfl
    · simp only [coeff_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : i < n
⊢ constantCoeff (((finSuccEquiv R N) F).coeff i) = 0

Tactic:
apply (hF.finSuccEquiv_coeff_isHomogeneous i (n - i) (by lia)).coeff_eq_zero

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : i < n
⊢ Finsupp.degree 0 ≠ n - i
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: M : Type u_2
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
⊢ (weight w) m = 0 ↔ ∀ (x : σ), m x = 0

Tactic:
by
  simp only [weight, Finsupp.linearCombination, LinearMap.toAddMonoidHom_coe, coe_lsum,
    LinearMap.coe_smulRight, LinearMap.id_coe, id_eq]
  rw [Finsupp.sum, Finset.sum_eq_zero_iff]
  apply forall_congr'
  intro x
  rw [Finsupp.mem_support_iff]
  constructor
  · intro hx
    by_contra hx'
    exact absurd (hw _ _ (hx hx')) hx'
  · order

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w)) (decompose' R w φ) =
    ∑ᶠ (m : M), (weightedHomogeneousComponent w m) φ

Tactic:
rw [← DirectSum.sum_support_of (decompose' R w φ)]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w))
      (∑ i ∈ DFinsupp.support (decompose' R w φ),
        (DirectSum.of (fun i ↦ ↥(weightedHomogeneousSubmodule R w i)) i) ((decompose' R w φ) i)) =
    ∑ᶠ (m : M), (weightedHomogeneousComponent w m) φ
Module: Mathlib.Algebra.Lie.Character

Goal state before:
pp: case mem
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
h : y ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ χ y = 0

Tactic:
| mem y h =>

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

Goal state before:
pp: R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
ψ : Module.Dual R L
x y : L
⊢ ψ.toFun ⁅x, y⁆ = ⁅ψ.toFun x, ψ.toFun y⁆

Tactic:
LieModule.IsTrivial.trivial,

Goal state after:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
ψ : Module.Dual R L
x y : L
⊢ ψ.toFun 0 = ⁅ψ.toFun x, ψ.toFun y⁆
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case mp
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
⊢ (charpoly (φ x)).coeff φ.nilRank ≠ 0 → (charpoly (φ x)).natTrailingDegree = φ.nilRank

Tactic:
intro h
    exact le_antisymm
      (Polynomial.natTrailingDegree_le_of_ne_zero h)
      (nilRank_le_natTrailingDegree_charpoly φ x)

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

Goal state before:
pp: R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆

Tactic:
Matrix.lie_transpose,

Goal state after:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ ⁅Bᵀ, Aᵀ⁆ * J = J * -⁅A, B⁆