mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
I : Ideal R
⊢ Submodule.localized' S p (Algebra.linearMap R S) I = span (⇑(algebraMap R S) '' ↑I)

Tactic:
span,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
I : Ideal R
⊢ Submodule.localized' S p (Algebra.linearMap R S) I = Submodule.span S (⇑(algebraMap R S) '' ↑I)
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case e'_2.a
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ A (g x✝) x✝ = ((X • A.map ⇑C + B.map ⇑C) (g x✝) x✝).coeff 1

Tactic:
simp [coeff_C]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)
⊢ motive p

Tactic:
refine p.induction_on (fun a => ?_) (fun {p q} => add p q) ?_ ?_ <;>
      try exact fun n f _ => C_mul_T _ f
  convert! C_mul_T 0 a
  exact (mul_one _).symm

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
⊢ Q f

Tactic:
induction f using LaurentPolynomial.induction_on_mul_T with | _ f n
   =>  _ 

Goal state after:
case mul_T
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
⊢ Q (toLaurent f * T (-↑n))
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Subsingleton n
A : Matrix n n α
b : n → α
i : n
⊢ (A.updateCol i b).det = b i

Tactic:
det_eq_elem_of_subsingleton _ i,

Goal state after:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Subsingleton n
A : Matrix n n α
b : n → α
i : n
⊢ A.updateCol i b i i = b i
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup N
inst✝¹⁵ : Module R M
inst✝¹⁴ : Module R N
inst✝¹³ : Algebra R S
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
p : Submonoid R
inst✝¹⁰ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁹ : IsLocalizedModule p f
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
hpT : Algebra.algebraMapSubmonoid T p ≤ T⁰
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
| Cardinal.lift.{max uP (max uN uS) uT, uM} (Module.rank R M)

Tactic:
← lift_lift.{uN, max uS uT uP},

Goal state after:
R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup N
inst✝¹⁵ : Module R M
inst✝¹⁴ : Module R N
inst✝¹³ : Algebra R S
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
p : Submonoid R
inst✝¹⁰ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁹ : IsLocalizedModule p f
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
hpT : Algebra.algebraMapSubmonoid T p ≤ T⁰
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
| Cardinal.lift.{max uS uT uP, max uN uM} (Cardinal.lift.{uN, uM} (Module.rank R M))
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n
h : a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) (inl b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) (inl b)

Tactic:
simp [TransvectionStruct.sumInl, transvection, h, single]

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

Goal state before:
pp: case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n
h : ¬a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) (inl b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) (inl b)

Tactic:
simp [TransvectionStruct.sumInl, transvection, h, single]

Goal state after:
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✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * B * ⅟B = A

Tactic:
rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
⊢ n < (listTransvecCol M).length

Tactic:
simpa [listTransvecCol] using hn

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
⊢ n < (listTransvecCol M).length

Tactic:
simpa [listTransvecCol] using hn

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

Goal state before:
pp: case «0».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A 0 2 * A 2 1 - A 0 1 * A 2 2 = -(A 0 1 * A 2 2) + A 0 2 * A 2 1

Tactic:
ring

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

Goal state before:
pp: case «1».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A 1 2 * A 2 0 - A 1 0 * A 2 2 = -(A 1 0 * A 2 2) + A 1 2 * A 2 0

Tactic:
ring

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

Goal state before:
pp: case «1».«2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 3 * (A 0 0 * A 1 2 - A 0 2 * A 1 0) = -(A 0 0 * A 1 2) + A 0 2 * A 1 0

Tactic:
ring

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

Goal state before:
pp: case «2».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 3 * (A 0 0 * A 2 1 - A 0 1 * A 2 0) = -(A 0 0 * A 2 1) + A 0 1 * A 2 0

Tactic:
ring

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

Goal state before:
pp: case «2».«2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 4 * (A 0 0 * A 1 1 - A 0 1 * A 1 0) = A 0 0 * A 1 1 - A 0 1 * A 1 0

Tactic:
ring

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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
⊢ ∀ (M N : Matrix n n α), f' (g M * g N) = M * N

Tactic:
intro M N

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
M N : Matrix n n α
⊢ f' (g M * g N) = M * N
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
⊢ (M * (List.take (n + 1) (listTransvecRow M)).prod) (inr ()) (inl i) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
have hnr : n < r := hk

Goal state after:
case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
⊢ (M * (List.take (n + 1) (listTransvecRow M)).prod) (inr ()) (inl i) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
s : Finset α
ih :
  ∀ s_1 ∈ s,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
      M.BlockTriangular b → image b univ = s.erase s_1 → M.det = ∏ a ∈ s.erase s_1, (M.toSquareBlock b a).det
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
hs : image b univ = s
⊢ M.det = ∏ a ∈ s, (M.toSquareBlock b a).det

Tactic:
subst hs

Goal state after:
case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A * B)⁻¹ = B⁻¹ * A⁻¹

Tactic:
simp only [inv_def]
  rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
    Ring.mul_inverse_rev]

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i
h_monic : ∀ (i : Fin n), (p i).Monic
⊢ (of fun i j ↦ (p j).coeff ↑i).det = 1

Tactic:
by
  rw [Matrix.det_of_isUpperTriangular (Matrix.matrixOfPolynomials_blockTriangular p (fun i ↦
      Nat.le_of_eq (h_deg i)))]
  convert! prod_const_one with x _
  rw [Matrix.of_apply, ← h_deg, coeff_natDegree, (h_monic x).leadingCoeff]

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

Goal state before:
pp: case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
hs : image b univ = s
⊢ M⁻¹.BlockTriangular b

Tactic:
subst hs

Goal state after:
case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
⊢ M⁻¹.BlockTriangular b
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁
L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)
D₀ : Fin r → 𝕜
h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀
c : 𝕜 := M' (inr ()) (inr ())
this :
  (List.map (toMatrix ∘ sumInl Unit) L₀).prod * M' * (List.map (toMatrix ∘ sumInl Unit) L₀').prod =
    diagonal (Sum.elim D₀ fun x ↦ c)
⊢ (List.map toMatrix (List.map (sumInl Unit) L₀ ++ L₁)).prod * M *
      (List.map toMatrix (L₁' ++ List.map (sumInl Unit) L₀')).prod =
    diagonal (Sum.elim D₀ fun x ↦ M' (inr ()) (inr ()))

Tactic:
by
    simpa [M', c, Matrix.mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
d : n → R
⊢ (diagonal d).charmatrix = diagonal fun i ↦ X - C (d i)

Tactic:
rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, diagonal_map (map_zero _), diagonal_sub]

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

Goal state before:
pp: n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ : (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L₀').prod = diagonal D₀
this : M = (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M)
⊢ (List.map (toMatrix ∘ reindexEquiv e.symm) L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M) *
      (List.map (toMatrix ∘ reindexEquiv e.symm) L₀').prod =
    diagonal (D₀ ∘ ⇑e)

Tactic:
toMatrix_reindexEquiv_prod,

Goal state after:
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ : (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L₀').prod = diagonal D₀
this : M = (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M)
⊢ (reindexAlgEquiv 𝕜 𝕜 e.symm) (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M) *
      (reindexAlgEquiv 𝕜 𝕜 e.symm) (List.map toMatrix L₀').prod =
    diagonal (D₀ ∘ ⇑e)
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
⊢ eval ((scalar n) r) (matPolyEquiv M) = M.map (eval r)

Tactic:
simpa only [AlgEquiv.symm_apply_apply] using (matPolyEquiv_symm_map_eval (matPolyEquiv M) r).symm

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
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
⊢ (-1) ^ Fintype.card m * ((diagonal fun x ↦ X) - A.map ⇑C * B.map ⇑C).det * (-X) ^ Fintype.card n =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((diagonal fun x ↦ X) - A.map ⇑C * B.map ⇑C).det)

Tactic:
ring

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
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
hdet_MN :
  (M * N).det = (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)
⊢ (-X) ^ Fintype.card m * ((-1) ^ Fintype.card n * ((diagonal fun x ↦ X) - B.map ⇑C * A.map ⇑C).det) =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card m * ((diagonal fun x ↦ X) - B.map ⇑C * A.map ⇑C).det)

Tactic:
ring

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
μ : R
σ : Equiv.Perm n
a✝¹ : σ ∈ univ
i : n
a✝ : i ∈ univ
hi : σ i = i
⊢ X - (C (M i i) - C μ) = X + C μ - C (M i i)

Tactic:
ring

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1)

Tactic:
ring

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

Goal state before:
pp: case a
R : Type u
S : Type v
T : Type w
ι : Type x
k✝ : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
⊢ x ^ (k + 2) - y ^ (k + 2) + x * (z * (x - y)) - ((z * x + y ^ (k + 1)) * (x - y) + x * (x ^ (k + 1) - y ^ (k + 1))) =
    0

Tactic:
ring

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

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : MulActionWithZero R S
inst✝¹ : SMulCommClass R S S
inst✝ : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
⊢ t ^ k • 0 = 0

Tactic:
smul_zero

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : MulActionWithZero R S
inst✝¹ : SMulCommClass R S S
inst✝ : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = ((X ^ k).coeff m - if m = 0 then M ^ k else 0) i j

Tactic:
coeff_X_pow

Goal state after:
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) i j
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
hy : y ^ 2 = 0
c : R
h : c * y ^ 2 + eval x (derivative p) * y + eval x p = eval (x + y) p
⊢ c * 0 + eval x (derivative p) * y + eval x p = eval x p + eval x (derivative p) * y

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
x✝ : p.natDegree < a ∨ a ≤ p.natDegree
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))

Tactic:
cases lt_or_ge (natDegree p) a with

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

Goal state before:
pp: case C
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
a : R
⊢ (a • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R S) a

Tactic:
smul_tmul,

Goal state after:
case C
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
a : R
⊢ 1 ⊗ₜ[R] (a • 1) = 1 ⊗ₜ[R] (algebraMap R S) a
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
⊢ (f.comp g).Splits

Tactic:
by
  rcases lt_or_eq_of_le hg with hg | hg
  · rw [eq_C_of_natDegree_eq_zero (Nat.lt_one_iff.mp hg)]
    simp
  obtain ⟨m, hm⟩ := splits_iff_exists_multiset'.mp hf
  rw [hm, mul_comp, C_comp, multiset_prod_comp]
  refine (Splits.C _).mul (multisetProd ?_)
  simp only [Multiset.mem_map]
  rintro - ⟨-, ⟨a, -, rfl⟩, rfl⟩
  apply of_natDegree_le_one_of_invertible (by simpa)
  rw [leadingCoeff, hg] at h
  simpa [leadingCoeff, hg]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : R →+* S
hi✝ : Function.Injective ⇑i
hf : (map i f).Splits
hi : ∀ a ∈ (map i f).roots, a ∈ i.range
⊢ f.Splits

Tactic:
by
  choose j hj using hi
  rw [splits_iff_exists_multiset]
  refine ⟨(f.map i).roots.pmap j fun _ ↦ id, map_injective i hi ?_⟩
  conv_lhs => rw [hf.eq_prod_roots, leadingCoeff_map_of_injective hi]
  simp [Multiset.pmap_eq_map, hj, Multiset.map_pmap, Polynomial.map_multiset_prod]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ Algebra.adjoin R (⇑g '' f.rootSet A) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤

Tactic:
Algebra.adjoin_image,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ Subalgebra.map g (Algebra.adjoin R (f.rootSet A)) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
by_cases h₁ : n ∈ p.support

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∉ p.support
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
F : Subfield R
f : (↥F)[X]
hf : f.Splits
hf0 : f ≠ 0
x : R
hx : (map F.subtype f).IsRoot x
⊢ x ∈ F

Tactic:
by
  simpa using hf.mem_range_of_isRoot hf0 hx

Goal state after: