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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
m : M
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ localized₀ P.primeCompl (f P) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
x✝ : ∃ M, M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s t : ↥P.primeCompl
ht : t • s • m = t • 1 • a
⊢ False

Tactic:
smul_smul

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
m : M
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ localized₀ P.primeCompl (f P) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
x✝ : ∃ M, M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s t : ↥P.primeCompl
ht : (t * s) • m = (t * 1) • a
⊢ False
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
a : M
ha : a ∈ N
t : ↥(Submonoid.powers ↑r)
e : ∃ s_1, s_1 • t • m = s_1 • 1 • a
u : ↥(Submonoid.powers ↑r)
hu : u • t • m = u • 1 • a
⊢ False

Tactic:
smul_smul

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
a : M
ha : a ∈ N
t : ↥(Submonoid.powers ↑r)
e : ∃ s_1, s_1 • t • m = s_1 • 1 • a
u : ↥(Submonoid.powers ↑r)
hu : (u * t) • m = (u * 1) • a
⊢ False
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
⊢ m ∈ N

Tactic:
let I : Ideal R := N.comap (LinearMap.toSpanSingleton R M m)
  suffices I = ⊤ by simpa [I] using I.eq_top_iff_one.mp this
  by_contra! ne
  have ⟨r, hrs, disj⟩ := exists_disjoint_powers_of_span_eq_top s span_eq _ ne
  let r : s := ⟨r, hrs⟩
  obtain ⟨a, ha, t, e⟩ := h r
  rw [← IsLocalizedModule.mk'_one (.powers r.1), IsLocalizedModule.mk'_eq_mk'_iff] at e
  have ⟨u, hu⟩ := e
  simp_rw [smul_smul] at hu
  exact Set.disjoint_right.mp disj (u * t).2 (by apply hu ▸ smul_mem _ _ ha)

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n : ℕ
e : ∃ c, ↑c * (x * s ^ n) = ↑c * ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Tactic:
obtain ⟨⟨_, m, rfl⟩, e⟩ := e

Goal state after:
case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : ↑⟨(fun x ↦ s ^ x) m, ⋯⟩ * (x * s ^ n) = ↑⟨(fun x ↦ s ^ x) m, ⋯⟩ * ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (algebraMap R S) (r * rn) - mk' S r ⟨m, hm⟩ ∈ I

Tactic:
←
      Ideal.Quotient.eq_zero_iff_mem,

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.Quotient.mk I) ((algebraMap R S) (r * rn) - mk' S r ⟨m, hm⟩) = 0
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: S : Type u_2
inst✝⁴ : CommSemiring S
R : Type u_4
inst✝³ : CommRing R
inst✝² : NoZeroDivisors R
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
⊢ FaithfulSMul R S

Tactic:
by
  rw [faithfulSMul_iff_algebraMap_injective, IsLocalization.injective_iff_isRegular P.primeCompl]
  exact fun ⟨_, h⟩ ↦ .of_ne_zero <| by aesop

Goal state after:
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_3
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalization M S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z • y + mk' S 1 z' • y' =
    (mk' S 1 (z * z') * (algebraMap R S) ↑z') • y + mk' S 1 (z * z') • (algebraMap R S) ↑z • y'

Tactic:
smul_smul

Goal state after:
case mp.refine_3
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalization M S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z • y + mk' S 1 z' • y' =
    (mk' S 1 (z * z') * (algebraMap R S) ↑z') • y + (mk' S 1 (z * z') * (algebraMap R S) ↑z) • y'
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ ∃ n_1 f', toLaurent f' = C a * T n * T ↑n_1

Tactic:
rcases n with n | n
    · exact ⟨0, Polynomial.C a * X ^ n, by simp⟩
    · refine ⟨n + 1, Polynomial.C a, ?_⟩
      simp only [Int.negSucc_eq, Polynomial.toLaurent_C, Int.natCast_succ, mul_T_assoc,
        neg_add_cancel, T_zero, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
M' : Submodule R M
⊢ lift.{uM, max uM uR} (Module.rank (FractionRing R) (LocalizedModule R⁰ M ⧸ Submodule.localized R⁰ M')) +
      lift.{uM, max uM uR} (Module.rank (FractionRing R) ↥(Submodule.localized R⁰ M')) =
    lift.{uM, max uM uR} (Module.rank (FractionRing R) (LocalizedModule R⁰ M))

Tactic:
← lift_add,

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
M' : Submodule R M
⊢ lift.{uM, max uM uR}
      (Module.rank (FractionRing R) (LocalizedModule R⁰ M ⧸ Submodule.localized R⁰ M') +
        Module.rank (FractionRing R) ↥(Submodule.localized R⁰ M')) =
    lift.{uM, max uM uR} (Module.rank (FractionRing R) (LocalizedModule R⁰ M))
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : A.IsSymm
⊢ A.adjugate.IsSymm

Tactic:
by
  rw [IsSymm, Matrix.adjugate_transpose, hA.eq]

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

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
m : Type u_4
a : m
b : n
hb : b ≠ j
c : R
M : Matrix m n R
⊢ (M * transvection i j c) a b = M a b

Tactic:
simp [transvection, Matrix.mul_add, hb]

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 * T n) = f r * ↑(x ^ n)

Tactic:
by
  simp

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

Goal state before:
pp: n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ (reindexEquiv e { i := t_i, j := t_j, hij := hij✝, c := c✝ }).toMatrix a b =
    (reindexAlgEquiv R R e) { i := t_i, j := t_j, hij := hij✝, c := c✝ }.toMatrix a b

Tactic:
simp only [reindexEquiv, transvection, toMatrix_mk]

Goal state after:
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b
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 B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
⊢ B = C * A ↔ A = ⅟C * B

Tactic:
← Matrix.invOf_mul_eq_iff_eq_mul_left,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
⊢ ⅟C * B = A ↔ A = ⅟C * B
Module: Mathlib.LinearAlgebra.Matrix.Transvection

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

Tactic:
simp only [length_listTransvecCol, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
      Matrix.one_mul]
    rw [if_neg]
    simpa only [not_le] using i.2

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
f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N
M : Matrix n n α
⊢ (g M).det.Monic

Tactic:
simp only [g, Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm]

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : k = k✝
⊢ single i j x = single i j x

Tactic:
funext
        simp

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : ¬k = k✝
⊢ 0 = single i j 0

Tactic:
funext
        simp

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
M : Matrix n n R
h : eval M (matPolyEquiv (M.charpoly • 1)) = eval M (matPolyEquiv M.charmatrix.adjugate * (X - C M))
⊢ (aeval M) M.charpoly = 0

Tactic:
rw [eval_mul_X_sub_C] at h

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (matPolyEquiv (M.charpoly • 1)) = 0
⊢ (aeval M) M.charpoly = 0
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)ˣ
N : Matrix n n R
⊢ ((↑M)⁻¹ * N * ↑M).charpoly = N.charpoly

Tactic:
by
  simpa using charpoly_units_conj M⁻¹ N

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

Goal state before:
pp: case a.a
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
⊢ (M - (scalar n) μ).charmatrix (σ i) i = (M.charmatrix (σ i) i).comp (X + C μ)

Tactic:
by_cases hi : σ i = i <;> simp [hi]

Goal state after:
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)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ ∑ x,
      ((eval 0 (derivative ((-1) ^ ↑x)) * eval 0 (1 0 x) + (-1) ^ ↑x * (eval 0 (derivative (1 0 x)) + M 0 x)) *
          eval 0 (submatrix 1 Fin.succ x.succAbove).det +
        (-1) ^ ↑x * eval 0 (1 0 x) *
          eval 0 (derivative (submatrix 1 Fin.succ x.succAbove + X • (M.submatrix Fin.succ x.succAbove).map ⇑C).det)) =
    M.trace

Tactic:
Finset.sum_eq_single 0

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ (eval 0 (derivative ((-1) ^ ↑0)) * eval 0 (1 0 0) + (-1) ^ ↑0 * (eval 0 (derivative (1 0 0)) + M 0 0)) *
        eval 0 (submatrix 1 Fin.succ (Fin.succAbove 0)).det +
      (-1) ^ ↑0 * eval 0 (1 0 0) *
        eval 0
          (derivative
            (submatrix 1 Fin.succ (Fin.succAbove 0) + X • (M.submatrix Fin.succ (Fin.succAbove 0)).map ⇑C).det) =
    M.trace

case succ.h₀
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ ∀ b ∈ univ,
    b ≠ 0 →
      (eval 0 (derivative ((-1) ^ ↑b)) * eval 0 (1 0 b) + (-1) ^ ↑b * (eval 0 (derivative (1 0 b)) + M 0 b)) *
            eval 0 (submatrix 1 Fin.succ b.succAbove).det +
          (-1) ^ ↑b * eval 0 (1 0 b) *
            eval 0 (derivative (submatrix 1 Fin.succ b.succAbove + X • (M.submatrix Fin.succ b.succAbove).map ⇑C).det) =
        0

case succ.h₁
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ 0 ∉ univ →
    (eval 0 (derivative ((-1) ^ ↑0)) * eval 0 (1 0 0) + (-1) ^ ↑0 * (eval 0 (derivative (1 0 0)) + M 0 0)) *
          eval 0 (submatrix 1 Fin.succ (Fin.succAbove 0)).det +
        (-1) ^ ↑0 * eval 0 (1 0 0) *
          eval 0
            (derivative
              (submatrix 1 Fin.succ (Fin.succAbove 0) + X • (M.submatrix Fin.succ (Fin.succAbove 0)).map ⇑C).det) =
      0
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R ≃+* T
I : Ideal R
⊢ Cardinal.lift.{u, v} (Submodule.spanRank (map f I)) = Cardinal.lift.{v, u} (Submodule.spanRank I)

Tactic:
apply (I.lift_spanRank_map_le (f : R →+* T)).antisymm
  nth_rw 1 [← Ideal.map_of_equiv f (I := I)]
  exact Ideal.lift_spanRank_map_le (f.symm : T →+* R) _

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
this : Nontrivial R
⊢ Module.rank R M = ⊤.spanRank

Tactic:
obtain ⟨I, B⟩ := ‹Module.Free R M›

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
this : Nontrivial R
I : Type u_2
B : Basis I R M
⊢ Module.rank R M = ⊤.spanRank
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
⊢ (Subalgebra.toSubmodule R[]).FG

Tactic:
refine ⟨{1}, Submodule.ext fun x => ?_⟩

Goal state after:
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[]
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: m n k : ℕ
⊢ (m + n).choose k = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2

Tactic:
by
  calc
    (m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, cast_id]
    _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
    _ = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by
      rw [coeff_mul, Finset.sum_congr rfl]
      simp only [coeff_X_add_one_pow, cast_id, imp_true_iff]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * ↑(i.choose n)

Tactic:
Nat.choose_eq_zero_of_lt h,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * ↑0
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : ¬p = 0
⊢ ((taylor r) p).degree = p.degree

Tactic:
· rw [degree_eq_natDegree hp, degree_eq_iff_natDegree_eq ((taylor_eq_zero r p).not.2 hp),
      natDegree_taylor]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
⊢ (((taylor r) f).sum fun i a ↦ C a * (X - C r) ^ i) = f

Tactic:
rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_cancel,
    taylor_zero]

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

Goal state before:
pp: case e_a
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
⊢ -(X • M.map ⇑C) = X • (-M).map ⇑C

Tactic:
rw [Matrix.map_neg C (map_neg C) M, smul_neg]

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
⊢ f (p.coeff i * s ^ (p.natDegree - i)) * (f s * a) ^ i = f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i

Tactic:
by
        simp_rw [f.map_mul, f.map_pow, pow_add, hsa.mul_pow, mul_assoc]

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
hi : i ∈ p.support
⊢ f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i = f s ^ p.natDegree * (f (p.coeff i) * a ^ i)

Tactic:
rw [mul_assoc, ← map_pow, (hf _ _).left_comm, map_pow, tsub_add_cancel_of_le]

Goal state after:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
hi : i ∈ p.support
⊢ i ≤ p.natDegree
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
hfi : f.coeff i ≠ 0
hi : f.degree = ↑i
⊢ 1 ≠ 0

Tactic:
simp [hf, hfi]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
hfi : f.coeff i ≠ 0
hi : ¬f.degree = ↑i
⊢ f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i) ≠ 0

Tactic:
simp [hf, hfi]

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
n : ℕ
⊢ ↑((p.toSubring T hp).coeff n) = p.coeff n

Tactic:
by
  simp

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

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

Tactic:
refine splits_iff_exists_multiset'.trans ⟨?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ (∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod) →
    ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod

case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ (∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod) →
    ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hR : IsField R
this : Field R := hR.toField
y : Sˣ
hx : ↑y ≠ 0
⊢ ∃ b, ↑y * b = 1

Tactic:
exact ⟨y.inv, y.val_inv⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : IsIntegral R 0
⊢ (algebraMap A B) (mk' A 0 h) = (algebraMap A B) 0

Tactic:
rw [algebraMap_mk', map_zero]

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.IsIntegral R A
I : Ideal A
inst✝ : I.IsPrime
⊢ I ∈ (map (algebraMap R A) (under R I)).minimalPrimes

Tactic:
by
  refine ⟨⟨inferInstance, map_comap_le⟩, fun r ⟨hr, hpr⟩ hrq ↦ ?_⟩
  contrapose! hpr
  exact mt map_le_iff_le_comap.mp (not_le_of_gt (IsIntegral.comap_lt_comap (hrq.lt_of_not_ge hpr)))

Goal state after: