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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ A * ⅟A - A * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A -
      U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A =
    1 + U * C * V * ⅟A - (U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A)

Tactic:
mul_invOf_self,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 - 1 * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A - U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A =
    1 + U * C * V * ⅟A - (U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A)
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) B).det = (((kroneckerMapBilinear f) A) 1 * ((kroneckerMapBilinear f) 1) B).det

Tactic:
by
      rw [← kroneckerMapBilinear_mul_mul f h_comm, Matrix.mul_one, Matrix.one_mul]

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
⊢ ⅟A = A⁻¹

Tactic:
let := detInvertibleOfInvertible A
  rw [inv_def, Ring.inverse_invertible, invOf_eq]

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

Goal state before:
pp: case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
⊢ ∃ B, A * B = 1

Tactic:
refine ⟨(Matrix.of cols)ᵀ, Matrix.ext fun i j ↦ ?_⟩

Goal state after:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
i j : m
⊢ (A * (of cols)ᵀ) i j = 1 i j
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal' d ⟨i', i⟩ ⟨j', j⟩ = 0

Tactic:
blockTriangular_blockDiagonal'

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ 0 = 0

case a
α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ ⟨j', j⟩.fst < ⟨i', i⟩.fst
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible A
⊢ (A * ⅟A).submatrix ⇑e₁ ⇑e₁ = 1

Tactic:
mul_invOf_self,

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible A
⊢ submatrix 1 ⇑e₁ ⇑e₁ = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
this : A = (A.submatrix ⇑e₁ ⇑e₂).submatrix ⇑e₁.symm ⇑e₂.symm
⊢ (A.submatrix ⇑e₁ ⇑e₂ * ⅟(A.submatrix ⇑e₁ ⇑e₂)).submatrix ⇑e₁.symm ⇑e₁.symm = 1

Tactic:
mul_invOf_self,

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
this : A = (A.submatrix ⇑e₁ ⇑e₂).submatrix ⇑e₁.symm ⇑e₂.symm
⊢ submatrix 1 ⇑e₁.symm ⇑e₁.symm = 1
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
⊢ matPolyEquiv (p • 1) = Polynomial.map (algebraMap R (Matrix n n R)) p

Tactic:
by
  ext m i j
  simp only [matPolyEquiv_coeff_apply, Matrix.smul_apply, Matrix.one_apply, smul_eq_mul, mul_ite,
    mul_one, mul_zero, coeff_map, algebraMap_matrix_apply, Algebra.algebraMap_self,
    RingHom.id_apply]
  split_ifs <;> simp

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
      (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₂)
      (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
      (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₂) =
    1
⊢ A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ = 1

Tactic:
replace := congr_arg Matrix.toBlocks₁₁ this

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  (fromBlocks (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
        (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₂)
        (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
        (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₂)).toBlocks₁₁ =
    toBlocks₁₁ 1
⊢ A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ = 1
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ 1 • Matrix.map 1 ⇑(algebraMap R A) = 1

Tactic:
Matrix.map_one (algebraMap R A) (map_zero _) (map_one _),

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ 1 • 1 = 1
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
i : Invertible A × Invertible D
this✝ : Invertible A := i.1
this : Invertible D := i.2
⊢ Invertible (fromBlocks A B 0 D)

Tactic:
exact fromBlocksZero₂₁Invertible A B D

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
⊢ X ^ Fintype.card n * (A * B).charpoly = X ^ Fintype.card m * (B * A).charpoly

Tactic:
by
  -- This proof follows https://math.stackexchange.com/a/311362/315369
  let M := fromBlocks (scalar m X) (A.map C) (B.map C) (1 : Matrix n n R[X])
  let N := fromBlocks (-1 : Matrix m m R[X]) 0 (B.map C) (-scalar n X)
  have hMN :
      M * N = fromBlocks (-scalar m X + (A * B).map C) (-(X : R[X]) • A.map C) 0 (-scalar n X) := by
    simp [M, N, fromBlocks_multiply, smul_eq_mul_diagonal, -diagonal_neg]
  have hNM : N * M = fromBlocks (-scalar m X) (-A.map C) 0 ((B * A).map C - scalar n X) := by
    simp [M, N, fromBlocks_multiply, sub_eq_add_neg, -scalar_apply, scalar_comm, Commute.all]
  have hdet_MN : (M * N).det = (-1 : R[X]) ^ (Fintype.card m + Fintype.card n) *
      (X ^ Fintype.card n * (scalar m X - (A * B).map C).det) := by
    rw [hMN, det_fromBlocks_zero₂₁, neg_add_eq_sub, ← neg_sub, det_neg]
    simp
    ring
  have hdet_NM : (N * M).det = (-1 : R[X]) ^ (Fintype.card m + Fintype.card n) *
      (X ^ Fintype.card m * (scalar n X - (B * A).map C).det) := by
    rw [hNM, det_fromBlocks_zero₂₁, ← neg_sub, det_neg (_ - _)]
    simp
    ring
  dsimp only [charpoly, charmatrix, RingHom.mapMatrix_apply]
  rw [← (isUnit_neg_one.pow _).isRegular.left.eq_iff, ← hdet_NM, ← hdet_MN, det_mul_comm]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (fromBlocks 1 (-A) B 1).det = (1 + B * A).det

Tactic:
by rw [det_fromBlocks_one₁₁, Matrix.mul_neg, sub_neg_eq_add]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : e ^ 0 = 0
⊢ e = 0

Tactic:
rw [pow_zero] at hn; rw [← one_mul e, hn, zero_mul]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
⊢ IsRadical 0 ↔ ∀ (x : R) (x_1 : ℕ), 0 ∣ x ^ x_1 → 0 ∣ x

Tactic:
exact forall_comm

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
⊢ m + n ≤ m + n - 1 + 1

Tactic:
by rw [← Nat.sub_le_iff_le_add]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)

Tactic:
rw [← neg_right_iff] at h_comm

Goal state after:
R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : (PiToModule.fromMatrix R b) A = (PiToModule.fromEnd R b) f
r : R
⊢ (PiToModule.fromMatrix R b) (r • A) = (PiToModule.fromEnd R b) (r • f)

Tactic:
rw [map_smul, map_smul, h]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
hb : IsUnit ((aeval b) P)
hab : IsNilpotent (a - b)
⊢ IsUnit ((aeval a) P)

Tactic:
rw [← add_sub_cancel (aeval b P) (aeval a P)]

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
hb : IsUnit ((aeval b) P)
hab : IsNilpotent (a - b)
⊢ IsUnit ((aeval b) P + ((aeval a) P - (aeval b) P))
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
hm : M.FG
hn : N.FG
⊢ (M * N).FG

Tactic:
rw [mul_eq_map₂]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
hm : M.FG
hn : N.FG
⊢ (Submodule.map₂ (LinearMap.mul R A) M N).FG
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
⊢ I.spanRank = 0 ↔ I = ⊥

Tactic:
by
  constructor
  · intro h
    obtain ⟨s, ⟨hs₁, hs₂⟩⟩ :=
      (FG.spanRank_le_iff_exists_span_set_card_le I (a := 0)).mp (by rw [h])
    simp only [nonpos_iff_eq_zero, mk_eq_zero_iff, Set.isEmpty_coe_sort] at hs₁
    simp_all
  · rintro rfl; rw [spanRank]
    exact Cardinal.iInf_eq_zero_iff.mpr (Or.inr ⟨⟨∅, by simp⟩, by simp⟩)

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
B : Type u_6
C : Type u_7
F : Type u_8
inst✝⁹ : Ring B
inst✝⁸ : Ring C
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : Algebra R C
inst✝⁴ : IsScalarTower R A B
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
b : B
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
hb : IsIntegral R b
⊢ (algebraMap R C).IsIntegralElem (f b)

Tactic:
← ((AlgHomClass.toAlgHom f).restrictScalars R).comp_algebraMap

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
B : Type u_6
C : Type u_7
F : Type u_8
inst✝⁹ : Ring B
inst✝⁸ : Ring C
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : Algebra R C
inst✝⁴ : IsScalarTower R A B
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
b : B
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
hb : IsIntegral R b
⊢ ((↑(AlgHom.restrictScalars R ↑f)).comp (algebraMap R B)).IsIntegralElem (f b)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
a✝ : Nontrivial A
hf : Monic 1
hfx : (aeval x) 1 = 0
⊢ False

Tactic:
simp [one_ne_zero' A] at hfx

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.charpoly.Monic

Tactic:
nontriviality R
  by_cases h : Fintype.card n = 0
  · rw [charpoly, det_eq_one_of_card_eq_zero h]
    apply monic_one
  have mon : (∏ i : n, (X - C (M i i))).Monic := by
    apply monic_prod_of_monic univ fun i : n => X - C (M i i)
    simp [monic_X_sub_C]
  rw [← sub_add_cancel (∏ i : n, (X - C (M i i))) M.charpoly] at mon
  rw [Monic] at *
  rwa [leadingCoeff_add_of_degree_lt] at mon
  rw [charpoly_degree_eq_dim]
  rw [← neg_sub]
  rw [degree_neg]
  apply lt_trans (charpoly_sub_diagonal_degree_lt M)
  rw [Nat.cast_lt]
  lia

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case succ.h₀.succ.h
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
j : Fin (n + 1)
⊢ Fin.castSucc 0 < i

Tactic:
· rw [Fin.castSucc_zero]; exact lt_of_le_of_ne (Fin.zero_le _) hi.symm

Goal state after:
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
k : ℕ
hk : ¬k = n
i : R
hi : f i = p.coeff k
⊢ (erase n p).coeff k ∈ f.rangeS

Tactic:
use i

Goal state after:
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
k : ℕ
hk : ¬k = n
i : R
hi : f i = p.coeff k
⊢ f i = (erase n p).coeff k
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det =
    C A⁻¹.det * ((-1) ^ Fintype.card n * (1 - (scalar n) X * C.mapMatrix A).det)

Tactic:
rw [← neg_sub, det_neg, det_one_sub_mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - X ^ k • 0

Tactic:
smul_zero,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))

Tactic:
simp only [add_tsub_cancel_left]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑l !) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max (if {x ∈ p.support | ↑(x.choose n) * p.coeff x = 0} = ∅ then 0 else max 0 0)
      (Finset.fold max 0 (fun x ↦ x - n) ({i ∈ p.support | ¬↑(i.choose n) * p.coeff i = 0})) ≤
    p.natDegree - n

Tactic:
simp only [ite_self, max_eq_right, zero_le, Finset.fold_max_le, true_and, and_imp,
        tsub_le_iff_right, mem_support_iff, Ne, Finset.mem_filter]
      intro x hx hx'
      have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
      grind

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ map T.subtype (p.toSubring T hp) = p

Tactic:
by
  ext n
  simp [coeff_map]

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ rootMultiplicity (a * r) (q.scaleRoots r) + rootMultiplicity a p = rootMultiplicity a p

Tactic:
dvd_iff_isRoot,

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬q.IsRoot a
hq0 : q ≠ 0
⊢ rootMultiplicity (a * r) (q.scaleRoots r) + rootMultiplicity a p = rootMultiplicity a p
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod

Tactic:
let S : Submonoid R[X] := MonoidHom.mrange C
    have hS : S = {C a | a : R} := MonoidHom.coe_mrange C
    rw [Splits, Submonoid.closure_union, ← hS, Submonoid.closure_eq, Submonoid.mem_sup] at hf
    obtain ⟨-, ⟨a, rfl⟩, g, hg, rfl⟩ := hf
    obtain ⟨mg, hmg, rfl⟩ := Submonoid.exists_multiset_of_mem_closure hg
    choose! j hj using hmg
    have hmg : mg = (mg.map j).map (X + C ·) := by simp [Multiset.map_congr rfl hj]
    rw [hmg, leadingCoeff_mul_monic, leadingCoeff_C]
    · use mg.map j
    · rw [hmg]
      apply monic_multiset_prod_of_monic
      simp [monic_X_add_C]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
a✝ : Nontrivial R
a : R
m : Multiset R
hm : f = C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod)
ha : a ∈ a ::ₘ m
h : (Irreducible (X + C a) ∧ ∀ m_1 ∈ (Multiset.map (fun x ↦ X + C x) m).toList, IsUnit m_1) ∧ IsUnit (C f.leadingCoeff)
⊢ f.natDegree ≤ 1

Tactic:
have : m = 0 := by simpa [not_isUnit_X_add_C, ← Multiset.eq_zero_iff_forall_notMem] using h.1.2

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
a✝ : Nontrivial R
a : R
m : Multiset R
hm : f = C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod)
ha : a ∈ a ::ₘ m
h : (Irreducible (X + C a) ∧ ∀ m_1 ∈ (Multiset.map (fun x ↦ X + C x) m).toList, IsUnit m_1) ∧ IsUnit (C f.leadingCoeff)
this : m = 0
⊢ f.natDegree ≤ 1
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hm : f.Monic
| C 1 * (Multiset.map (fun x ↦ X - C x) f.roots).prod

Tactic:
C_1,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hm : f.Monic
| 1 * (Multiset.map (fun x ↦ X - C x) f.roots).prod
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : (algebraMap R B) r * y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval ((algebraMap R B) r * (x * y)))

Tactic:
Algebra.commutes

Goal state after:
case e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : y * (algebraMap R B) r = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval (x * y * (algebraMap R B) r))
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
n : ℕ
hn : p.natDegree = n
⊢ f.Splits ∧ g.Splits

Tactic:
induction n generalizing p f g with

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ∑ i ∈ Finset.range (g.natDegree + 1),
      ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) (g.coeff i) * (Ideal.Quotient.mk I) X ^ i =
    (Ideal.Quotient.mk I) g

Tactic:
nth_rw 3 [(as_sum_range_C_mul_X_pow g)]

Goal state after:
S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ∑ i ∈ Finset.range (g.natDegree + 1),
      ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) (g.coeff i) * (Ideal.Quotient.mk I) X ^ i =
    (Ideal.Quotient.mk I) (∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i) * X ^ i)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
⊢ f = f.comp (C 1 * (X - C b) + C b)

Tactic:
C_1,

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
⊢ f = f.comp (1 * (X - C b) + C b)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R N
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton M

Tactic:
exact subsingleton_tensorProduct_iff_left R M

Goal state after: