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

Goal state before:
pp: case weightMap
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h : ↑P.flip.toPerfPair ∘ₗ f.coweightMap = ↑P.flip.toPerfPair ∘ₗ g.coweightMap
⊢ f.weightMap x = g.weightMap x

Tactic:
← f.weight_coweight_transpose,

Goal state after:
case weightMap
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h : f.weightMap.dualMap ∘ₗ ↑P.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ g.coweightMap
⊢ f.weightMap x = g.weightMap x
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case mp
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
inst✝ : Fintype G
x : k[G]
⊢ (((lsmul k k[G]).flip ((leftRegular k G).norm (MonoidAlgebra.single 1 1)) ∘ₗ
            (linearCombination k fun x ↦ 1) ∘ₗ ↑(coeffLinearEquiv k))
          x).coeff =
      coeff 0 →
    (linearCombination k fun x ↦ 1) x.coeff = 0

Tactic:
Finsupp.ext_iff

Goal state after:
case mp
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
inst✝ : Fintype G
x : k[G]
⊢ (∀ (a : G),
      (((lsmul k k[G]).flip ((leftRegular k G).norm (MonoidAlgebra.single 1 1)) ∘ₗ
                (linearCombination k fun x ↦ 1) ∘ₗ ↑(coeffLinearEquiv k))
              x).coeff
          a =
        (coeff 0) a) →
    (linearCombination k fun x ↦ 1) x.coeff = 0
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : k[G]
hx : (((leftRegular k G) g) x).coeff = x.coeff
γ : G
⊢ x.coeff γ = x.coeff g

Tactic:
Finsupp.ext_iff

Goal state after:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : k[G]
hx : ∀ (a : G), (((leftRegular k G) g) x).coeff a = x.coeff a
γ : G
⊢ x.coeff γ = x.coeff g
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: x✝ : Set ℤ
hn : x✝.Nonempty
hb : BddAbove x✝
⊢ IsLUB x✝ (if h : x✝.Nonempty ∧ BddAbove x✝ then ↑((Classical.choose ⋯).greatestOfBdd ⋯ ⋯) else 0)

Tactic:
rw [dif_pos ⟨hn, hb⟩]

Goal state after:
x✝ : Set ℤ
hn : x✝.Nonempty
hb : BddAbove x✝
⊢ IsLUB x✝ ↑((Classical.choose ⋯).greatestOfBdd ⋯ ⋯)
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: x✝ : Set ℤ
hn : x✝.Nonempty
hb : BddBelow x✝
⊢ IsGLB x✝ (if h : x✝.Nonempty ∧ BddBelow x✝ then ↑((Classical.choose ⋯).leastOfBdd ⋯ ⋯) else 0)

Tactic:
rw [dif_pos ⟨hn, hb⟩]

Goal state after:
x✝ : Set ℤ
hn : x✝.Nonempty
hb : BddBelow x✝
⊢ IsGLB x✝ ↑((Classical.choose ⋯).leastOfBdd ⋯ ⋯)
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i : ι
f : ι → ℕ
hf : Function.support f ⊆ ↑b.support
hf' : P.root i = ∑ j ∈ b.support, f j • P.root j
⊢ ∃ f, Function.support f ⊆ ↑b.support ∧ (0 < f ∨ f < 0) ∧ P.root i = ∑ j ∈ b.support, f j • P.root j

Tactic:
refine ⟨Nat.cast ∘ f, by simpa, Or.inl <| Pi.lt_def.mpr ⟨fun _ ↦ by simp, ?_⟩, by simp [hf']⟩

Goal state after:
case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i : ι
f : ι → ℕ
hf : Function.support f ⊆ ↑b.support
hf' : P.root i = ∑ j ∈ b.support, f j • P.root j
⊢ ∃ i, 0 i < (Nat.cast ∘ f) i
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✝ : P.IsCrystallographic
i : ι
hi : b.IsPos (-i)
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0

Tactic:
· obtain ⟨j, hj, hj₀⟩ := hi.exists_mem_support_pos_pairingIn
    exact ⟨j, hj, by aesop⟩

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

Goal state before:
pp: x a b : ℝ
⊢ (a + b).cauchy = (b + a).cauchy

Tactic:
simp only [cauchy_add, add_comm]

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 : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |min (↑a j) (↑b j) - ↑b j| < ε✝

Tactic:
rw [← min_sub_sub_right]

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✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |min (↑a j - ↑b j) (↑b j - ↑b j)| < ε✝
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : A.IsHermitian
f : α → β
hf : Function.Semiconj f star star
⊢ (A.map f).IsHermitian

Tactic:
by
  rw [IsHermitian, ← conjTranspose_map f hf, h.eq]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝² : NonUnitalSemiring α
inst✝¹ : StarRing α
inst✝ : Fintype n
A : Matrix m n α
⊢ (A * Aᴴ).IsHermitian

Tactic:
by rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]

