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

Goal state before:
pp: case pos
ι : 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 : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
S₁ : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₁_def : S₁ = {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
hS₁₂ :
  Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j)) =
    (fun z ↦ -↑(chainTopCoeff i j) + z) '' Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
hS₁ : S₁ = Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
hS₂ : S₂ = Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j))
⊢ chainBotCoeff i (chainTopIdx i j) = chainBotCoeff i j + chainTopCoeff i j ∧ chainTopCoeff i (chainTopIdx i j) = 0

Tactic:
image_const_add_Icc,

Goal state after:
case pos
ι : 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 : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
S₁ : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₁_def : S₁ = {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
hS₁₂ :
  Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j)) =
    Icc (-↑(chainTopCoeff i j) + -↑(chainBotCoeff i j)) (-↑(chainTopCoeff i j) + ↑(chainTopCoeff i j))
hS₁ : S₁ = Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
hS₂ : S₂ = Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j))
⊢ chainBotCoeff i (chainTopIdx i j) = chainBotCoeff i j + chainTopCoeff i j ∧ chainTopCoeff i (chainTopIdx i j) = 0
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
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
this : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos (-i)
⊢ p i

Tactic:
· suffices p (-i) by rw [← neg_neg i]; exact h₀ (-i) this
    exact hi.induction_on_reflect h₁ h₂

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : a ≤ b
⊢ a ⊔ b ≈ b

Tactic:
obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(b - a) j
⊢ a ⊔ b ≈ b

case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : a ≈ b
⊢ a ⊔ b ≈ b
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≤ a
⊢ a ⊓ b ≈ b

Tactic:
obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
⊢ a ⊓ b ≈ b

case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≈ a
⊢ a ⊓ b ≈ b
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ n)ᴴ = Aᴴ ^ n

Tactic:
conjTranspose_pow

Goal state after:
n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ Aᴴ ^ n = Aᴴ ^ n
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ (n + 1))ᴴ⁻¹ = (Aᴴ ^ (n + 1))⁻¹

Tactic:
conjTranspose_pow

Goal state after:
n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (Aᴴ ^ (n + 1))⁻¹ = (Aᴴ ^ (n + 1))⁻¹
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
hA : Function.Injective A.mulVec
⊢ (Aᴴ * A).PosDef

Tactic:
classical
  simpa using conjTranspose_mul_mul_same .one hA

Goal state after:
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: case cons
α : Type u_1
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ ∏ i ∈ cons a s has, (f i)! ∣ (∑ i ∈ cons a s has, f i)!

Tactic:
rw [prod_cons, Finset.sum_cons]

Goal state after:
case cons
α : Type u_1
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ (f a)! * ∏ x ∈ s, (f x)! ∣ (f a + ∑ x ∈ s, f x)!
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
i j : ι
h : i ≠ j
⊢ ∃ k ∈ b.support, P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k

Tactic:
contrapose! 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
i j : ι
h : ∀ k ∈ b.support, P.pairingIn ℤ i k = P.pairingIn ℤ j k
⊢ i = j
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
n k : ℕ
⊢ eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)

Tactic:
induction k with

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x : F
⊢ basisDivisor x x = 0

Tactic:
simp only [basisDivisor, sub_self, inv_zero, map_zero, zero_mul]

Goal state after:
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
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right✝ : j ∈ s
⊢ eval (v i) (Lagrange.basis s v j) = 0

Tactic:
rw [eval_basis_of_ne hij hi]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: 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
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ (∏ x, (w 0 * v x.succ - v 0 * w x.succ)) * ∏ x, ∏ x_1 > x, (w x.succ * v x_1.succ - v x.succ * w x_1.succ) =
    ∏ x, ∏ x_1 > x, (w x * v x_1 - v x * w x_1)

Tactic:
simp only [prod_univ_succ, Ioi_zero_eq_map, Finset.prod_map, coe_succEmb, prod_Ioi_succ]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
⊢ (∏ i ∈ s, (X - C (v i))).natDegree = #s

Tactic:
natDegree_prod_of_monic (h := fun i _ => monic_X_sub_C (v i)),

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
⊢ ∑ i ∈ s, (X - C (v i)).natDegree = #s
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
⊢ eval (v i) (nodal s v) = 0

Tactic:
by
  rw [eval_nodal]
  exact s.prod_eq_zero hi (sub_self (v i))

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : SemilatticeSup M
w : σ → M
p : MvPolynomial σ R
⊢ weightedTotalDegree' w p = ⊥ ↔ p = 0

Tactic:
simp only [weightedTotalDegree', Finset.sup_eq_bot_iff, mem_support_iff, WithBot.coe_ne_bot,
    MvPolynomial.eq_zero_iff]
  exact forall_congr' fun _ => Classical.not_not

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
⊢ ∑ i ∈ Finite.toFinset ⋯, (weightedHomogeneousComponent w i) φ = φ

Tactic:
ext1 d

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i ∈ Finite.toFinset ⋯, (weightedHomogeneousComponent w i) φ) = coeff d φ
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (∏ _i ∈ Finset.range n, φ).IsHomogeneous (∑ _i ∈ Finset.range n, m)

Tactic:
apply IsHomogeneous.prod _ _ _ (fun _ _ ↦ hφ)

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

Goal state before:
pp: 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
h : charpoly φ = X ^ finrank R M
m : M
⊢ ∃ n, (φ ^ n) m = 0

Tactic:
use finrank R M
    suffices φ ^ finrank R M = 0 by simp only [this, LinearMap.zero_apply]
    simpa only [h, map_pow, aeval_X] using φ.aeval_self_charpoly

Goal state after:
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
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun a m ↦ (AddMonoidHom.id ℕ) m) = n

Tactic:
convert! h (mem_support_iff.mp hd)

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun a m ↦ (AddMonoidHom.id ℕ) m) = (weight 1) d
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)

Tactic:
split_ifs <;>
    simp only [zero_coeff, coeff_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff (cons i d) φ ≠ 0
⊢ (weight 1) d = j

Tactic:
have h' : (weight 1) (Finsupp.cons i d) = i + j := by
    simpa [Finset.sum_subset_zero_on_sdiff (g := d.cons i)
     (d.cons_support (y := i)) (by simp) (fun _ _ ↦ rfl), ← h] using hφ hd

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff (cons i d) φ ≠ 0
h' : (weight 1) (cons i d) = i + j
⊢ (weight 1) d = j
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
⊢ (weightedHomogeneousComponent w 0) φ = C (coeff 0 φ)

Tactic:
ext1 d

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
⊢ coeff d ((weightedHomogeneousComponent w 0) φ) = coeff d (C (coeff 0 φ))
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
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✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    (toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij kl = if kl = ij then 1 else 0
⊢ (monomial (Finsupp.single ij 1)) ((toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij ij) = X ij

Tactic:
rw [this, if_pos rfl, X]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = 0
hnR : ↑n ≤ #R
⊢ F = 0

Tactic:
contrapose! h

Goal state after:
R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hnR : ↑n ≤ #R
h : F ≠ 0
⊢ ∃ r, (eval r) F ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ ∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ = φ

Tactic:
ext1 d

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ) = coeff d φ
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: 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
inst✝¹ : Module.Finite R L
inst✝ : Free R L
x : L
⊢ φ.IsNilRegular x ↔ (eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0

Tactic:
rw [IsNilRegular, polyCharpoly_coeff_eval]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (-(1 • 1)).det = 1

Tactic:
← neg_smul,

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (-1 • 1).det = 1
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ A ∈ ↑(skewAdjointMatricesLieSubalgebra (unitOfInvertible 2 • S l R)) ↔ A ∈ ↑(so' l l R)

Tactic:
LieSubalgebra.mem_coe,

Goal state after:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ A ∈ skewAdjointMatricesLieSubalgebra (unitOfInvertible 2 • S l R) ↔ A ∈ ↑(so' l l R)
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)

Tactic:
set f := fun (x : Matrix l l R) ↦ x.submatrix s.symm s.symm

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
A : Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R
⊢ A ∈
      ↑(skewAdjointMatricesLieSubalgebra
          ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l)) (indefiniteDiagonal (Unit ⊕ l) l R))) ↔
    A ∈ ↑(skewAdjointMatricesLieSubalgebra (unitOfInvertible 2 • fromBlocks 1 0 0 (S l R)))

Tactic:
LieSubalgebra.mem_coe,

Goal state after:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
A : Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R
⊢ A ∈
      skewAdjointMatricesLieSubalgebra
        ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l)) (indefiniteDiagonal (Unit ⊕ l) l R)) ↔
    A ∈ ↑(skewAdjointMatricesLieSubalgebra (unitOfInvertible 2 • fromBlocks 1 0 0 (S l R)))
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
A : Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R
⊢ A ∈
      skewAdjointMatricesLieSubalgebra
        ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l)) (indefiniteDiagonal (Unit ⊕ l) l R)) ↔
    A ∈ ↑(skewAdjointMatricesLieSubalgebra (unitOfInvertible 2 • fromBlocks 1 0 0 (S l R)))

Tactic:
LieSubalgebra.mem_coe,

Goal state after:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
A : Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R
⊢ A ∈
      skewAdjointMatricesLieSubalgebra
        ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l)) (indefiniteDiagonal (Unit ⊕ l) l R)) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (unitOfInvertible 2 • fromBlocks 1 0 0 (S l R))
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case h.refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
t : Finset K := (constantCoeff ψ).roots.toFinset
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
⊢ r ≤ (s \ t).card

Tactic:
refine le_trans ?_ (Finset.le_card_sdiff _ _)

Goal state after:
case h.refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
t : Finset K := (constantCoeff ψ).roots.toFinset
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
⊢ r ≤ s.card - t.card
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
⊢ LinearIndependent R w'

Tactic:
have hli' := Pi.linearIndependent_single_of_ne_zero (R := R)
      (v := fun i : m ↦ if w i = 0 then (1 : R) else w i) (by simp [ite_eq_iff'])

Goal state after:
m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
hli' : LinearIndependent R fun i ↦ Pi.single i (if w i = 0 then 1 else w i)
⊢ LinearIndependent R w'
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
x✝² x✝¹ : Derivation R A A
x✝ : A
⊢ x✝² (x✝¹ x✝) = ⁅x✝², x✝¹⁆ x✝ + x✝¹ (x✝² x✝)

Tactic:
commutator_apply

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
x✝² x✝¹ : Derivation R A A
x✝ : A
⊢ x✝² (x✝¹ x✝) = x✝² (x✝¹ x✝) - x✝¹ (x✝² x✝) + x✝¹ (x✝² x✝)