mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℤ
⊢ (eval₂ f x) (T n) = ↑(x ^ n)

Tactic:
by_cases! hn : 0 ≤ n
  · lift n to ℕ using hn
    apply eval₂_T_n
  · obtain ⟨m, rfl⟩ := Int.exists_eq_neg_ofNat hn.le
    rw [eval₂_T_neg_n, zpow_neg, zpow_natCast, ← inv_pow, Units.val_pow_eq_pow_val]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
r : R
n : ℕ
⊢ (eval₂ f x) (C r) * ↑x⁻¹ ^ n = f r * ↑x⁻¹ ^ n

Tactic:
eval₂_C

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
r : R
n : ℕ
⊢ f r * ↑x⁻¹ ^ n = f r * ↑x⁻¹ ^ n
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
r : R
⊢ smeval (AddMonoidAlgebra.single 0 r) x = r • 1

Tactic:
smeval_single x (0 : ℤ) r,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
r : R
⊢ r • ↑(x ^ 0) = r • 1
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ A.adjugate i j =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j

Tactic:
rw [adjugate_fin_succ_eq_det_submatrix, det_fin_two]

Goal state after:
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ (-1) ^ (↑j + ↑i) *
      (A.submatrix j.succAbove i.succAbove 0 0 * A.submatrix j.succAbove i.succAbove 1 1 -
        A.submatrix j.succAbove i.succAbove 0 1 * A.submatrix j.succAbove i.succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case e_f.e_a.e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
x : { a // p a } ⊕ { a // ¬p a }
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ x) x =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (σ x) x

Tactic:
generalize hy : σ x = y

Goal state after:
case e_f.e_a.e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
x y : { a // p a } ⊕ { a // ¬p a }
hy : σ x = y
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M y x =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) y x
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : IsUnit A.det
hB : IsUnit B.det
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) (A * A⁻¹) (B * B⁻¹) = 1

Tactic:
← one_kronecker_one,

Goal state after:
case pos
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : IsUnit A.det
hB : IsUnit B.det
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) (A * A⁻¹) (B * B⁻¹) = kroneckerMap (fun x1 x2 ↦ x1 * x2) 1 1
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
M : Matrix n n R
⊢ (aeval M) M.charpoly = 0

Tactic:
have h : M.charpoly • (1 : Matrix n n R[X]) = adjugate (charmatrix M) * charmatrix M :=
    (adjugate_mul _).symm
  -- Using the algebra isomorphism `Matrix n n R[X] ≃ₐ[R] Polynomial (Matrix n n R)`,
  -- we have the same identity in `Polynomial (Matrix n n R)`.
  apply_fun matPolyEquiv at h
  simp only [map_mul, matPolyEquiv_charmatrix] at h
  -- Because the coefficient ring `Matrix n n R` is non-commutative,
  -- evaluation at `M` is not multiplicative.
  -- However, any polynomial which is a product of the form $N * (t I - M)$
  -- is sent to zero, because the evaluation function puts the polynomial variable
  -- to the right of any coefficients, so everything telescopes.
  apply_fun fun p => p.eval M at h
  rw [eval_mul_X_sub_C] at h
  -- Now $χ_M (t) I$, when thought of as a polynomial of matrices
  -- and evaluated at some `N` is exactly $χ_M (N)$.
  rw [matPolyEquiv_smul_one, eval_map] at h
  -- Thus we have $χ_M(M) = 0$, which is the desired result.
  exact h

Goal state after:
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
⊢ ∀ (a₁ a₂ : A) (b₁ b₂ : Matrix n n R),
    (toFunLinear n R A) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      (toFunLinear n R A) (a₁ ⊗ₜ[R] b₁) * (toFunLinear n R A) (a₂ ⊗ₜ[R] b₂)

Tactic:
intros
      simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply, Matrix.map_mul]
      ext
      dsimp
      simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum,
        _root_.mul_assoc, Algebra.left_comm]

Goal state after:
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
p : a = b
H : a' + b = b' + a
⊢ a' = b'

Tactic:
p

Goal state after:
α : Type u_1
a a' b b' : α
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
p : a = b
H : a' + b = b' + b
⊢ a' = b'
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b ≤ b' + a
⊢ b' + a ≤ b' + b

Tactic:
p

Goal state after:
α : Type u_1
a a' b b' : α
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b ≤ b' + a
⊢ b' + b ≤ b' + b
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b < b' + a
⊢ a' < b'

Tactic:
p

Goal state after:
α : Type u_1
a a' b b' : α
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b < b' + b
⊢ a' < b'
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n = a - b
⊢ (a' - b') ^ n = 0

Tactic:
p

Goal state after:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n = 0
⊢ (a' - b') ^ n = 0
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case convert_1
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 α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
this : Invertible 1 := invertibleOne
⊢ Invertible (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)

Tactic:
letI : Invertible (1 : Matrix m m α) := invertibleOne

Goal state after:
case convert_1
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 α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
this✝ : Invertible 1 := invertibleOne
this : Invertible 1 := invertibleOne
⊢ Invertible (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case convert_1
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 α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ Invertible (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)

pp: case convert_6
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 α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ Invertible D

pp: case convert_7
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 α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D) =
    ⅟(fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)

Tactic:
· -- the product is invertible because all the factors are
    letI : Invertible (1 : Matrix n n α) := invertibleOne
    letI : Invertible (1 : Matrix m m α) := invertibleOne
    refine Invertible.mul ?_ (fromBlocksZero₁₂Invertible _ _ _)
    exact
      Invertible.mul (fromBlocksZero₂₁Invertible _ _ _)
        (fromBlocksZero₂₁Invertible _ _ _)

Goal state after:
case convert_7
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 α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D) =
    ⅟(fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 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 α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
this : Invertible 1 := invertibleOne
⊢ Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)

Tactic:
letI : Invertible (1 : Matrix m m α) := invertibleOne

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 α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
this✝ : Invertible 1 := invertibleOne
this : Invertible 1 := invertibleOne
⊢ Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f =
    ((f.sum fun e a ↦ a * x ^ e) + f.sum fun e a ↦ a * ↑e * x ^ (e - 1) * y) +
      f.sum fun e a ↦ a * ↑(polyBinomAux1 x y e a) * y ^ 2

Tactic:
by
  rw [poly_binom_aux2]
  simp [left_distrib, sum_add, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ w ^ 2
⊢ x * z ∣ (w * z) ^ 2

Tactic:
mul_pow

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ w ^ 2
⊢ x * z ∣ w ^ 2 * z ^ 2
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (P * X) ↔ IsNilpotent P

Tactic:
← commute_X P

Goal state after:
R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)

Tactic:
intro n

Goal state after:
case right
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
⊢ n ≠ 0 → IsNilpotent (P.coeff n)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Ring T
f : R →+* S
x : S
g : S →+* T
p : R[X]
hp : p.Monic
hx : eval₂ f x p = 0
⊢ g (eval₂ f x p) = 0

Tactic:
eval₂_eq_eval_map

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Ring T
f : R →+* S
x : S
g : S →+* T
p : R[X]
hp : p.Monic
hx : eval x (Polynomial.map f p) = 0
⊢ g (eval x (Polynomial.map f p)) = 0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : Fintype.card n = 0
⊢ M.charmatrix.det.Monic

Tactic:
det_eq_one_of_card_eq_zero h

Goal state after:
case pos
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : Fintype.card n = 0
⊢ Monic 1
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ (∏ i, (X - C (M i i)) - M.charpoly).degree < M.charpoly.degree

Tactic:
charpoly_degree_eq_dim

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ (∏ i, (X - C (M i i)) - M.charpoly).degree < ↑(Fintype.card n)
Module: Mathlib.Algebra.Polynomial.Eval.Subring

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ (mapRingHom f).rangeS ↔ ∀ (n : ℕ), p.coeff n ∈ f.rangeS

Tactic:
constructor
  · rintro ⟨p, rfl⟩ n
    rw [coe_mapRingHom, coeff_map]
    exact Set.mem_range_self _
  · intro h
    rw [p.as_sum_range_C_mul_X_pow]
    refine (mapRingHom f).rangeS.sum_mem ?_
    intro i _hi
    rcases h i with ⟨c, hc⟩
    use C c * X ^ i
    rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]

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

Goal state before:
pp: case empty
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
his : ∀ x ∈ ∅, IsIntegral R x
x : A
⊢ x ∈ span R ↑{1} ↔ x ∈ Subalgebra.toSubmodule R[]

Tactic:
rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]

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
⊢ (1 + X • M.map ⇑C).det = 1 + C M.trace * X + (1 + X • M.map ⇑C).det.divX.divX * X ^ 2

Tactic:
pow_two,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 + X • M.map ⇑C).det = 1 + C M.trace * X + (1 + X • M.map ⇑C).det.divX.divX * (X * X)
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
⊢ (1 + X • M.map ⇑C).det = 1 + (1 + X • M.map ⇑C).det.divX * X

Tactic:
add_comm (1 : R[X]),

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 + X • M.map ⇑C).det = (1 + X • M.map ⇑C).det.divX * X + 1
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
⊢ (mapRingHom f) X = X

Tactic:
by
    simp only [coe_mapRingHom, map_X]

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
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
⊢ t_inv * t = 1

Tactic:
rw [← T_add, neg_add_cancel, T_zero]

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 : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
⊢ (D fun i ↦ (X • M.map ⇑C) i + 1 i).coeff k =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)

Tactic:
conv_lhs => rw [show (fun i ↦ ((X : R[X]) • M.map C) i + (1 : Matrix n n R[X]) i) =
      (fun i => ((X : R[X]) • M.map C) i) + (fun i => (1 : Matrix n n R[X]) i) from rfl]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
⊢ (D ((fun i ↦ (X • M.map ⇑C) i) + fun i ↦ 1 i)).coeff k =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
a✝ : Nontrivial R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → ((taylor r) ((monomial n) c)).natDegree = n

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
a✝ : Nontrivial R
n : ℕ
⊢ ∀ (c : R), c ≠ 0 → ((taylor r) ((monomial n) c)).natDegree = n
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (hasseDeriv f.natDegree) f = C f.leadingCoeff

Tactic:
have : _ ≤ 0 := Nat.sub_self f.natDegree ▸ natDegree_hasseDeriv_le ..
  rw [eq_C_of_natDegree_le_zero this, hasseDeriv_coeff, zero_add, Nat.choose_self,
    Nat.cast_one, one_mul, leadingCoeff]

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
⊢ ∀ x_1 ∈ Finset.range (p.natDegree + 1),
    f (p.integralNormalization.coeff x_1) * (f p.leadingCoeff * x) ^ x_1 =
      f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff x_1) * x ^ x_1)

Tactic:
intro n

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
n : ℕ
⊢ n ∈ Finset.range (p.natDegree + 1) →
    f (p.integralNormalization.coeff n) * (f p.leadingCoeff * x) ^ n =
      f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff n) * x ^ n)
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z (C (p.coeff 0)) = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

Tactic:
eval₂_C

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : f (p.coeff 0) = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Subsingleton R
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

pp: case inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
· simp [Subsingleton.elim p 0]

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hf : f.Splits
x : R
⊢ eval x (derivative (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod)) =
    f.leadingCoeff * (Multiset.map (fun a ↦ (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase a)).prod) f.roots).sum

Tactic:
simp [derivative_prod, eval_multisetSum, eval_multiset_prod]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
⊢ x ∈ A

Tactic:
← inv_inv x

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
⊢ x⁻¹⁻¹ ∈ A
Module: Mathlib.Algebra.Polynomial.Splits

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

Tactic:
Nat.add_eq_zero_iff

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : f.natDegree = 0 ∧ g.natDegree = 0
⊢ f.Splits ∧ g.Splits
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x (C (p.coeff 0)) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
eval₂_C

Goal state after:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)