Goal state after:
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
A : M
n : ℕ
⊢ A⁻¹ ^ ↑n = (A ^ ↑n)⁻¹

Tactic:
rw [zpow_natCast, zpow_natCast, inv_pow']

Goal state after:
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
A : M
h : IsUnit A.det
n : ℤ
⊢ IsUnit (A ^ n).det

Tactic:
by
  rcases n with n | n
  · simpa using h.pow n
  · simpa using h.pow n.succ

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

Goal state before:
pp: case pred
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ (-↑z)).det ↔ IsUnit A.det ∨ -↑z = 0
⊢ IsUnit (A ^ (-↑z - 1)).det ↔ IsUnit A.det ∨ -↑z - 1 = 0

Tactic:
rw [← neg_add', ← Int.natCast_succ, zpow_neg_natCast, isUnit_nonsing_inv_det_iff, det_pow,
      isUnit_pow_succ_iff, neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj]
    simp

Goal state after:
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
A : M
n : ℕ
x✝ : ↑n ≠ -1
⊢ A ^ (↑n + 1) = A ^ ↑n * A

Tactic:
simp only [pow_succ, ← Nat.cast_succ, zpow_natCast]

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

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

Tactic:
· rw [nonsing_inv_apply_not_isUnit _ h]
    exact .zero

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
h₃ : (ρ - μ) * |v i| ≤ (N *ᵥ |v|) i
⊢ (N *ᵥ |v|) i * (diagonal d *ᵥ |v|) i = (|v| ᵥ* diagonal d) i * (N *ᵥ |v|) i

Tactic:
simp [mulVec_eq_sum, vecMul_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
⊢ ∃ v, ((aeval f) q) v ≠ 0

Tactic:
by
    by_contra! h_contra
    have := minpoly.min R f
      ((monic_X_sub_C μ).of_mul_monic_left (hq ▸ minpoly.monic (Algebra.IsIntegral.isIntegral f)))
      (LinearMap.ext h_contra)
    rw [hq, degree_mul, degree_X_sub_C, degree_eq_natDegree] at this
    · norm_cast at this; grind
    · rintro rfl
      exact minpoly.ne_zero (Algebra.IsIntegral.isIntegral f) (mul_zero (X - C μ) ▸ hq)

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
⊢ eval (-↑k) (ascPochhammer R (n + 1)) = 0

Tactic:
rw [ascPochhammer_succ_eval]
    rcases lt_trichotomy k n with hkn | rfl | hkn
    · simp [ih hkn]
    · simp
    · lia

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n k : ℕ
h : k < n
⊢ eval (-↑k) (ascPochhammer R n) = 0

Tactic:
induction n with
  | zero => contradiction
  | succ n ih =>
    rw [ascPochhammer_succ_eval]
    rcases lt_trichotomy k n with hkn | rfl | hkn
    · simp [ih hkn]
    · simp
    · lia

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
this : ∀ (y : L₂), (∃ l, (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) l = (0, y)) → y = 0
⊢ InjOn ⇑(LinearMap.fst R L₁ L₂) ↑(span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})

Tactic:
have aux : {(b₁.h i, b₂.h (eι i)) | i : ι₁} = (fun i : ι₁ ↦ (b₁.h i, b₂.h (eι i))) '' univ := by
      ext; simp

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
this : ∀ (y : L₂), (∃ l, (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) l = (0, y)) → y = 0
aux : {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} = (fun i ↦ (b₁.h i, b₂.h (eι i))) '' univ
⊢ InjOn ⇑(LinearMap.fst R L₁ L₂) ↑(span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
i j : Fin n
⊢ ((vandermonde v)ᵀ * vandermonde v) i j = ∑ k, v k ^ (↑i + ↑j)

Tactic:
by
  simp only [vandermonde_apply, Matrix.mul_apply, Matrix.transpose_apply, pow_add]

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 ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ((interpolate (s.erase i) v) r).degree < ↑(#s - 1)

Tactic:
rw [← Finset.card_erase_of_mem 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
⊢ ((interpolate (s.erase i) v) r).degree < ↑(#(s.erase i))
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
m n : ℕ
hmn : m ≤ n
y : ↥H
hy : y ∈ (fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n)) m
⊢ y ∈ (fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n)) n

Tactic:
LinearMap.mem_ker

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
m n : ℕ
hmn : m ≤ n
y : ↥H
hy : ((ad R ↥H) x ^ m) y = 0
⊢ ((ad R ↥H) x ^ n) y = 0
Module: Mathlib.LinearAlgebra.Charpoly.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
h : (minpoly R f).coeff 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < (minpoly R f).degree
hPmonic : P.Monic
hzero : ∀ (x : M), ((aeval f) P) x = 0
⊢ False

Tactic:
exact not_le.2 hdegP (minpoly.min _ _ hPmonic (LinearMap.ext hzero))

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case refine_1
ι : 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 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
z : { x // x ∈ s✝ }
hz1 : z ∈ s.support
⊢ IsHomogeneousElem 𝒜 ↑z

pp: case refine_2
ι : 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 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
z : { x // x ∈ s✝ }
hz1 : z ∈ s.support
⊢ ↑z ∈ span s✝

Tactic:
· rcases z with ⟨z, hz2⟩
    apply h _ hz2

Goal state after:
case refine_2
ι : 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 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
z : { x // x ∈ s✝ }
hz1 : z ∈ s.support
⊢ ↑z ∈ span s✝
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
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
a✝ : R
x : MvPolynomial σ R
x✝ : x ∈ {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}
w✝ : IsWeightedHomogeneous w x m
hx : ∀ (a : R), motive (C a * x) ⋯
a : R
⊢ motive (C a * a✝ • x) ⋯

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
a✝ : R
x : MvPolynomial σ R
x✝ : x ∈ {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}
w✝ : IsWeightedHomogeneous w x m
hx : ∀ (a : R), motive (C a * x) ⋯
a : R
⊢ motive (C a * ((algebraMap R (MvPolynomial σ R)) a✝ * x)) ⋯
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
p : MvPolynomial σ R
⊢ weightedTotalDegree (Pi.single i 1) p = degreeOf i p

Tactic:
by
  simp only [weightedTotalDegree, weight, linearCombination, Pi.single_apply, degreeOf, degrees,
    Multiset.count_finset_sup]
  congr; ext d
  simp +contextual

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ IsGreatest {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)

Tactic:
have coe_mono : Monotone (toIdeal : HomogeneousIdeal 𝒜 → Ideal A) := fun x y => id

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
⊢ IsGreatest {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case convert_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
⊢ n ≠ m → (weightedHomogeneousComponent w m) ↑(x n) = 0

Tactic:
hmn

Goal state after:
case convert_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ (weightedHomogeneousComponent w m) ↑(x n) = 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: M : Type u_2
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
⊢ (weight w) m = 0 ↔ ∀ (x : σ), m x = 0

Tactic:
simp only [weight, Finsupp.linearCombination, LinearMap.toAddMonoidHom_coe, coe_lsum,
    LinearMap.coe_smulRight, LinearMap.id_coe, id_eq]
  rw [Finsupp.sum, Finset.sum_eq_zero_iff]
  apply forall_congr'
  intro x
  rw [Finsupp.mem_support_iff]
  constructor
  · intro hx
    by_contra hx'
    exact absurd (hw _ _ (hx hx')) hx'
  · order

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
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✝ : Nontrivial R
⊢ (φ.polyCharpoly b).natDegree = finrank R M

Tactic:
by
  rw [polyCharpoly, polyCharpolyAux, (charpoly.univ_monic _ _).natDegree_map,
    charpoly.univ_natDegree, finrank_eq_card_chooseBasisIndex]

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
⊢ (J l R).det * (J l R).det = 1

Tactic:
by
  rw [← det_mul, J_squared, ← one_smul R (-1 : Matrix _ _ R), smul_neg, ← neg_smul, det_smul,
    Fintype.card_sum, det_one, mul_one]
  apply Even.neg_one_pow
  exact Even.add_self _

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

Goal state before:
pp: l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ PB l R * fromBlocks 1 0 0 ⅟(PD l R) = 1

Tactic:
by
  rw [PB, Matrix.fromBlocks_multiply, mul_invOf_self]
  simp only [Matrix.mul_zero, Matrix.mul_one, Matrix.zero_mul, zero_add, add_zero,
    Matrix.fromBlocks_one]

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

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype m
A : Matrix m n R
⊢ Module.rank R (m → R) ≤ ↑(Fintype.card m)

Tactic:
rw [rank_fun']

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

Goal state before:
pp: case inl.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
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z = 0
⊢ ⟨x, ⋯⟩ ≠ 0

pp: case inl.refine_2
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
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z = 0
⊢ ((toEnd K ↥U ↥E) (α • u + x')) ⟨x, ⋯⟩ = 0

Tactic:
· exact Subtype.coe_ne_coe.mp hx₀

Goal state after:
case inl.refine_2
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
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z = 0
⊢ ((toEnd K ↥U ↥E) (α • u + x')) ⟨x, ⋯⟩ = 0
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case inr.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
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z ≠ 0
⊢ ⟨↑z, ⋯⟩ ≠ 0

Tactic:
simpa only [coe_bracket_of_module, ne_eq, Submodule.mk_eq_zero, Subtype.ext_iff] using! hz₀

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

Goal state before:
pp: m : Type um
m₀ : Type um₀
n₀ : Type un₀
R : Type uR
n : Type un
inst✝ : Semiring R
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ lift.{um₀, max uR um} A.cRank ≤ lift.{um, max uR um₀} (A.submatrix ⇑em ⇑en).cRank

Tactic:
simpa using ((A.reindex em.symm en.symm).lift_cRank_submatrix_le em.symm en.symm)

Goal state after: