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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
i j k : ι
m n : R
hk : m • P.root i + n • P.root j = P.root k
B : P.InvariantForm := P.toInvariantForm
lsq : ι → R := fun i ↦ (B.form (P.root i)) (P.root i)
hlsq : ∀ (i : ι), lsq i = (P.RootForm (P.root i)) (P.root i)
h₂ : lsq k = m * m * lsq i + m * n * (2 * (B.form (P.root i)) (P.root j)) + n * n * lsq j
h₃ : 2 * (B.form (P.root i)) (P.root j) = P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₁ :
  P.pairing j i • (m * m * lsq i + m * n * (P.pairing i j * lsq j) + n * n * lsq j) • P.coroot k =
    P.pairing j i • ((m • lsq i) • P.coroot i + (n • lsq j) • P.coroot j)
⊢ (m * m * (P.pairing j i * lsq i)) • P.coroot k + (m * n * (P.pairing j i * P.pairing i j * lsq j)) • P.coroot k +
      (n * n * (P.pairing j i * lsq j)) • P.coroot k =
    (m * (P.pairing j i * lsq i)) • P.coroot i + (n * (P.pairing j i * lsq j)) • P.coroot j

Tactic:
simp only [add_smul, smul_add, ← mul_smul, smul_eq_mul] at h₁

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
i j k : ι
m n : R
hk : m • P.root i + n • P.root j = P.root k
B : P.InvariantForm := P.toInvariantForm
lsq : ι → R := fun i ↦ (B.form (P.root i)) (P.root i)
hlsq : ∀ (i : ι), lsq i = (P.RootForm (P.root i)) (P.root i)
h₂ : lsq k = m * m * lsq i + m * n * (2 * (B.form (P.root i)) (P.root j)) + n * n * lsq j
h₃ : 2 * (B.form (P.root i)) (P.root j) = P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₁ :
  (P.pairing j i * (m * m * lsq i)) • P.coroot k + (P.pairing j i * (m * n * (P.pairing i j * lsq j))) • P.coroot k +
      (P.pairing j i * (n * n * lsq j)) • P.coroot k =
    (P.pairing j i * (m * lsq i)) • P.coroot i + (P.pairing j i * (n * lsq j)) • P.coroot j
⊢ (m * m * (P.pairing j i * lsq i)) • P.coroot k + (m * n * (P.pairing j i * P.pairing i j * lsq j)) • P.coroot k +
      (n * n * (P.pairing j i * lsq j)) • P.coroot k =
    (m * (P.pairing j i * lsq i)) • P.coroot i + (n * (P.pairing j i * lsq j)) • P.coroot j
Module: Mathlib.LinearAlgebra.RootSystem.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl : coroot l = (preReflection (coroot i) (p (root i))) (coroot j)
⊢ coroot k = coroot l

Tactic:
have hkl : (p.flip (coroot l)) (root k) = 2 := by
    simp only [hl, preReflection_apply, map_sub, map_smul, hk, LinearMap.flip_apply,
      LinearMap.sub_apply, hp j, LinearMap.smul_apply, smul_eq_mul, hp i, mul_two,
      sub_add_cancel_right, mul_neg, sub_neg_eq_add, sα, α, α', β]
    rw [mul_comm (p (root i) (coroot j))]
    abel

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl : coroot l = (preReflection (coroot i) (p (root i))) (coroot j)
hkl : (p.flip (coroot l)) (root k) = 2
⊢ coroot k = coroot l
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ v.IsEquiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1

Tactic:
by
  constructor
  · intro h x
    rw [h.lt_one_iff_lt_one]
  · rw [isEquiv_iff_val_eq_one]
    intro h x
    by_cases hx : x = 0
    · simp only [(zero_iff _).2 hx, zero_ne_one]
    constructor
    · intro hh
      by_contra h_1
      cases ne_iff_lt_or_gt.1 h_1 with
      | inl h_2 => simpa [hh, lt_self_iff_false] using h.2 h_2
      | inr h_2 =>
          rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh
          exact hh.not_lt (h.2 ((one_lt_val_iff v' hx).1 h_2))
    · intro hh
      by_contra h_1
      cases ne_iff_lt_or_gt.1 h_1 with
      | inl h_2 => simpa [hh, lt_self_iff_false] using h.1 h_2
      | inr h_2 =>
        rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh
        exact hh.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2))

Goal state after:
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, v x < 1 ↔ v' x < 1) ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1

Tactic:
exact (Equiv.subRight 1).surjective.forall

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

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✝ : Fintype ι
i j : ι
hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i))
hji : 2 • (P.RootForm (P.root i)) (P.root j) = (P.toLinearMap (P.root i)) (2 • P.Polarization (P.root j))
⊢ 2 •
      ((P.toLinearMap (P.root j)) ((P.RootForm (P.root i)) (P.root i) • P.coroot i) *
        (P.RootForm (P.root i)) (P.root j)) =
    P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))

Tactic:
← mul_smul_comm,

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
inst✝ : Fintype ι
i j : ι
hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i))
hji : 2 • (P.RootForm (P.root i)) (P.root j) = (P.toLinearMap (P.root i)) (2 • P.Polarization (P.root j))
⊢ (P.toLinearMap (P.root j)) ((P.RootForm (P.root i)) (P.root i) • P.coroot i) *
      2 • (P.RootForm (P.root i)) (P.root j) =
    P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

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
i j : ι
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
h : P.root j = 2 • P.root i
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4

Tactic:
· rw [← coroot_eq_smul_coroot_iff] at h
    rw [pairing, pairing, h]
    norm_num
    suffices (2 : R) • P.pairing i j = (2 : R) • 1 from h2 this
    rw [pairing, ← map_smul, ← h]
    simp

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case inr.inl
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑↑n - ↑↑(chainTopCoeff (⇑α) β)
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
← Int.cast_sub

Goal state after:
case inr.inl
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑(↑n - ↑(chainTopCoeff (⇑α) β))
⊢ k = -1 ∨ k = 0 ∨ k = 1
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

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
i : ι
q : Submodule R N
hq : q ∈ invtSubmodule ↑(P.coreflection i)
⊢ q.dualAnnihilator ∈ (P.toPerfPair.conj ↑(P.reflection i)).invtSubmodule

Tactic:
toPerfPair_conj_reflection,

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
i : ι
q : Submodule R N
hq : q ∈ invtSubmodule ↑(P.coreflection i)
⊢ q.dualAnnihilator ∈ invtSubmodule (↑(P.coreflection i)).dualMap
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
i : ι
x : N
⊢ (↑(reflection P i)⁻¹).coweightMap x = (↑(reflection P i)).coweightMap x

Tactic:
by simp [← coweightEquiv_apply]

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

Goal state before:
pp: ι : 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]
z : ℤ
⊢ P.root j + z • P.root i ∈ range ⇑P.root ↔ z ∈ Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)

Tactic:
by
  rcases z.eq_nat_or_neg with ⟨n, rfl | rfl⟩
  · simp [P.root_add_nsmul_mem_range_iff_le_chainTopCoeff h]
  · simp [P.root_sub_nsmul_mem_range_iff_le_chainBotCoeff h, ← sub_eq_add_neg]

Goal state after:
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
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
f : M →+ ℚ
hf : ∀ i ∈ s, f (P.root i) = 1
_i : InvolutiveNeg ι := P.indexNeg
h_card : (baseOf (⇑P.root) f).ncard = s.ncard
i : ι
hi : -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
z : ℤ
hz : f (P.root (-i)) = ↑z
⊢ f (P.root i) = ↑(-z)

Tactic:
simp [← hz]

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

Goal state before:
pp: R₁ : Type u_1
inst✝² : CommSemiring R₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R₁
i j : n
⊢ ((toBilin' M) (Pi.single i 1)) (Pi.single j 1) = M i j

Tactic:
simp [Matrix.toBilin'_apply, Pi.single_apply]

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ (h - f).Pos

Tactic:
convert pos_add_limZero fg (neg_limZero gh)

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ h - f = g - f + -(g - h)
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
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i : ι
⊢ P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑⋯.toFinset) ∨
    -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑⋯.toFinset)

Tactic:
simpa using coroot_mem_or_neg_mem_closure_of_root P s hli hsp i

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
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
⊢ (g - f * f.inv hf * g).LimZero

Tactic:
have h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g := by rw [h₂, h₃, ← sub_mul]

Goal state after:
α : 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
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
⊢ (g - f * f.inv hf * g).LimZero
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 : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A ^ n * A⁻¹ ^ m = A ^ n * (A * A⁻¹) * A⁻¹ ^ m

Tactic:
by simp only [h', Matrix.mul_one]

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
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
hρ : HasEigenvalue (toLin' N) (μ - ρ)
⊢ ∃ v, N *ᵥ v = (μ - ρ) • v ∧ v ≠ 0

Tactic:
simpa [hasEigenvector_iff, mulVec_transpose] using hρ.exists_hasEigenvector

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

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

Tactic:
eval_add,

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

Goal state before:
pp: n t : ℕ
⊢ n.ascFactorial t * eval n (X + ↑t) = n.ascFactorial (t + 1)

Tactic:
eval_add,

Goal state after:
n t : ℕ
⊢ n.ascFactorial t * (eval n X + eval n ↑t) = n.ascFactorial (t + 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n * X + ascPochhammer S n * ↑n)

Tactic:
eval_add,

Goal state after:
case succ
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n * X) + eval s (ascPochhammer S n * ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ eval (-r) (ascPochhammer R k * X + ascPochhammer R k * ↑k) = (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))

Tactic:
eval_add,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ eval (-r) (ascPochhammer R k * X) + eval (-r) (ascPochhammer R k * ↑k) =
    (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) =
    (-1) ^ k * (-1 * (eval r (descPochhammer R k) * r) - -1 * (↑k * eval r (descPochhammer R k)))

Tactic:
neg_one_mul,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) =
    (-1) ^ k * (-(eval r (descPochhammer R k) * r) - -1 * (↑k * eval r (descPochhammer R k)))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) =
    (-1) ^ k * (eval r (descPochhammer R k) * -r + -(-1 * (eval r (descPochhammer R k) * ↑k)))

Tactic:
neg_one_mul,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) =
    (-1) ^ k * (eval r (descPochhammer R k) * -r + - -(eval r (descPochhammer R k) * ↑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₂
⊢ LieSubalgebra.map (LieEquiv.prodComm R L₂ L₁).toLieHom (prod eι.symm b₂ b₁) = prod eι b₁ b₂

Tactic:
rw [prod, prod, map_lieSpan]; congr; ext; aesop

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

Goal state before:
pp: case refine_1.succ.inr
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
h : r + ↑n = 0
⊢ ∃ k < n + 1, ↑k = -r

Tactic:
exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩

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

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
⊢ range b₂.e = range (⇑p₂ ∘ prodE eι b₁ b₂)

Tactic:
simp [show p₂ ∘ prodE eι b₁ b₂ = b₂.e ∘ eι from rfl]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ((interpolate (s.erase i) v) r).degree < ↑(#(s.erase i))

Tactic:
exact degree_interpolate_lt _ (Set.InjOn.mono (coe_subset.mpr (erase_subset _ _)) hvs)

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

Tactic:
· exact eq_interpolate_of_eval_eq _ hvs h.1 h.2

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
⊢ f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i
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
this : ∑ i, f ⟨μ i, ⋯⟩ • ⟨μ i, ⋯⟩ = 0
⊢ ∑ i, f ⟨μ i, ⋯⟩ ^ 2 = 0

Tactic:
simpa only [map_sum, map_zero, map_smul, sq] using! f.congr_arg this

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
a✝ b✝ : MvPolynomial σ R
x✝¹ : a✝ ∈ {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}
x✝ : b✝ ∈ {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}
w✝¹ : IsWeightedHomogeneous w a✝ m
hx : ∀ (a : R), motive (C a * a✝) ⋯
w✝ : IsWeightedHomogeneous w b✝ m
hy : ∀ (a : R), motive (C a * b✝) ⋯
a : R
⊢ motive (C a * (a✝ + b✝)) ⋯

Tactic:
simp [mul_add, add _ _ _ _ (hx a) (hy a)]

Goal state after: