mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Cauchy abv
f : CauSeq β abv
hf : ⟦f⟧ ≠ 0
⊢ (⟦f⟧)⁻¹ * ⟦f⟧ = 1

Tactic:
simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf

Goal state after:
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ (⟦f⟧)⁻¹ * ⟦f⟧ = 1
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 : Cauchy abv
f : CauSeq β abv
hf : ⟦f⟧ ≠ 0
⊢ ⟦f⟧ * (⟦f⟧)⁻¹ = 1

Tactic:
simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf

Goal state after:
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ ⟦f⟧ * (⟦f⟧)⁻¹ = 1
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 : Cauchy abv
f : CauSeq β abv
hf : ⟦f⟧ ≠ 0
⊢ ⟦f⟧ * (⟦f⟧)⁻¹ = 1

Tactic:
simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf
    simp only [mk_eq_mk, hf, not_false_eq_true, inv_mk, mk_mul]
    exact Quotient.sound (CauSeq.mul_inv_cancel hf)

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
⊢ (const abv (f.lim * g.lim) - f * g).LimZero

Tactic:
rw [h]

Goal state after:
α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
⊢ ((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)).LimZero
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ 0 < v ⬝ᵥ star v ↔ v ≠ 0

Tactic:
by
  simpa using dotProduct_star_self_pos_iff (v := star v)

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : f 1 ^ 2 = f 1
h : f 1 = 0
⊢ f 1 ≤ 1

Tactic:
rw [h]

Goal state after:
case inl
R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : f 1 ^ 2 = f 1
h : f 1 = 0
⊢ 0 ≤ 1
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : f 1 ^ 2 = f 1
h : f 1 = 1
⊢ f 1 ≤ 1

Tactic:
rw [h]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : A.IsHermitian
f : n ≃ m
⊢ ((Matrix.reindex f f) A).IsHermitian

Tactic:
by
  rw [reindex_apply]
  apply submatrix h

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

Goal state before:
pp: 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
⊢ M⁻¹.PosSemidef

Tactic:
by
  by_cases h : IsUnit M.det
  · have := (conjTranspose_mul_mul_same hM M⁻¹).conjTranspose
    rwa [mul_nonsing_inv_cancel_right _ _ h, conjTranspose_conjTranspose] at this
  · rw [nonsing_inv_apply_not_isUnit _ h]
    exact .zero

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

Goal state before:
pp: n : ℕ
⊢ sf 4 * n = sf 2 * 2 * n

Tactic:
Nat.mul_two

Goal state after:
n : ℕ
⊢ sf 4 * n = sf (2 + 2) * n
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i : ι
⊢ coroot ↑↑(b.baseSupportEquiv i) = b.h' i

Tactic:
let := b.isCartanSubalgebra
  suffices b.h' i ∈ corootSpace (b.baseSupp' i) by
    have _i : IsAddTorsionFree L := .of_isTorsionFree K L
    exact (eq_coroot_of_mem_corootSpace_of_two (b.baseSupp' i).val this (by simp [baseSupp'])).symm
  have h_mem : ⁅b.e i, b.f i⁆ ∈ H := by
    nth_rw 1 [(b.sl2 i).lie_e_f, b.cartan_eq_lieSpan]
    exact subset_lieSpan <| mem_range_self i
  have h_eq : b.h' i = ⟨⁅b.e i, b.f i⁆, h_mem⟩ := by simp [(b.sl2 i).lie_e_f, h']
  rw [h_eq]
  have he : b.e i ∈ rootSpace H (b.baseSupp i) :=
    (mem_genWeightSpace _ _ _).mpr fun ⟨z, hz⟩ ↦ ⟨1, by simp⟩
  have hf : b.f i ∈ rootSpace H (-b.baseSupp i) :=
    (mem_genWeightSpace _ _ _).mpr fun ⟨z, hz⟩ ↦ ⟨1, by simp [← eq_neg_iff_add_eq_zero]⟩
  exact (mem_corootSpace _).mpr <| Submodule.subset_span ⟨b.e i, he, b.f i, hf, rfl⟩

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
⊢ i = j

Tactic:
let f' : b.support → ℤ := f ∘ (↑)

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 : ι → ℤ
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
⊢ i = j
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
⊢ ∑ x ∈ s.erase i, eval (v i) (Lagrange.basis s v x) = 0

Tactic:
refine sum_eq_zero fun j hj => ?_

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
j : ι
hj : j ∈ s.erase i
⊢ eval (v i) (Lagrange.basis s v j) = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = Lagrange.basis {x, y} id x + ∑ x_1 ∈ {y}, Lagrange.basis {x, y} id x_1

Tactic:
sum_singleton,

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = Lagrange.basis {x, y} id x + Lagrange.basis {x, y} id y
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s✝ t : Finset ι
i j : ι
v✝ r r' : ι → F
s : Finset ι
v f g : ι → F
⊢ ∑ i ∈ s, C ((f + g) i) * Lagrange.basis s v i =
    ∑ x ∈ s, (C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x)

Tactic:
have h : (fun x => C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x) =
    (fun x => C ((f + g) x) * Lagrange.basis s v x) := by
      simp_rw [← add_mul, ← C_add, Pi.add_apply]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s✝ t : Finset ι
i j : ι
v✝ r r' : ι → F
s : Finset ι
v f g : ι → F
h :
  (fun x ↦ C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x) = fun x ↦
    C ((f + g) x) * Lagrange.basis s v x
⊢ ∑ i ∈ s, C ((f + g) i) * Lagrange.basis s v i =
    ∑ x ∈ s, (C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s✝ t : Finset ι
i j : ι
v✝ r r' : ι → F
s : Finset ι
v f g : ι → F
h :
  (fun x ↦ C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x) = fun x ↦
    C ((f + g) x) * Lagrange.basis s v x
⊢ ∑ i ∈ s, C ((f + g) i) * Lagrange.basis s v i =
    ∑ x ∈ s, (C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x)

Tactic:
rw [h]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
i : ι
v r : ι → F
⊢ ∑ i_1 ∈ {i}, C (r i_1) * Lagrange.basis {i} v i_1 = C (r i)

Tactic:
sum_singleton,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
i : ι
v r : ι → F
⊢ C (r i) * Lagrange.basis {i} v i = C (r i)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
i : ι
v r : ι → F
⊢ (interpolate {i} v) r = C (r i)

Tactic:
rw [interpolate_apply, sum_singleton, basis_singleton, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : ¬r i = 0
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)

Tactic:
· rw [degree_C hr, zero_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = (interpolate s v) r
⊢ f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i

Tactic:
rw [h]

Goal state after:
case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = (interpolate s v) r
⊢ ((interpolate s v) r).degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) ((interpolate s v) r) = r i
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
a : R
⊢ (vandermonde fun i ↦ v i + a).det = (vandermonde v).det

Tactic:
by
  simp [Matrix.det_vandermonde]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ ∑ x ∈ s.erase i, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = 0

Tactic:
refine sum_eq_zero fun j hj => ?_

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
j : ι
hj : j ∈ s.erase i
⊢ eval (v i) ((interpolate (insert j (t \ s)) v) r) * eval (v i) (Lagrange.basis s v j) = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate s v) r =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

Tactic:
interpolate_eq_sum_interpolate_insert_sdiff _ hvs ⟨i, mem_insert_self i {j}⟩ _,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ ∑ i_1 ∈ {i, j}, (interpolate (insert i_1 (s \ {i, j})) v) r * Lagrange.basis {i, j} v i_1 =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate (insert i (s \ {i, j})) v) r * Lagrange.basis {i, j} v i +
      ∑ x ∈ {j}, (interpolate (insert x (s \ {i, j})) v) r * Lagrange.basis {i, j} v x =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s

Tactic:
sum_singleton,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate (insert i (s \ {i, j})) v) r * Lagrange.basis {i, j} v i +
      (interpolate (insert j (s \ {i, j})) v) r * Lagrange.basis {i, j} v j =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
⊢ derivative (nodal ∅ v) = ∑ i ∈ ∅, nodal (∅.erase i) v

Tactic:
nodal_empty,

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
⊢ derivative 1 = ∑ i ∈ ∅, nodal (∅.erase i) v
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: case pos
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
j : n
h : i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

pp: case neg
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
j : n
h : ¬i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

Tactic:
· simp only [h, ↓reduceIte, Polynomial.aevalTower_X, IsHomogeneous.sub, isHomogeneous_X]

Goal state after:
case neg
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
j : n
h : ¬i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1
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
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:
rw [h zero_coeff]
    simp only [show n = m ↔ m = n from eq_comm]
    split_ifs with h1
    · rfl
    · simp only [coeff_zero]

Goal state after:
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
⊢ Polynomial.map (↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ))))
      (charpoly.univ A ιM) =
    Polynomial.map (MvPolynomial.map (algebraMap R A))
      (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM))

Tactic:
← charpoly.univ_map_map _ (algebraMap R A)

Goal state after:
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
⊢ Polynomial.map (↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ))))
      (Polynomial.map (MvPolynomial.map (algebraMap R A)) (charpoly.univ R ιM)) =
    Polynomial.map (MvPolynomial.map (algebraMap R A))
      (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM))
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
i j : n
hij : i ≠ j
A : ↥(sl n R) := (single i j hij) 1
B : ↥(sl n R) := (single j i ⋯) 1
c : IsLieAbelian ↥(sl n R)
⊢ False

Tactic:
have c' : A.val * B.val = B.val * A.val := by
    rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]

Goal state after:
n : Type u_1
R : Type u₂
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
i j : n
hij : i ≠ j
A : ↥(sl n R) := (single i j hij) 1
B : ↥(sl n R) := (single j i ⋯) 1
c : IsLieAbelian ↥(sl n R)
c' : ↑A * ↑B = ↑B * ↑A
⊢ False
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: 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
⊢ ∃ s, r ≤ s.card ∧ ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0

Tactic:
classical
    -- Let `t` denote the set of roots of `constantCoeff ψ`.
    let t := (constantCoeff ψ).roots.toFinset
    -- We show that `t` has cardinality at most `finrank K L - r`.
    have ht : t.card ≤ finrank K L - r := by
      refine (Multiset.toFinset_card_le _).trans ?_
      refine (card_roots' _).trans ?_
      rw [constantCoeff_apply]
      -- Indeed, `constantCoeff ψ` has degree at most `finrank K Q = finrank K L - r`.
      apply lieCharpoly_coeff_natDegree
      suffices finrank K Q + r = finrank K L by rw [← this, zero_add, Nat.add_sub_cancel]
      apply Submodule.finrank_quotient_add_finrank
    -- Hence there exists a subset of size `≥ r` in the complement of `t`,
    -- and `constantCoeff ψ` takes non-zero values on all of this subset.
    obtain ⟨s, hs⟩ := exists_finset_le_card K _ hLK
    use s \ t
    refine ⟨?_, ?_⟩
    · refine le_trans ?_ (Finset.le_card_sdiff _ _)
      omega
    · intro α hα
      simp only [Finset.mem_sdiff, Multiset.mem_toFinset, mem_roots', IsRoot.def, not_and, t] at hα
      exact hα.2 hψ

Goal state after:
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
h : LinearIndependent R w'
⊢ ∀ (a : m), (∀ (x : m), w x ≠ 0 → ¬diagonal w x = diagonal w a) → diagonal w a = 0

Tactic:
not_imp_not

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
h : LinearIndependent R w'
⊢ ∀ (a : m), (∀ (x : m), diagonal w x = diagonal w a → w x = 0) → diagonal w a = 0
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: 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
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
this : engel K x ≤ engel K ↑v
z : ↥E
⊢ ∃ n, ((toEnd K ↥U ↥E) (α • u + x') ^ n) z = 0

Tactic:
simpa only [mem_engel_iff, Subtype.ext_iff, coe_toEnd_pow _ _ _ E] using! this z.2

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ ⁅x, ⁅y, a z⁆⁆ - ⁅x, ⁅z, a y⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆ - ⁅y, ⁅z, a x⁆⁆ - ⁅y, a ⁅x, z⁆⁆) +
            (⁅⁅z, x⁆, a y⁆ + ⁅x, ⁅z, a y⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - ⁅z, a ⁅x, y⁆⁆) -
          (⁅x, ⁅y, a z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆) - ⁅z, a ⁅x, y⁆⁆ - a (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)) +
        (⁅x, ⁅z, a y⁆⁆ - (⁅⁅z, x⁆, a y⁆ + ⁅x, ⁅z, a y⁆⁆) - ⁅y, a ⁅x, z⁆⁆ - a (⁅x, ⁅z, y⁆⁆ - ⁅z, ⁅x, y⁆⁆)) -
      (⁅y, ⁅z, a x⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - a (⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆)) =
    0

Tactic:
leibniz_lie z y

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ ⁅x, ⁅y, a z⁆⁆ - ⁅x, ⁅z, a y⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆ - ⁅y, ⁅z, a x⁆⁆ - ⁅y, a ⁅x, z⁆⁆) +
            (⁅⁅z, x⁆, a y⁆ + ⁅x, ⁅z, a y⁆⁆ - (⁅⁅z, y⁆, a x⁆ + ⁅y, ⁅z, a x⁆⁆) - ⁅z, a ⁅x, y⁆⁆) -
          (⁅x, ⁅y, a z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆) - ⁅z, a ⁅x, y⁆⁆ - a (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)) +
        (⁅x, ⁅z, a y⁆⁆ - (⁅⁅z, x⁆, a y⁆ + ⁅x, ⁅z, a y⁆⁆) - ⁅y, a ⁅x, z⁆⁆ - a (⁅x, ⁅z, y⁆⁆ - ⁅z, ⁅x, y⁆⁆)) -
      (⁅y, ⁅z, a x⁆⁆ - (⁅⁅z, y⁆, a x⁆ + ⁅y, ⁅z, a x⁆⁆) - ⁅x, a ⁅y, z⁆⁆ - a (⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆)) =
    0