mathlib-initiative/mathlib-tactics huggingface dataset:
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
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : ∑ x, (u * ↑(a x) + v * ↑(b x)) • ↑x = ∑ x, Pi.single ri 1 x • ↑x
aux : P.root i = ∑ x, Pi.single ri 1 x • ↑x
hli : LinearIndepOn ℚ id (⇑P.root '' s)
⊢ u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1

Tactic:
← linearIndependent_subtype_iff

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
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : ∑ x, (u * ↑(a x) + v * ↑(b x)) • ↑x = ∑ x, Pi.single ri 1 x • ↑x
aux : P.root i = ∑ x, Pi.single ri 1 x • ↑x
hli : LinearIndependent ℚ Subtype.val
⊢ u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_3
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ K⁻¹ * (abv (a - b) * K⁻¹) < ε

Tactic:
h

Goal state after:
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_3
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ K⁻¹ * (K * ε * K * K⁻¹) ≤ ε
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
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k
this : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos (-i)
⊢ p i

Tactic:
suffices p (-i) by rw [← neg_neg i]; exact h₀ (-i) this
    exact hi.induction_on_add h₁ h₂

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

Goal state before:
pp: x a : ℝ
⊢ 1 * a = a

Tactic:
apply ext_cauchy; simp [cauchy_mul, cauchy_one]

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

Goal state before:
pp: x a : ℝ
⊢ a * 1 = a

Tactic:
apply ext_cauchy; simp [cauchy_mul, cauchy_one]

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

Goal state before:
pp: f : CauSeq ℚ abs
⊢ 0 < mk f ↔ f.Pos

Tactic:
by
  rw [← mk_zero, mk_lt]
  exact iff_of_eq (congr_arg Pos (sub_zero f))

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

Goal state before:
pp: case inl
x a : ℝ
⊢ ∀ (c : ℝ), a + c = a + c ∨ a + c < a + c

Tactic:
simp only [lt_self_iff_false, or_false, forall_const]

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✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
⊢ (const abv (f.lim * g.lim) - f * g).LimZero

Tactic:
h

Goal state after:
α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
⊢ ((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)).LimZero
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(b - a) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ ↑(c - a) j
⊢ a < b ⊓ c

Tactic:
refine ⟨εb ⊓ εc, lt_inf_iff.mpr ⟨εb0, εc0⟩, ib ⊔ ic, fun i hi => ?_⟩

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(b - a) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ ↑(c - a) j
i : ℕ
hi : i ≥ max ib ic
⊢ min εb εc ≤ ↑(b ⊓ c - a) i
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv f.lim
⊢ f.LimZero

Tactic:
h

Goal state after:
α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv 0
⊢ f.LimZero
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
⊢ v ⬝ᵥ Pi.single x 1 = w ⬝ᵥ Pi.single x 1

Tactic:
h

Goal state after:
n : Type u_2
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
⊢ w ⬝ᵥ Pi.single x 1 = w ⬝ᵥ Pi.single x 1
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |max (↑a j - ↑b j) (↑b j - ↑b j)| < ε✝

Tactic:
rwa [sub_self, max_eq_right, abs_zero]

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ ↑a j - ↑b j ≤ 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : f 1 ^ 2 = f 1
h : f 1 = 0
⊢ f 1 ≤ 1

Tactic:
h

Goal state after:
case inl
R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : f 1 ^ 2 = f 1
h : f 1 = 0
⊢ 0 ≤ 1
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : f 1 ^ 2 = f 1
h : f 1 = 1
⊢ f 1 ≤ 1

Tactic:
h

Goal state after:
case inr
R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : f 1 ^ 2 = f 1
h : f 1 = 1
⊢ 1 ≤ 1
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
h : ¬(ia = ib ∧ ja = jb)
a b : α
⊢ single ia ja a ⊙ single ib jb b = 0

Tactic:
not_and_or

Goal state after:
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
h : ¬ia = ib ∨ ¬ja = jb
a b : α
⊢ single ia ja a ⊙ single ib jb b = 0
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
h : A.IsHermitian
k : ℤ
⊢ Aᴴ ^ k = A ^ k

Tactic:
h

Goal state after:
α : Type u_1
m : Type u_3
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
h : A.IsHermitian
k : ℤ
⊢ A ^ k = A ^ k
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case pred
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit A.det
m : ℤ
n : ℕ
ihn : A ^ (m + -↑n) = A ^ m * A ^ (-↑n)
⊢ A ^ (m + (-↑n - 1)) = A ^ m * A ^ (-↑n - 1)

Tactic:
| pred n ihn =>

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
m n : ℤ
hm : 0 ≤ m
hn : 0 ≤ n
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
by
  obtain ⟨k, rfl⟩ := eq_ofNat_of_zero_le hm
  obtain ⟨l, rfl⟩ := eq_ofNat_of_zero_le hn
  rw [← Int.natCast_add, zpow_natCast, zpow_natCast, zpow_natCast, pow_add]

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 : A.IsSymm
k : ℤ
⊢ Aᵀ ^ k = A ^ k

Tactic:
h

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: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Fintype m
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective fun v ↦ v ᵥ* B
⊢ (B * A * Bᴴ).PosDef

Tactic:
replace hB := star_injective.comp <| hB.comp star_injective

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Fintype m
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective (star ∘ (fun v ↦ v ᵥ* B) ∘ star)
⊢ (B * A * Bᴴ).PosDef
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case refine_2
ι : 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)
⊢ (b.cartanMatrix * Matrix.diagonal d).PosDef

Tactic:
cartanMatrix_mul_diagonal_eq

Goal state after:
case refine_2
ι : 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)
⊢ (2 • (LinearMap.BilinForm.toMatrix b.toWeightBasisInt) (P.posRootForm ℤ).posForm).PosDef
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
⊢ (spectrum K f).Finite

Tactic:
convert! f.finite_hasEigenvalue using 1
  ext x
  exact Module.End.hasEigenvalue_iff_mem_spectrum.symm

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

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

Tactic:
natCast_comp,

Goal state after:
S : Type u
inst✝ : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
| ascPochhammer ℕ (n + 1) * (X + 1 + ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
natCast_comp,

Goal state after:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (X + 1 + ↑n) * (ascPochhammer ℕ n).comp (X + 1) = (X + (↑n + 1)) * (ascPochhammer ℕ n).comp (X + 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ 0 = ↑0

Tactic:
Nat.cast_zero

Goal state after:
case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: a b : ℕ
⊢ eval (↑(a + b)) (descPochhammer ℤ b) = ↑((a + 1).ascFactorial b)

Tactic:
descPochhammer_eval_eq_descFactorial ℤ (a + b) b,

Goal state after:
a b : ℕ
⊢ ↑((a + b).descFactorial b) = ↑((a + 1).ascFactorial b)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: a b : ℕ
⊢ eval (↑a + ↑b) (descPochhammer ℤ b) = ↑((a + 1).ascFactorial b)

Tactic:
rw [← Nat.cast_add, descPochhammer_eval_eq_descFactorial ℤ (a + b) b,
    Nat.add_descFactorial_eq_ascFactorial]

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
s : Finset ι
v f g : ι → F
h :
  (fun x ↦ C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x) = fun x ↦
    C ((f + g) x) * Lagrange.basis s v x
⊢ ∑ i ∈ s, C ((f + g) i) * Lagrange.basis s v i =
    ∑ x ∈ s, (C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x)

Tactic:
h

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s✝ t : Finset ι
i j : ι
v✝ r r' : ι → F
s : Finset ι
v f g : ι → F
h :
  (fun x ↦ C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x) = fun x ↦
    C ((f + g) x) * Lagrange.basis s v x
⊢ ∑ i ∈ s, C ((f + g) i) * Lagrange.basis s v i = ∑ x ∈ s, C ((f + g) x) * Lagrange.basis s v x
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
⊢ ((interpolate s v) r).degree < ↑(#s)

Tactic:
Nat.cast_withBot

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
⊢ ((interpolate s v) r).degree < ↑(#s)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
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
h : f = (interpolate s v) r
⊢ f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i

Tactic:
h

Goal state after:
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
h : f = (interpolate s v) r
⊢ ((interpolate s v) r).degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) ((interpolate s v) r) = r i
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq : ⟨a i, ⋯⟩ - ⟨a j, ⋯⟩ = ⟨a k, ⋯⟩ - ⟨a l, ⋯⟩
⊢ (algebraMap R K) (f (⟨a (i, j).1, ⋯⟩ - ⟨a (i, j).2, ⋯⟩)) = (algebraMap R K) (f (⟨a (k, l).1, ⋯⟩ - ⟨a (k, l).2, ⋯⟩))

Tactic:
heq

Goal state after:
ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq : ⟨a i, ⋯⟩ - ⟨a j, ⋯⟩ = ⟨a k, ⋯⟩ - ⟨a l, ⋯⟩
⊢ (algebraMap R K) (f (⟨a k, ⋯⟩ - ⟨a l, ⋯⟩)) = (algebraMap R K) (f (⟨a (k, l).1, ⋯⟩ - ⟨a (k, l).2, ⋯⟩))
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
⊢ ∀ {y_1 : L} (x_1 : ℕ),
    ((ad R L) x ^ x_1) y = 0 → ∀ (x_2 : ℕ), ((ad R L) x ^ x_2) y_1 = 0 → ∃ k, ((ad R L) x ^ k) ⁅y, y_1⁆ = 0

Tactic:
z

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y z : L
⊢ ∀ (x_1 : ℕ), ((ad R L) x ^ x_1) y = 0 → ∀ (x_2 : ℕ), ((ad R L) x ^ x_2) z = 0 → ∃ k, ((ad R L) x ^ k) ⁅y, z⁆ = 0
Module: Mathlib.LinearAlgebra.Lagrange

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

Tactic:
by
  nth_rewrite 1 [eq_interpolate hvs hP, iterate_derivative_interpolate _ hvs hk]
  simp [eval_finsetSum, eval_prod]

Goal state after:
Module: Mathlib.LinearAlgebra.Charpoly.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
⊢ charpoly 1 = (X - 1) ^ Module.finrank R M

Tactic:
by
  simp [charpoly, Module.finrank_eq_card_chooseBasisIndex, Matrix.charpoly_one]

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 ι
v r : ι → F
j : ι
hj : j ∈ s
⊢ C (r j) * Lagrange.basis s v j = C (nodalWeight s v j) * (nodal s v / (X - C (v j))) * C (r j)

Tactic:
rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hj]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
r x : A
hx₁ : IsHomogeneousElem 𝒜 x
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
⊢ (GradedRing.proj 𝒜 j) (↑(((decompose 𝒜) r) k) * x) ∈ I

Tactic:
obtain ⟨i, hi⟩ := hx₁

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
⊢ (GradedRing.proj 𝒜 j) (↑(((decompose 𝒜) r) k) * x) ∈ I
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
⊢ (∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)) →
    IsWeightedHomogeneous w (∏ i ∈ insert i s, φ i) (∑ i ∈ insert i s, n i)

Tactic:
h

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (∏ i ∈ insert i s, φ i) (∑ i ∈ insert i s, n i)
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
I : LieIdeal R L
h : ∀ x ∈ I, ∀ y ∈ ⁅I, I⁆, ((killingForm R L) x) y = 0
⊢ IsSolvable ↥I

Tactic:
set DI : LieIdeal R L := ⁅I, I⁆

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h : ∀ x ∈ I, ∀ y ∈ DI, ((killingForm R L) x) y = 0
⊢ IsSolvable ↥I
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
⊢ ∑ i_1 ∈ s.support, ↑(((decompose 𝒜) (s i_1 • ↑i_1)) i) ∈ span s✝

Tactic:
refine Ideal.sum_mem _ ?_

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
⊢ ∀ c ∈ s.support, ↑(((decompose 𝒜) (s c • ↑c)) i) ∈ span s✝
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ homogeneousSubmodule σ R 0 = 1

Tactic:
ext
  rw [MvPolynomial.mem_homogeneousSubmodule,
    ← MvPolynomial.totalDegree_zero_iff_isHomogeneous, Submodule.mem_one,
    MvPolynomial.algebraMap_eq, MvPolynomial.totalDegree_eq_zero_iff_eq_C]
  grind [coeff_zero_C]

Goal state after:
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 : Ideal A
r : A
hr : r ∈ I
⊢ r ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 r]

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 : Ideal A
r : A
hr : r ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) r), ↑(((decompose 𝒜) r) i) ∈ (homogeneousHull 𝒜 I).toIdeal
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 : Ideal A
r : A
hr : r ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) r), ↑(((decompose 𝒜) r) i) ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
refine Ideal.sum_mem _ ?_

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 : Ideal A
r : A
hr : r ∈ I
⊢ ∀ c ∈ DFinsupp.support ((decompose 𝒜) r), ↑(((decompose 𝒜) r) c) ∈ (homogeneousHull 𝒜 I).toIdeal