mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg
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α : ¬α.IsZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
this : ↑(chainLength α β) = ↑(chainTopCoeff (⇑α) β) * 2 + β (coroot α)
⊢ β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))

Tactic:
simp only [Int.cast_sub, Int.cast_natCast, Int.cast_mul, Int.cast_ofNat, eq_sub_iff_add_eq',
    this, mul_comm (2 : K)]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
p q : Module.Dual R M × M
⊢ (p + q).1 (p + q).2 = p.1 p.2 + q.1 q.2 + (q.1 p.2 + p.1 q.2)

Tactic:
Prod.fst_add,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
p q : Module.Dual R M × M
⊢ (p.1 + q.1) (p + q).2 = p.1 p.2 + q.1 q.2 + (q.1 p.2 + p.1 q.2)
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
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Hom P₂
f : P.Hom P₁
i : ι₂
⊢ (⇑(f.coweightMap ∘ₗ g.coweightMap) ∘ ⇑P₂.coroot) i = (⇑P.coroot ∘ ⇑(f.indexEquiv.trans g.indexEquiv).symm) i

Tactic:
simp only [LinearMap.coe_comp]

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
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Hom P₂
f : P.Hom P₁
i : ι₂
⊢ ((⇑f.coweightMap ∘ ⇑g.coweightMap) ∘ ⇑P₂.coroot) i = (⇑P.coroot ∘ ⇑(f.indexEquiv.trans g.indexEquiv).symm) i
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)
⊢ Submodule.map (↑(P.coreflection i)).dualMap q.dualAnnihilator ≤ q.dualAnnihilator

Tactic:
exact (Submodule.dualAnnihilator_map_dualMap_le _ _).trans <| Submodule.dualAnnihilator_anti hq

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

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x✝ : ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
⊢ q = ⊥ ∨ q = ⊤

Tactic:
have := IsIrreducible.eq_top_of_invtSubmodule_reflection q hq

Goal state after:
case refine_1
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x✝ : ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
this : q ≠ ⊥ → q = ⊤
⊢ q = ⊥ ∨ q = ⊤
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 ι
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : LinearOrder S
inst✝⁵ : IsStrictOrderedRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := (P.posRootForm S).rootLength i
lj : S := (P.posRootForm S).rootLength j
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
⊢ 4 * lij ^ 2 ≤ 4 * (li * lj)

Tactic:
rw [mul_le_mul_iff_right₀ four_pos]

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✝⁸ : Finite ι
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : LinearOrder S
inst✝⁵ : IsStrictOrderedRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := (P.posRootForm S).rootLength i
lj : S := (P.posRootForm S).rootLength j
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
⊢ lij ^ 2 ≤ li * lj
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✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : P.root j = t • P.root i
this : ∃ c, ∑ i, c i • P.coroot ↑i = P.coroot j
f : ↥b.support → ℤ
hf : ∑ i, f i • P.coroot ↑i = P.coroot j
⊢ P.coroot i = ∑ i, (t * ↑(f i)) • P.coroot ↑i

Tactic:
simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
      coroot_eq_smul_coroot_iff.mpr hj]

Goal state after:
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
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
⊢ 0 < f ∨ f < 0

Tactic:
suffices ∀ (f : ι → ℤ)
      (hf : ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (P.root '' b.support))
      (hf₀ : f.support ⊆ b.support) (hf' : f ≠ 0), 0 < f by
    obtain ⟨k, hk⟩ := hf
    have hf' : f ≠ 0 := by rintro rfl; exact P.ne_zero k <| by simp [hk]
    rcases b.root_mem_or_neg_mem k with hk' | hk' <;> rw [hk] at hk'
    · left; exact this f hk' hf₀ hf'
    · right; simpa using this (-f) (by convert! hk'; simp) (by simpa only [support_neg]) (by simpa)

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
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
⊢ ∀ (f : ι → ℤ),
    ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
      Function.support f ⊆ ↑b.support → f ≠ 0 → 0 < f
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]
⊢ ↑(chainBotCoeff i j) = sSup {k | P.root j - k • P.root i ∈ range ⇑P.root}

Tactic:
by
  rw [setOfPred_root_sub_zsmul_mem_eq_Icc h]
  simp

Goal state after:
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
hp : i ≠ j
hn : P.root i ≠ -P.root j
h_add : P.root i + P.root j ∉ range ⇑P.root
h_sub : P.root i - P.root j ∉ range ⇑P.root
⊢ (algebraMap ℤ R) (P.pairingIn ℤ i j) = 0

Tactic:
P.pairingIn_eq_zero_of_add_notMem_of_sub_notMem hp hn h_add h_sub,

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
hp : i ≠ j
hn : P.root i ≠ -P.root j
h_add : P.root i + P.root j ∉ range ⇑P.root
h_sub : P.root i - P.root j ∉ range ⇑P.root
⊢ (algebraMap ℤ R) 0 = 0
Module: Mathlib.LinearAlgebra.RootSystem.Base

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
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
x✝ y✝ : M
hx✝ : x✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
hy✝ : y✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
f : ι → ℕ
hf : Function.support f ⊆ ↑b.support
hf' : x✝ = ∑ j ∈ b.support, f j • P.root j
⊢ (∃ f, Function.support f ⊆ ↑b.support ∧ y✝ = ∑ j ∈ b.support, f j • P.root j) →
    ∃ f, Function.support f ⊆ ↑b.support ∧ x✝ + y✝ = ∑ j ∈ b.support, f j • P.root j

Tactic:
⟨g, hg, hg'⟩

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
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
x✝ y✝ : M
hx✝ : x✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
hy✝ : y✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
f : ι → ℕ
hf : Function.support f ⊆ ↑b.support
hf' : x✝ = ∑ j ∈ b.support, f j • P.root j
g : ι → ℕ
hg : Function.support g ⊆ ↑b.support
hg' : y✝ = ∑ j ∈ b.support, g j • P.root j
⊢ ∃ f, Function.support f ⊆ ↑b.support ∧ x✝ + y✝ = ∑ j ∈ b.support, f j • P.root j
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg
ι : 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
B : P.InvariantForm
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
i j : ι
hji_ne : (B.form (P.root j)) (P.root j) ≠ (B.form (P.root i)) (P.root i)
⊢ ∃ i j,
    ∀ (k : ι),
      (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
        (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

Tactic:
refine ⟨i, j, fun k ↦ ?_⟩

Goal state after:
case neg
ι : 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
B : P.InvariantForm
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
i j : ι
hji_ne : (B.form (P.root j)) (P.root j) ≠ (B.form (P.root i)) (P.root i)
k : ι
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)
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 : ι
⊢ P.root (chainBotIdx i j) = P.root j - chainBotCoeff i j • P.root i

Tactic:
by
  by_cases h : LinearIndependent R ![P.root i, P.root j]
  · simp only [chainBotIdx, reduceDIte, h]
    exact (P.root_sub_nsmul_mem_range_iff_le_chainBotCoeff h).mpr
      (le_refl <| P.chainBotCoeff i j) |>.choose_spec
  · simp only [chainBotIdx, chainBotCoeff, h, reduceDIte, zero_smul, sub_zero]

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
x y : β
⊢ (const x - const y).LimZero ↔ x = y

Tactic:
← const_sub,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x y : β
⊢ (const (x - y)).LimZero ↔ x = y
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
x y : β
⊢ (const x - const y).LimZero ↔ x = y

Tactic:
rw [← const_sub, const_limZero, sub_eq_zero]

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
⊢ (const y - const x).Pos ↔ x < y

Tactic:
← const_sub,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
⊢ (const (y - x)).Pos ↔ x < y
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ 0 < a → 0 < b → 0 < a * b

Tactic:
by
    induction a using Real.ind_mk
    induction b using Real.ind_mk
    simpa only [mk_lt, mk_pos, ← mk_mul] using CauSeq.mul_pos

Goal state after:
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 x = w x

Tactic:
rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]

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

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ c ≈ b ⊓ c

Tactic:
exact Setoid.symm (CauSeq.inf_eq_right hb)

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

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
A : Matrix n n α
⊢ A ⊙ 1 = 0 ↔ A.diag = 0

Tactic:
simpa using hadamard_one_eq_diagonal_iff (A := A) (d := 0)

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

Goal state before:
pp: α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ v ᵥ* A ⊙ B ⬝ᵥ w = (diagonal v * A * (B * diagonal w)ᵀ).trace

Tactic:
rw [← sum_hadamard_eq, Finset.sum_comm]
  simp [dotProduct, vecMul, Finset.sum_mul, mul_assoc]

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

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ A.IsHermitian

Tactic:
← transpose_transpose A

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ Aᵀᵀ.IsHermitian
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: R : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
f : End R M
inst✝² : IsDomain R
inst✝¹ : Module.Finite R M
inst✝ : IsTorsionFree R M
⊢ {μ | f.HasEigenvalue μ}.Finite

Tactic:
have h : minpoly R f ≠ 0 := minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := R) f)

Goal state after:
R : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
f : End R M
inst✝² : IsDomain R
inst✝¹ : Module.Finite R M
inst✝ : IsTorsionFree R M
h : minpoly R f ≠ 0
⊢ {μ | f.HasEigenvalue μ}.Finite
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
⊢ p j

Tactic:
let q : Submodule R M := span R (P.root ∘ (↑) '' {i | p i})
  have hq₀ : q ≠ ⊥ := q.ne_bot_iff.mpr ⟨P.root i, subset_span <| by simpa, P.ne_zero i⟩
  have hq_mem (k : b.support) : P.root k ∈ q ↔ p k := by
    refine ⟨fun hk ↦ ?_, fun hk ↦ subset_span <| by simpa⟩
    contrapose hk
    exact b.linearIndepOn_root.linearIndependent.notMem_span_image hk
  have hq_notMem (k : b.support) (hk : P.root k ∉ q) : q ≤ LinearMap.ker (P.coroot' k) := by
    refine fun x hx ↦ LinearMap.mem_ker.mpr ?_
    contrapose! hk
    rw [hq_mem]
    induction hx using Submodule.span_induction with
    | mem x hx =>
      obtain ⟨l, hl, rfl⟩ : ∃ l : b.support, p l ∧ P.root l = x := by simp_all
      replace hk : b.cartanMatrix k l ≠ 0 := by
        rwa [ne_eq, cartanMatrix_apply_eq_zero_iff_symm, cartanMatrix_apply_eq_zero_iff_pairing]
      tauto
    | zero => simp_all
    | add x y hx hy hx' hy' =>
      replace hk : P.coroot' k x ≠ 0 ∨ P.coroot' k y ≠ 0 := by by_contra! contra; simp_all
      tauto
    | smul a x hx hx' => simp_all
  have hq : ∀ k, q ∈ invtSubmodule (P.reflection k) := by
    rw [← b.forall_mem_support_invtSubmodule_iff]
    refine fun k hkb ↦ (mem_invtSubmodule _).mpr fun x hx ↦ ?_
    rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply]
    apply q.sub_mem hx
    by_cases hk : P.root k ∈ q
    · exact q.smul_mem _ hk
    · replace hk : P.coroot' k x = 0 := hq_notMem ⟨k, hkb⟩ hk hx
      simp [hk]
  simp [← hq_mem, IsIrreducible.eq_top_of_invtSubmodule_reflection q hq hq₀]

Goal state after:
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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
m : M
hm : m ∈ range ⇑P.root
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
k : ↥b.support
this : ∀ (j : ↥b.support), (P.reflection ↑k ≪≫ₗ f) (P.root ↑j) = (f ≪≫ₗ P₂.reflection ↑(e k)) (P.root ↑j)
j : ↥b.support
⊢ ↑(P.reflection ↑k ≪≫ₗ f) (b.toWeightBasis j) = ↑(f ≪≫ₗ P₂.reflection ↑(e k)) (b.toWeightBasis j)

Tactic:
by simpa using this j

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

Goal state before:
pp: case e'_2
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : ↑rn = -r
⊢ r = -↑rn

Tactic:
simp [rnn]

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

Goal state before:
pp: case hy
ι₁ : 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₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ prodF eι b₁ b₂ i ∈ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))

Tactic:
· exact subset_lieSpan <| mem_union_right _ <| mem_range_self i

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
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:
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 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
hy : ⁅x, y⁆ ∈ engel R x
⊢ y ∈ engel R x

Tactic:
mem_engel_iff

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
hy : ∃ n, ((ad R L) x ^ n) ⁅x, y⁆ = 0
⊢ y ∈ engel R x
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
⊢ y ∈ engel R x

Tactic:
mem_engel_iff

Goal state after:
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
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
y : ↥N
hy : y ∈ (dx ^ (k + 1)).ker
⊢ y ∈ Submodule.comap N.subtype (engel R x).toSubmodule

Tactic:
simp only [Submodule.mem_comap, mem_engel_iff, mem_toSubmodule]

Goal state after:
case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
y : ↥N
hy : y ∈ (dx ^ (k + 1)).ker
⊢ ∃ n, ((ad R L) x ^ n) (N.subtype y) = 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]
deg : ℕ
hdeg : ↑deg = P.degree
hP : ↑(#s) = ↑deg + ↑1
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
← WithBot.coe_add

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
deg : ℕ
hdeg : ↑deg = P.degree
hP : ↑(#s) = ↑(deg + 1)
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)