mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: case hf
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
hc : ∑ i ∈ s, c i • v i = 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ ∀ x ∈ s, x ∉ {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} → c x • v x = 0

Tactic:
simp +contextual [eq_comm (a := (0 : R))]

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

Goal state before:
pp: 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
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
⊢ ∃ k, k • f = ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1)) x

Tactic:
have : (toEnd K L L f ^ (chainTopCoeff α (0 : Weight K H L) + 1)) x ∈ rootSpace H (-α) := by
      convert toEnd_pow_apply_mem hf hx (chainTopCoeff α (0 : Weight K H L) + 1)
      rw [coe_chainTop', FunLike.coe_zero, add_zero, succ_nsmul',
        add_assoc, smul_neg, neg_add_cancel, add_zero]
    simpa using! (finrank_eq_one_iff_of_nonzero' ⟨f, hf⟩ (by simpa using! isSl2.f_ne_zero)).mp
      (finrank_rootSpace_eq_one _ hα.neg) ⟨_, this⟩

Goal state after:
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
⊢ genWeightSpace L (↑(-(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β))) • ⇑α + ⇑β) ≠ ⊥

Tactic:
Int.cast_smul_eq_zsmul,

Goal state after:
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
⊢ genWeightSpace L (-(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) ≠ ⊥
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: 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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
x : ↥H
⊢ β x = (u • ⇑α) x

Tactic:
exact DFunLike.congr_fun hu.symm x

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
inst✝ : P.IsReduced
this : Module.IsReflexive R M
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}

Tactic:
rcases eq_or_ne i j with rfl | h₁

Goal state after:
case 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
i : ι
inst✝¹ : IsDomain R
inst✝ : P.IsReduced
this : Module.IsReflexive R M
⊢ (P.pairingIn ℤ i i, P.pairingIn ℤ i i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}

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
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : P.IsCrystallographic
i j : ι
inst✝¹ : IsDomain R
inst✝ : P.IsReduced
this : Module.IsReflexive R M
h₁ : i ≠ j
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
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 = t • ∑ x, ↑(f x) • P.coroot ↑x

Tactic:
Int.cast_smul_eq_zsmul,

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✝² : 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 = t • ∑ x, f x • P.coroot ↑x
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' : -∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ 0 < f ∨ f < 0

Tactic:
right; simpa using this (-f) (by convert! hk'; simp) (by simpa only [support_neg]) (by simpa)

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
⊢ ∑ j ∈ b.support, (-f) j • P.root j ∈ range ⇑P.root

Tactic:
rw [← neg_mem_range_root_iff]

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
⊢ -∑ j ∈ b.support, (-f) j • P.root j ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case 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
b : P.Base
inst✝ : CharZero R
i : ι
f : ι → ℕ
hf : Function.support f ⊆ ↑b.support
hf' : P.root i = ∑ j ∈ b.support, f j • P.root j
⊢ ∃ f, Function.support f ⊆ ↑b.support ∧ (0 < f ∨ f < 0) ∧ P.root i = ∑ j ∈ b.support, f j • P.root j

Tactic:
refine ⟨Nat.cast ∘ f, by simpa, Or.inl <| Pi.lt_def.mpr ⟨fun _ ↦ by simp, ?_⟩, by simp [hf']⟩
    by_contra! contra
    replace contra : f = 0 := by ext i; simpa using contra i
    exact P.ne_zero i <| by simp [hf', contra]

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

Goal state before:
pp: case pos
ι : 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 : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : ↑m < n
this : m = ⟨↑m, hm⟩.castSucc
⊢ ∑ m' ≤ ⟨↑m, hm⟩.castSucc, P.root (Fin.snoc f k m') ∈ range ⇑P.root

Tactic:
Fin.sum_Iic_castSucc

Goal state after:
case pos
ι : 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 : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : ↑m < n
this : m = ⟨↑m, hm⟩.castSucc
⊢ ∑ i ≤ ⟨↑m, hm⟩, P.root (Fin.snoc f k i.castSucc) ∈ range ⇑P.root
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 - y)).LimZero ↔ x = y

Tactic:
const_limZero,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x y : β
⊢ x - y = 0 ↔ x = y
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x y : β
⊢ ofRat (x / y) = ofRat x / ofRat y

Tactic:
by
  simp only [div_eq_mul_inv, ofRat_inv, ofRat_mul]

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

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
d : n → R
μ : R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
b : Basis n R M
this✝ : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
h_iSup : ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ = ⊤
hμ_notMem : μ ∉ Set.range d
this : Disjoint (eigenspace ((toLin b b) (diagonal d)) μ) (⨆ i ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) i)
⊢ False

Tactic:
rw [h_iSup, disjoint_top] at this

Goal state after:
case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
d : n → R
μ : R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
b : Basis n R M
this✝ : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
h_iSup : ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ = ⊤
hμ_notMem : μ ∉ Set.range d
this : eigenspace ((toLin b b) (diagonal d)) μ = ⊥
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case pos
n : Type u_2
R' : Type u_4
inst✝⁴ : CommRing R'
inst✝³ : PartialOrder R'
inst✝² : StarRing R'
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : IsUnit M.det
⊢ M⁻¹.PosSemidef

Tactic:
have := (conjTranspose_mul_mul_same hM M⁻¹).conjTranspose
    rwa [mul_nonsing_inv_cancel_right _ _ h, conjTranspose_conjTranspose] at this

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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : B.form.Nondegenerate
⊢ ((LinearMap.BilinForm.toMatrix b.toWeightBasis) B.form).Nondegenerate

Tactic:
LinearMap.BilinForm.nondegenerate_toMatrix_iff

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
S : Type u_5
inst✝⁹ : CommRing S
inst✝⁸ : Algebra S R
inst✝⁷ : IsDomain R
inst✝⁶ : NeZero 2
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : IsDomain S
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsValuedIn S
inst✝¹ : Fintype ι
inst✝ : P.IsAnisotropic
b : P.Base
B : P.InvariantForm
hB : B.form.Nondegenerate
⊢ B.form.Nondegenerate
Module: Mathlib.Algebra.Lie.Prod

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (inl R L₁ L₂).range.toSubmodule = (LieIdeal.toLieSubalgebra R (L₁ × L₂) (snd R L₁ L₂).ker).toSubmodule

Tactic:
range_toSubmodule,

Goal state after:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (↑(inl R L₁ L₂)).range = (LieIdeal.toLieSubalgebra R (L₁ × L₂) (snd R L₁ L₂).ker).toSubmodule
Module: Mathlib.Algebra.Lie.Prod

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (inr R L₁ L₂).range.toSubmodule = (LieIdeal.toLieSubalgebra R (L₁ × L₂) (fst R L₁ L₂).ker).toSubmodule

Tactic:
range_toSubmodule,

Goal state after:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (↑(inr R L₁ L₂)).range = (LieIdeal.toLieSubalgebra R (L₁ × L₂) (fst R L₁ L₂).ker).toSubmodule
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 ι
i j : ↥b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  (P.pairingIn ℤ ↑i ↑j, P.pairingIn ℤ ↑j ↑i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
h₂ : P.pairingIn ℤ ↑i ↑j ≤ 0
contra : P.pairingIn ℤ ↑j ↑i = -1 ∧ P.pairingIn ℤ ↑i ↑j = -4
⊢ False

Tactic:
pairingIn_neg_one_neg_four_iff

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✝³ : P.IsCrystallographic
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  (P.pairingIn ℤ ↑i ↑j, P.pairingIn ℤ ↑j ↑i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
h₂ : P.pairingIn ℤ ↑i ↑j ≤ 0
contra : P.root ↑i = -2 • P.root ↑j
⊢ False
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
⊢ (ρ - μ) * |v i| = |μ - ρ| * |v i|

Tactic:
rw [← abs_eq_self.mpr h₀, abs_sub_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n : ℕ
v w : Fin (n + 1) → K
i j : Fin (n + 1)
hw : w i ≠ 0
⊢ projVandermonde v w i j = v i ^ ↑j * w i ^ n / w i ^ ↑j

Tactic:
projVandermonde_apply,

Goal state after:
K : Type u_2
inst✝ : Field K
n : ℕ
v w : Fin (n + 1) → K
i j : Fin (n + 1)
hw : w i ≠ 0
⊢ v i ^ ↑j * w i ^ ↑j.rev = v i ^ ↑j * w i ^ n / w i ^ ↑j
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
j : Fin (n + 1)
hlt : j < last n
⊢ projVandermonde v w i j = Pi.single (last n) (v i ^ n) j

Tactic:
projVandermonde_apply,

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
j : Fin (n + 1)
hlt : j < last n
⊢ v i ^ ↑j * w i ^ ↑j.rev = Pi.single (last n) (v i ^ n) j
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.choose b) = eval (↑(a - (b - 1))) (ascPochhammer K b) / ↑b !

Tactic:
eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0),

Goal state after:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.choose b) * ↑b ! = eval (↑(a - (b - 1))) (ascPochhammer K b)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.choose b) = eval (↑a) (descPochhammer K b) / ↑b !

Tactic:
eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0),

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.choose b) * ↑b ! = eval (↑a) (descPochhammer K b)
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ.inr.inr
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
i₀ : Fin (n + 1)
hi₀ : w i₀ ≠ 0
⊢ ∏ i, ∏ j > i, ((v ∘ ⇑(swap 0 i₀)) j * (w ∘ ⇑(swap 0 i₀)) i - (v ∘ ⇑(swap 0 i₀)) i * (w ∘ ⇑(swap 0 i₀)) j) =
    ↑↑(Perm.sign (swap 0 i₀)) * ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
← (Equiv.swap 0 i₀).prod_Ioi_comp_eq_sign_mul_prod (by simp)

Goal state after:
case succ.inr.inr
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
i₀ : Fin (n + 1)
hi₀ : w i₀ ≠ 0
⊢ ∏ i, ∏ j > i, ((v ∘ ⇑(swap 0 i₀)) j * (w ∘ ⇑(swap 0 i₀)) i - (v ∘ ⇑(swap 0 i₀)) i * (w ∘ ⇑(swap 0 i₀)) j) =
    ∏ i, ∏ j > i, (v ((swap 0 i₀) j) * w ((swap 0 i₀) i) - v ((swap 0 i₀) i) * w ((swap 0 i₀) j))
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ ≠ 0

Tactic:
exact inv_ne_zero (sub_ne_zero_of_ne hxy)

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree = (X ^ Fintype.card ↥G).degree

Tactic:
degree_nodal,

Goal state after:
case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ↑(#(↑G).toFinset) = (X ^ Fintype.card ↥G).degree
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
⊢ ∏ j ∈ s.erase i, (v i - v j)⁻¹ = (∏ i_1 ∈ s.erase i, (v i - v i_1))⁻¹

Tactic:
prod_inv_distrib

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
⊢ (∏ x ∈ s.erase i, (v i - v x))⁻¹ = (∏ i_1 ∈ s.erase i, (v i - v i_1))⁻¹
Module: Mathlib.Algebra.Lie.CartanCriterion

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

Tactic:
simp [toMatrix_apply, hyv, hsv]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
this : (univ ℤ n).coeff (Fintype.card n) = 1
⊢ (univ R n).coeff (Fintype.card n) = 1

Tactic:
← univ_map_map n (Int.castRingHom R),

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
this : (univ ℤ n).coeff (Fintype.card n) = 1
⊢ (Polynomial.map (MvPolynomial.map (Int.castRingHom R)) (univ ℤ n)).coeff (Fintype.card n) = 1
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case hg
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ∀ (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M),
    (toMvPolynomial b (Free.chooseBasis R M).end φ i).IsHomogeneous 1

Tactic:
· exact LinearMap.toMvPolynomial_isHomogeneous _ _ _

Goal state after: