mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.BilinearForm

Goal state before:
pp: R₁ : Type u_1
M₁ : Type u_2
inst✝⁸ : CommSemiring R₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
n : Type u_5
o : Type u_6
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₁ M₂'
c : Basis o R₁ M₂'
inst✝ : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
x y : M₂'
⊢ ((((toMatrix₂ b b).symm M).comp ((toLin c b) P) ((toLin c b) Q)) x) y =
    (((LinearMap.BilinForm.toMatrix c).symm (Pᵀ * M * Q)) x) y

Tactic:
LinearMap.BilinForm.toMatrix,

Goal state after:
R₁ : Type u_1
M₁ : Type u_2
inst✝⁸ : CommSemiring R₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
n : Type u_5
o : Type u_6
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₁ M₂'
c : Basis o R₁ M₂'
inst✝ : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
x y : M₂'
⊢ ((((toMatrix₂ b b).symm M).comp ((toLin c b) P) ((toLin c b) Q)) x) y = (((toMatrix₂ c c).symm (Pᵀ * M * Q)) 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
f : ℕ → β
g : CauSeq β abv
h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
⊢ abv (f j - f i) < ε

Tactic:
by
      obtain ⟨h₁, h₂⟩ := hi _ le_rfl; rw [abv_sub abv] at h₁
      have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi _ ij).1 h₁)
      have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add this (h₂ _ ij))
      rwa [add_halves, add_halves, add_right_comm, sub_add_sub_cancel, sub_add_sub_cancel] at this

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

Goal state before:
pp: C : ℝ → Prop
x : ℝ
h : ∀ (y : CauSeq ℚ abs), C (mk y)
⊢ C x

Tactic:
by
  obtain ⟨x⟩ := x
  induction x using Quot.induction_on
  exact h _

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

Goal state before:
pp: ⊢ 0 < 1

Tactic:
by
  convert! ratCast_lt.2 zero_lt_one <;> simp [← ofCauchy_ratCast, ofCauchy_one, ofCauchy_zero]

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

Goal state before:
pp: case neg
m : Type u_1
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
ι : Type u_5
inst✝ : AddLeftMono R
A : ι → Matrix m m R
i : ι
hi : Finset ι
hins : i ∉ hi
H : hi.Nonempty → (∀ i ∈ hi, (A i).PosDef) → (∑ i ∈ hi, A i).PosDef
hs : (insert i hi).Nonempty
hA : ∀ i_1 ∈ insert i hi, (A i_1).PosDef
h : ¬¬hi.Nonempty
⊢ (A i + ∑ x ∈ hi, A x).PosDef

Tactic:
exact PosDef.add (hA _ <| Finset.mem_insert_self i hi) <|
          H (not_not.mp h) fun _ _hi => hA _ (Finset.mem_insert_of_mem _hi)

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

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Q.toMatrix'.PosDef
⊢ QuadraticMap.PosDef Q

Tactic:
rw [← Q.toQuadraticMap_associated ℝ,
    ← (LinearMap.toMatrix₂' ℝ).left_inv (Q.associatedHom ℝ)]
  exact hQ.toQuadraticForm'

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
P : RootPairing ι R M N
b : P.Base
inst✝¹ : P.IsCrystallographic
inst✝ : CharZero R
i j : ↥b.support
⊢ P.pairingIn ℤ ↑i ↑j = 0 ↔ P.pairing ↑i ↑j = 0

Tactic:
← (algebraMap_injective ℤ R).eq_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
i j : ↥b.support
⊢ (algebraMap ℤ R) (P.pairingIn ℤ ↑i ↑j) = (algebraMap ℤ R) 0 ↔ P.pairing ↑i ↑j = 0
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
⊢ b.cartanMatrix i j ∈ {-3, -2, -1, 0}

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
  have : Module.IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
  simp only [cartanMatrix, cartanMatrixIn_def]
  have h₁ := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
  have h₂ : P.pairingIn ℤ i j ≤ 0 := b.cartanMatrix_le_zero_of_ne i j hij
  suffices P.pairingIn ℤ i j ≠ -4 by aesop
  by_contra contra
  replace contra : P.pairingIn ℤ j i = -1 ∧ P.pairingIn ℤ i j = -4 := ⟨by simp_all, contra⟩
  rw [pairingIn_neg_one_neg_four_iff] at contra
  refine (not_linearIndependent_iff.mpr ?_) b.linearIndepOn_root
  refine ⟨⟨{i, j}, by simpa⟩, Finsupp.single i (1 : R) + Finsupp.single j (2 : R), ?_⟩
  simp [contra, hij, hij.symm]

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

Goal state before:

Tactic:
(ρ - μ) * |v i|
          = |μ - ρ| * |v i| := by rw [← abs_eq_self.mpr h₀, abs_sub_comm]
        _ = |(N *ᵥ v) i| := by simp [hv]
        _ = |∑ j, N i j * v j| := by simp [mulVec_eq_sum, mul_comm]
        _ ≤ ∑ j, |N i j * v j| := Finset.abs_sum_le_sum_abs _ _
        _ = ∑ j, N i j * |v j| := by simp [abs_eq_self.mpr (hN i _)]
        _ = (N *ᵥ |v|) i := by 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
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : (minpoly R f).degree ≤ q.degree
⊢ False

Tactic:
rw [hq, degree_mul, degree_X_sub_C, degree_eq_natDegree] at this

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
μ : R
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : 1 + ↑q.natDegree ≤ ↑q.natDegree
⊢ False

R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
μ : R
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : 1 + q.degree ≤ q.degree
⊢ q ≠ 0
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case mem
ι : 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
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), P.root ↑k ∈ q ↔ p k
k : ↥b.support
x✝ x : M
hx : x ∈ ⇑P.root ∘ Subtype.val '' {i | p i}
hk : (P.coroot' ↑k) x ≠ 0
⊢ p k

Tactic:
| mem x hx =>

Goal state after:
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
⊢ ¬q.leadingCoeff = 0

Tactic:
leadingCoeff_eq_zero_iff_deg_eq_bot,

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
⊢ ¬q.degree = ⊥
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
t : T
⊢ eval t (ascPochhammer T n) = eval₂ f t (ascPochhammer S n)

Tactic:
by
  rw [← ascPochhammer_map f]
  exact eval_map f t

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 ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
this : ∀ (k : ι), P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k
⊢ (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix

Tactic:
by
      ext; simp [f', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]

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 ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
⊢ f' = g'

Tactic:
replace hf : (fun k : b.support ↦ P.pairingIn ℤ i k) = f' ᵥ* b.cartanMatrix := by
    suffices ∀ k, P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k by
      ext; simp [f', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]
    refine fun k ↦ algebraMap_injective ℤ R ?_
    simp_rw [algebraMap_pairingIn, map_sum, map_mul, algebraMap_pairingIn,
      ← P.root_coroot'_eq_pairing]
    simp [hf]

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✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
⊢ f' = g'
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.ascFactorial b) = eval (↑a) (ascPochhammer S b)

Tactic:
by
  rw [← ascPochhammer_nat_eq_ascFactorial, ascPochhammer_eval_cast]

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.descFactorial b) = eval (↑(a - (b - 1))) (ascPochhammer S b)

Tactic:
← ascPochhammer_eval_cast,

Goal state after:
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.descFactorial b) = ↑(eval (a - (b - 1)) (ascPochhammer ℕ b))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n : ℕ
hn : (descPochhammer R n).natDegree = n
⊢ (descPochhammer R (n + 1)).natDegree = n + 1

Tactic:
have : natDegree (X - (n : R[X])) = 1 := natDegree_X_sub_C (n : R)

Goal state after:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n : ℕ
hn : (descPochhammer R n).natDegree = n
this : (X - ↑n).natDegree = 1
⊢ (descPochhammer R (n + 1)).natDegree = n + 1
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
P✝ : RootPairing ι R M N
inst✝¹⁵ : P✝.IsValuedIn S
b✝ : P✝.Base
inst✝¹⁴ : P✝.IsCrystallographic
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
inst✝² : Finite ι₂
inst✝¹ : P₂.IsRootSystem
inst✝ : P₂.IsReduced
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
f : M ≃ₗ[R] M₂ := b.toWeightBasis.equiv b₂.toWeightBasis e
⊢ ∀ (m : M), f m ∈ range ⇑P₂.root ↔ m ∈ range ⇑P.root

Tactic:
by
    refine fun m ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
    · simpa using apply_mem_range_root_of_cartanMatrixEq _ b e.symm f.symm
        (by simp [f, Module.Basis.equiv]) (f m) h (by simp [(he _ _).symm])
    · exact apply_mem_range_root_of_cartanMatrixEq b b₂ e f (by simp [f, Module.Basis.equiv]) m h he

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

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
a : S
ha : a ∈ Set.Ici (↑(n + 1) - 1)
b : S
hb : b ∈ Set.Ici (↑(n + 1) - 1)
hab : a ≤ b
⊢ (fun x ↦ eval x (descPochhammer S (n + 1))) a ≤ (fun x ↦ eval x (descPochhammer S (n + 1))) b

Tactic:
rw [Set.mem_Ici, Nat.cast_add_one, add_sub_cancel_right] at ha hb

Goal state after:
case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
a : S
ha : ↑n ≤ a
b : S
hb : ↑n ≤ b
hab : a ≤ b
⊢ (fun x ↦ eval x (descPochhammer S (n + 1))) a ≤ (fun x ↦ eval x (descPochhammer S (n + 1))) b
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
i : ι
hi : i ∈ s
⊢ eval (v i) (Lagrange.basis s v i) + ∑ x ∈ s.erase i, eval (v i) (Lagrange.basis s v x) = 1

Tactic:
eval_basis_self hvs hi,

Goal state after:
case refine_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
i : ι
hi : i ∈ s
⊢ 1 + ∑ x ∈ s.erase i, eval (v i) (Lagrange.basis s v x) = 1
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
⊢ r i * eval (v i) (Lagrange.basis s v i) + ∑ x ∈ s.erase i, r x * eval (v i) (Lagrange.basis s v x) = r i

Tactic:
eval_basis_self hvs hi,

Goal state after:
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
⊢ r i * 1 + ∑ x ∈ s.erase i, r x * eval (v i) (Lagrange.basis s v x) = r i
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ X - C (v i) ∣ nodal s v

Tactic:
classical
  exact ⟨nodal (s.erase i) v, nodal_eq_mul_nodal_erase hi⟩

Goal state after:
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
⊢ IsNilpotent (↥(derivedSeries R L 1)) M

Tactic:
set A := AlgebraicClosure (FractionRing R)

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
⊢ IsNilpotent (↥(derivedSeries R L 1)) M
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case pos
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(((decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
h✝ : k + i = j
⊢ ↑⟨↑(((decompose 𝒜) r) k) * x, mem₁⟩ ∈ I

pp: case neg
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(((decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
h✝ : ¬k + i = j
⊢ ↑0 ∈ I

Tactic:
· exact I.mul_mem_left _ hx₂

Goal state after:
case neg
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(((decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
h✝ : ¬k + i = j
⊢ ↑0 ∈ I
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: case h
R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
x✝ : ∀ (m : M), ∃ n, (φ ^ n) m = 0
h : ∀ (m : M), ∃ n, (φ ^ n) m = 0 := x✝
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → ⨆ m, (φ ^ m).ker = (φ ^ b).ker
x : M
⊢ (φ ^ n) x = 0

Tactic:
← mem_ker,

Goal state after:
case h
R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
x✝ : ∀ (m : M), ∃ n, (φ ^ n) m = 0
h : ∀ (m : M), ∃ n, (φ ^ n) m = 0 := x✝
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → ⨆ m, (φ ^ m).ker = (φ ^ b).ker
x : M
⊢ x ∈ ker (φ ^ n)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ ((rename f) φ).IsHomogeneous n

Tactic:
rw [← φ.support_sum_monomial_coeff, map_sum]

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ (∑ x ∈ φ.support, (rename f) ((monomial x) (coeff x φ))).IsHomogeneous n
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weight w)) φ.support
⊢ 0 = (weightedHomogeneousComponent w m) φ

Tactic:
weightedHomogeneousComponent_eq_zero_of_notMem w φ m hm

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weight w)) φ.support
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
⊢ finrank K ↥V = (charpoly φ).natTrailingDegree

Tactic:
let G := φ.restrict hφW

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
⊢ finrank K ↥V = (charpoly φ).natTrailingDegree
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
⊢ i ≤ n

Tactic:
contrapose! hi

Goal state after:
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : n < i
⊢ ((finSuccEquiv R N) F).coeff i = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
hnR : ↑n ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
F : MvPolynomial (Fin k) R
hF : ((rename f) F).IsHomogeneous n
h : (rename f) F ≠ 0
hF₀ : F ≠ 0
⊢ F.IsHomogeneous n

Tactic:
rename_isHomogeneous_iff hf

Goal state after:
R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
hnR : ↑n ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
F : MvPolynomial (Fin k) R
hF : F.IsHomogeneous n
h : (rename f) F ≠ 0
hF₀ : F ≠ 0
⊢ F.IsHomogeneous n
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: K : Type u
V : Type v
V' : Type v'
inst✝⁵ : Semiring K
inst✝⁴ : AddCommMonoid V
inst✝³ : Module K V
inst✝² : AddCommMonoid V'
inst✝¹ : Module K V'
inst✝ : Nontrivial K
⊢ rank 0 = 0

Tactic:
by
  rw [rank, LinearMap.range_zero, rank_bot]

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
simp [Pso, indefiniteDiagonal, h, hi, one_apply]

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
simp [Pso, indefiniteDiagonal, h, hi, one_apply]

Goal state after: