mathlib-initiative/mathlib-tactics huggingface dataset:
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
i : ι
this : P.root i ∈ span ℕ (⇑P.root '' ↑b.support) ∨ -P.root i ∈ span ℕ (⇑P.root '' ↑b.support)
⊢ P.root i ∈ span ℤ (⇑P.root '' ↑b.support)

Tactic:
← span_span_of_tower (R := ℕ)

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
i : ι
this : P.root i ∈ span ℕ (⇑P.root '' ↑b.support) ∨ -P.root i ∈ span ℕ (⇑P.root '' ↑b.support)
⊢ P.root i ∈ span ℤ ↑(span ℕ (⇑P.root '' ↑b.support))
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 : ι
inst✝ : P.IsReduced
h : P.root i - P.root j ∈ range ⇑P.root
h' : LinearIndependent R ![P.root i, P.root j]
⊢ P.root j - P.root i ∈ range ⇑P.root

Tactic:
← neg_mem_range_root_iff,

Goal state after:
ι : 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 : ι
inst✝ : P.IsReduced
h : P.root i - P.root j ∈ range ⇑P.root
h' : LinearIndependent R ![P.root i, P.root j]
⊢ -(P.root j - P.root i) ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : LinearIndependent R ![P.root i, P.root j]
h₁ : P.pairing j i = 1
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
← neg_mem_range_root_iff,

Goal state after:
case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : LinearIndependent R ![P.root i, P.root j]
h₁ : P.pairing j i = 1
⊢ -(P.root i - P.root j) ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case inr.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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
pos : 0 < f
⊢ False

pp: case inr.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
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
neg : f < 0
⊢ False

Tactic:
· simpa [hij, f] using le_of_lt pos j

Goal state after:
case inr.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
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
neg : f < 0
⊢ False
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 : ι
⊢ chainBotCoeff i j = 0 ↔ ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j - P.root i ∉ range ⇑P.root

Tactic:
by
  by_cases h : LinearIndependent R ![P.root i, P.root j]
  swap; · simp [chainBotCoeff_of_not_linearIndependent h, h]
  have : P.chainBotCoeff i j = 0 ↔ Iic (P.chainBotCoeff i j) = {0} := by
    simpa [Set.ext_iff, mem_Iic, mem_singleton_iff] using ⟨fun h ↦ by simp [h], fun h ↦ by rw [← h]⟩
  simp only [h, not_true_eq_false, false_or, this, Iic_chainBotCoeff_eq h, Set.ext_iff,
    mem_ofPred_eq, mem_singleton_iff]
  refine ⟨fun h' ↦ by simpa using h' 1, fun h' n ↦ ⟨fun h'' ↦ ?_, fun h'' ↦ by simp [h'']⟩⟩
  replace h' : 1 ∉ {k | P.root j - k • P.root i ∈ range P.root} := by simpa using h'
  rw [← Iic_chainBotCoeff_eq h, mem_Iic, not_le, Nat.lt_one_iff] at h'
  rw [root_sub_nsmul_mem_range_iff_le_chainBotCoeff h] at h''
  lia

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
f : M →+ ℚ
hf : ∀ i ∈ s, f (P.root i) = 1
_i : InvolutiveNeg ι := P.indexNeg
h_card : (baseOf (⇑P.root) f).ncard = s.ncard
hsp : ∀ (i : ι), ∃ z, f (P.root i) = ↑z
i : ι
hi : i ∈ s
j k : ι
n : ℤ
hn : f (P.root j) = ↑n
m : ℤ
hm : f (P.root k) = ↑m
hj : 0 < n
hk : 0 < m
contra : 1 = ↑(n + m)
⊢ 1 = n + m

Tactic:
← Int.cast_one,

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
s : Set ι
hli : LinearIndepOn R (⇑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
hsp : ∀ (i : ι), ∃ z, f (P.root i) = ↑z
i : ι
hi : i ∈ s
j k : ι
n : ℤ
hn : f (P.root j) = ↑n
m : ℤ
hm : f (P.root k) = ↑m
hj : 0 < n
hk : 0 < m
contra : ↑1 = ↑(n + m)
⊢ 1 = n + m
Module: Mathlib.LinearAlgebra.Matrix.BilinearForm

Goal state before:
pp: R₂ : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
inst✝² : IsDomain R₂
inst✝¹ : Free R₂ M₂
inst✝ : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
⊢ B.Nondegenerate ↔ ker B = ⊥

Tactic:
refine ⟨Nondegenerate.ker_eq_bot, fun h ↦ .ofSeparatingLeft ?_⟩

Goal state after:
R₂ : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
inst✝² : IsDomain R₂
inst✝¹ : Free R₂ M₂
inst✝ : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
h : ker B = ⊥
⊢ SeparatingLeft B
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
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
q : Submodule R M
⊢ (∀ i ∈ b.support, q ∈ invtSubmodule ↑(P.reflection i)) ↔ ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)

Tactic:
by
  refine ⟨fun hq i ↦ ?_, fun hq i _ ↦ hq i⟩
  let := P.indexNeg
  have (j : ι) : P.reflection (-j) = P.reflection j := by ext x; simp [reflection_apply, two_smul]
  refine b.induction_reflect i (by simp_all) hq ?_
  clear i
  intro i j hi hj
  rw [reflection_reflectionPerm]
  exact Module.End.invtSubmodule.comp _ (Module.End.invtSubmodule.comp _ (hq j hj) hi) (hq j hj)

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:
rw [← const_sub, const_pos, sub_pos]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : b ≤ c
ha : a < c
⊢ a ⊔ b ≤ c

Tactic:
obtain hb | hb := hb
    · exact Or.inl (CauSeq.sup_lt ha hb)
    · replace ha := le_of_le_of_eq ha.le (Setoid.symm hb)
      refine le_of_le_of_eq (Or.inr ?_) hb
      exact CauSeq.sup_eq_right ha

Goal state after:
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).IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_zpow, h]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : 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)) μ
i : n
⊢ b i ∈ eigenspace ((toLin b b) (diagonal d)) (d i)

Tactic:
mem_eigenspace_iff

Goal state after:
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)) μ
i : n
⊢ ((toLin b b) (diagonal d)) (b i) = d i • b i
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : n → R
h : 0 ≤ d
x : n →₀ R
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * diagonal d i j * xj

Tactic:
refine Finsupp.sum_nonneg fun i _ ↦ Finsupp.sum_nonneg fun j _ ↦ ?_
    simp +contextual [diagonal, apply_ite, star_left_conjugate_nonneg (h _)]

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosSemidef
this : (1 * x).PosSemidef
⊢ x.PosSemidef

Tactic:
one_mul

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosSemidef
this : x.PosSemidef
⊢ x.PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosDef
this : (1 * x).PosDef
⊢ x.PosDef

Tactic:
one_mul

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosDef
this : x.PosDef
⊢ x.PosDef
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
⊢ |(N *ᵥ v) i| = |∑ j, N i j * v j|

Tactic:
simp [mulVec_eq_sum, mul_comm]

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

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

Tactic:
simp [mulVec_eq_sum, mul_comm]

Goal state after:
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
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ ((aeval f) p) x = eval μ p • x

Tactic:
refine p.induction_on ?_ ?_ ?_

Goal state after:
case refine_1
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ ∀ (a : R), ((aeval f) (C a)) x = eval μ (C a) • x

case refine_2
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ ∀ (p q : R[X]),
    ((aeval f) p) x = eval μ p • x → ((aeval f) q) x = eval μ q • x → ((aeval f) (p + q)) x = eval μ (p + q) • x

case refine_3
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ ∀ (n : ℕ) (a : R),
    ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x →
      ((aeval f) (C a * X ^ (n + 1))) x = eval μ (C a * X ^ (n + 1)) • x
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
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker ((aeval f) (C q.leadingCoeff * X + C (q.coeff 0))) = LinearMap.ker ((aeval f) q)

Tactic:
← eq_X_add_C_of_degree_eq_one

Goal state after:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker ((aeval f) q) = LinearMap.ker ((aeval f) q)

K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ q.degree = 1
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
⊢ eval 0 (descPochhammer R n) = if n = 0 then 1 else 0

Tactic:
cases n
  · simp
  · simp [X_mul, descPochhammer_succ_left]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
d : ι → K
hp : d ∈ p
hf : ∀ (i : ι ⊕ ↑{(i, j) | i ≠ j}), (f i) d ≠ 0
⊢ ∃ d ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)

Tactic:
refine ⟨d, hp, fun i ↦ hf (Sum.inl i), fun i j h ↦ ?_⟩

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
d : ι → K
hp : d ∈ p
hf : ∀ (i : ι ⊕ ↑{(i, j) | i ≠ j}), (f i) d ≠ 0
i j : ι
h : i ≠ j
⊢ ((fun x1 x2 ↦ x1 ≠ x2) on d) i j
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case inl
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
s : S
h : ↑n - 1 ≤ s
heq : ↑n - 1 = s
⊢ 0 ≤ eval 0 (ascPochhammer S n)

Tactic:
ascPochhammer_eval_zero

Goal state after:
case inl
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
s : S
h : ↑n - 1 ≤ s
heq : ↑n - 1 = s
⊢ 0 ≤ if n = 0 then 1 else 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
hs : s.Nonempty
⊢ ∑ j ∈ s, Lagrange.basis s v j = 1

Tactic:
refine eq_of_degrees_lt_of_eval_index_eq s hvs (lt_of_le_of_lt (degree_sum_le _ _) ?_) ?_ ?_
  · rw [Nat.cast_withBot, Finset.sup_lt_iff (WithBot.bot_lt_coe #s)]
    intro i hi
    rw [degree_basis hvs hi, Nat.cast_withBot, WithBot.coe_lt_coe]
    exact Nat.pred_lt (card_ne_zero_of_mem hi)
  · rw [degree_one, ← WithBot.coe_zero, Nat.cast_withBot, WithBot.coe_lt_coe]
    exact Nonempty.card_pos hs
  · intro i hi
    rw [eval_finsetSum, eval_one, ← add_sum_erase _ _ hi, eval_basis_self hvs hi,
      add_eq_left]
    refine sum_eq_zero fun j hj => ?_
    rcases mem_erase.mp hj with ⟨hij, _⟩
    rw [eval_basis_of_ne hij hi]

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 : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∑ x ∈ s, 1 * Lagrange.basis s v x = 1

Tactic:
one_mul

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∑ x ∈ s, Lagrange.basis s v x = 1
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
⊢ 1 * (monomial d) 1 = (monomial d) 1

Tactic:
one_mul

Goal state after:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
⊢ (monomial d) 1 = (monomial d) 1
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
h : j ∈ ((bind₁ f) φ).vars
⊢ ∃ i ∈ φ.vars, j ∈ (f i).vars

Tactic:
by
  classical
  simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne] using vars_bind₁ f φ h

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

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

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

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

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

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

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
⊢ ((toMatrix b b) f).charpoly = f.charpoly

Tactic:
by
  nontriviality R
  unfold LinearMap.charpoly
  set b' := chooseBasis R M
  rw [← basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix b b' b b']
  set P := b.toMatrix b'
  set A := toMatrix b' b' f
  set Q := b'.toMatrix b
  let e := Basis.indexEquiv b b'
  let ι' := ChooseBasisIndex R M
  let φ := reindexLinearEquiv R R e e
  let φ₁ := reindexLinearEquiv R R e (Equiv.refl ι')
  let φ₂ := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
  let φ₃ := reindexLinearEquiv R R (Equiv.refl ι') e
  calc
    (P * A * Q).charpoly = (φ (P * A * Q)).charpoly := (charpoly_reindex ..).symm
    _ = (φ₁ P * φ₂ A * φ₃ Q).charpoly := by rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
    _ = A.charpoly := by rw [charpoly_mul_comm, ← mul_assoc]; simp [P, Q, φ₁, φ₂, φ₃]

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 : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
⊢ nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (1 * ∏ x_1 ∈ s.erase i, (x - v x_1))

Tactic:
one_mul

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
⊢ nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * ∏ x_1 ∈ s.erase i, (x - v x_1)