mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
y : R
inst✝ : CommSemiring R
⊢ (∀ (n : ℕ) (x : R), y ∣ x ^ n → y ∣ x) ↔ (Ideal.span {y}).IsRadical

Tactic:
← Ideal.mem_span_singleton

Goal state after:
R : Type u_1
y : R
inst✝ : CommSemiring R
⊢ (∀ (n : ℕ) (x : R), x ^ n ∈ Ideal.span {y} → x ∈ Ideal.span {y}) ↔ (Ideal.span {y}).IsRadical
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case h
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : ((f ^ n).restrict ⋯) ⟨x, ⋯⟩ = 0
⊢ ((f ^ n).restrict ⋯) ⟨x, hx⟩ = 0

Tactic:
LinearMap.restrict_apply

Goal state after:
case h
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : ⟨(f ^ n) ↑⟨x, ⋯⟩, ⋯⟩ = 0
⊢ ⟨(f ^ n) ↑⟨x, hx⟩, ⋯⟩ = 0
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' : M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m = (f P) m'
ne : ¬1 • m = 1 • m'
P : Ideal R
mP : P.IsMaximal
le : eqIdeal R m m' ≤ P
⊢ False

Tactic:
have ⟨s, hs⟩ := (IsLocalizedModule.eq_iff_exists P.primeCompl _).mp (h P)

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' : M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m = (f P) m'
ne : ¬1 • m = 1 • m'
P : Ideal R
mP : P.IsMaximal
le : eqIdeal R m m' ≤ P
s : ↥P.primeCompl
hs : s • m = s • m'
⊢ False
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝²⁹ : CommSemiring R✝
inst✝²⁸ : CommSemiring S
inst✝²⁷ : CommSemiring P
inst✝²⁶ : CommSemiring Q
M✝ : Submonoid R✝
T : Submonoid P
inst✝²⁵ : Algebra R✝ S
inst✝²⁴ : Algebra P Q
inst✝²³ : IsLocalization M✝ S
inst✝²² : IsLocalization T Q
g : R✝ →+* P
R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
r : Rₚ
⊢ (↑↑(map Bₚ f.toRingHom ⋯)).toFun ((algebraMap Rₚ Aₚ) r) = (algebraMap Rₚ Bₚ) r

Tactic:
obtain ⟨a, m, rfl⟩ := IsLocalization.exists_mk'_eq M r
    simp [algebraMap_mk' (S := A), algebraMap_mk' (S := B), map_mk']

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ Submonoid.map (algebraMap R S) (nonZeroDivisors R) ≤ nonZeroDivisors S

Tactic:
exact map_nonZeroDivisors_le M S

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
⊢ (Ideal.map (algebraMap S S') P).LiesOver (Ideal.map (algebraMap R R') p)

Tactic:
suffices h : Ideal.map (algebraMap R R') (under R (under R' (P.map (algebraMap S S')))) =
      Ideal.map (algebraMap R R') p from ⟨by rw [← h, IsLocalization.map_under (M := M)]⟩

Goal state after:
R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
⊢ Ideal.map (algebraMap R R') (under R (under R' (Ideal.map (algebraMap S S') P))) = Ideal.map (algebraMap R R') p
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_2
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 ∈ Submodule.span R a, ∃ z, 0 = mk' S 1 z • y

Tactic:
exact ⟨0, Submodule.zero_mem _, 1, by rw [mk'_one, map_one, one_smul]⟩

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
m : Ideal R
hm : m.IsMaximal
hx : ∀ (i : Ideal R) (i_1 : i.IsPrime), I ≤ i → (algebraMap R (Localization.AtPrime i)) x = 0
hle : ¬I ≤ m
⊢ (algebraMap R (Localization.AtPrime m)) x ∈ map (algebraMap R (Localization.AtPrime m)) I

Tactic:
simp [IsLocalization.AtPrime.map_eq_top_of_not_le _ hle]

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

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix n n α
h : A.IsSymm
f : n ≃ m
⊢ ((Matrix.reindex f f) A).IsSymm

Tactic:
rw [reindex_apply]

Goal state after:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix n n α
h : A.IsSymm
f : n ≃ m
⊢ (A.submatrix ⇑f.symm ⇑f.symm).IsSymm
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ x ∈ Finset.univ, (sign x • ∏ i, (X • A.map ⇑C + B.map ⇑C) (x i) i).coeff 0 = sign x • ∏ i, B (x i) i

Tactic:
rintro g -

Goal state after:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ (sign g • ∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff 0 = sign g • ∏ i, B (g i) i
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m : ℤ
n : ℕ
⊢ T m ^ n = T (↑n * m)

Tactic:
T,

Goal state after:
R : Type u_1
inst✝ : Semiring R
m : ℤ
n : ℕ
⊢ AddMonoidAlgebra.single m 1 ^ n = T (↑n * m)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m : ℤ
n : ℕ
⊢ AddMonoidAlgebra.single m 1 ^ n = T (↑n * m)

Tactic:
T,

Goal state after:
R : Type u_1
inst✝ : Semiring R
m : ℤ
n : ℕ
⊢ AddMonoidAlgebra.single m 1 ^ n = AddMonoidAlgebra.single (↑n * m) 1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Semiring R
n : ℤ
⊢ T 0 = 1

Tactic:
T_zero

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : Semiring R
n : ℤ
⊢ 1 = 1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ T n * (C a * T m) = C a * T m * T n

Tactic:
T,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ AddMonoidAlgebra.single n 1 * (C a * T m) = C a * T m * AddMonoidAlgebra.single n 1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ AddMonoidAlgebra.single n 1 * (C a * T m) = C a * T m * AddMonoidAlgebra.single n 1

Tactic:
T,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ AddMonoidAlgebra.single n 1 * (C a * AddMonoidAlgebra.single m 1) =
    C a * AddMonoidAlgebra.single m 1 * AddMonoidAlgebra.single n 1
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

Goal state after:
case refine_2.ofNat
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ∃ n_1 f', toLaurent f' = C a * T (Int.ofNat n) * T ↑n_1

case refine_2.negSucc
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ∃ n_1 f', toLaurent f' = C a * T (Int.negSucc n) * T ↑n_1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : MulActionWithZero R S
inst✝ : Monoid S
n : ℤ
x : Sˣ
⊢ (T n).smeval x = ↑(x ^ n)

Tactic:
T,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : MulActionWithZero R S
inst✝ : Monoid S
n : ℤ
x : Sˣ
⊢ smeval (AddMonoidAlgebra.single n 1) x = ↑(x ^ n)
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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det ^ Fintype.card n = A'.det * A'.det ^ (Fintype.card n - 1)

Tactic:
by rw [← pow_succ', h_card]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
g : ℕ → R
x : ℕ
hg : ∑ i ∈ Finset.range 0, g i • (r * ↑s ^ (i + x)) = 0
i : ℕ
hin : i < 0
⊢ g i = 0

Tactic:
contradiction

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

Goal state before:
pp: case neg
𝕜 : 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 ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
⊢ ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
rw [IH]

Goal state after:
case neg
𝕜 : 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 ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())
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 α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
⊢ (A * B).adjugate = B.adjugate * A.adjugate

Tactic:
have hAB : IsLeftRegular (A * B).det := by
    rw [det_mul]
    exact hA.mul hB
  refine (isRegular_of_isLeftRegular_det hAB).left ?_
  simp only
  rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]

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 : Matrix n n α
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A

Tactic:
have : A * (A.adjugate * A.adjugate.adjugate) =
      A * (A.det ^ (Fintype.card n - 1) • (1 : Matrix n n α)) := by
    rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
this : A * (A.adjugate * A.adjugate.adjugate) = A * A.det ^ (Fintype.card n - 1) • 1
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
⊢ [].prod⁻¹ = (List.map Inv.inv [].reverse).prod

Tactic:
by rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]

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

Goal state before:
pp: case e_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
e : ℕ
a : R
⊢ (x + y) ^ e = x ^ e + ↑e * x ^ (e - 1) * y + ↑(powAddExpansion x y e) * y ^ 2

Tactic:
apply (powAddExpansion _ _ _).property

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ (r - 1) * -∑ i ∈ Finset.range n, r ^ i = 1

Tactic:
simp [mul_geom_sum, hn]

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

Goal state before:
pp: case neg
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : ¬s.Finite
⊢ ⨅ s, (↑↑s).encard ≤ s.encard

Tactic:
Set.Infinite.encard_eq hs

Goal state after:
case neg
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : ¬s.Finite
⊢ ⨅ s, (↑↑s).encard ≤ ⊤
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
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ M.charpoly.degree = ↑(Fintype.card n)

pp: case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ M.charpoly.degree = ↑(Fintype.card n)

Tactic:
· rw [h]
    unfold charpoly
    rw [det_eq_one_of_card_eq_zero]
    · simp
    · assumption

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ M.charpoly.degree = ↑(Fintype.card n)
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
⊢ eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace

Tactic:
let e := Matrix.reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
  rw [← Matrix.det_reindexLinearEquiv_self R[X] (Fintype.equivFin n)]
  convert! derivative_det_one_add_X_smul_aux (e M)
  · ext; simp [map_add, e]
  · delta trace
    rw [← (Fintype.equivFin n).symm.sum_comp]
    simp_rw [e, coe_reindexLinearEquiv, reindex_apply, diag_apply, submatrix_apply]

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 0 = 1

Tactic:
T_zero

Goal state after:
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
⊢ 1 = 1
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
s : Finset n
⊢ (of (s.piecewise M.row (row 1))).det = (M.submatrix Subtype.val Subtype.val).det

Tactic:
let e := Equiv.sumCompl (fun x => x ∈ s)
  let +generalize A : Matrix n n R := Matrix.of (s.piecewise M (1 : Matrix n n R))
  rw [← Matrix.det_submatrix_equiv_self e A]
  have h_blocks : A.submatrix e e =
      Matrix.fromBlocks
        (M.submatrix Subtype.val Subtype.val)
        (M.submatrix Subtype.val Subtype.val) 0 1 := by
    ext (i | i) (j | j) <;> dsimp [A, e]
    · simp only [Finset.piecewise, if_pos i.prop]
    · simp only [Finset.piecewise, if_pos i.prop]
    · simp only [Finset.piecewise, if_neg i.prop]
      exact Matrix.one_apply_ne (fun h => i.prop (h ▸ j.prop))
    · simp only [Finset.piecewise, if_neg i.prop, Matrix.one_apply, Subtype.ext_iff]
  rw [h_blocks, Matrix.det_fromBlocks_zero₂₁, Matrix.det_one, mul_one]

Goal state after:
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).choose k) * ↑(i.choose l) = ↑((k + l).choose k) * ↑(i.choose (k + l))

Tactic:
cast_choose ℚ h1,

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).choose k) * (↑i ! / (↑l ! * ↑(i - l)!)) = ↑((k + l).choose k) * ↑(i.choose (k + l))
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this✝ : p.coeff p.natDegree ≠ 0
this : p.leadingCoeff = 0
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : p.coeff i ≠ 0
ps_zero : p.coeff i * s ^ (p.natDegree - i) = 0
this : p.coeff i = 0
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this✝ : (a : Prop) → Decidable a
hp : ¬p = 0
h : p.leadingCoeff = 0
this : p = 0
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
i : ℕ
⊢ ↑((toSubring 1 T ⋯).coeff i) = ↑(coeff 1 i)

Tactic:
by
    rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
      OneMemClass.coe_one]

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

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.Splits
hf0 : 0 ≠ 0
hf₀ : ¬f.leadingCoeff = 0
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) 0).prod
⊢ ∃ a, eval a f = 0

Tactic:
contradiction

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

Goal state before:
pp: case mul
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
φ : R →+* S
x y : R[X]
hx✝ : x ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy✝ : y ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hx : map φ x ≠ 0 → (map φ x).roots = Multiset.map (⇑φ) x.roots
hy : map φ y ≠ 0 → (map φ y).roots = Multiset.map (⇑φ) y.roots
hφ : map φ (x * y) ≠ 0
⊢ (map φ (x * y)).roots = Multiset.map (⇑φ) (x * y).roots

Tactic:
| mul x y _ _ hx hy =>

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this : g = C g.leadingCoeff * (Multiset.map (fun x ↦ X - C x) g.roots).prod
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (s ×ˢ g.roots)).prod = (Multiset.map (fun x ↦ eval x g) s).prod

Tactic:
rw [hg.leadingCoeff, map_one, one_mul] at this

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this : g = (Multiset.map (fun x ↦ X - C x) g.roots).prod
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (s ×ˢ g.roots)).prod = (Multiset.map (fun x ↦ eval x g) s).prod
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
⊢ ⇑g '' f.rootSet A = f.rootSet B

Tactic:
by
  classical
  rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
h : 0 ≠ 0
⊢ eval₂ f r 0 = 0 → ∃ i, coeff 0 i ≠ 0 ∧ coeff 0 i ∈ comap f I

Tactic:
contradiction

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case pos
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := (R ∙ n).annihilator
I_ne_top : n = 0
⊢ Nontrivial (N ⊗[R] M)

Tactic:
contradiction

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
x : ↥l23.ker
m : M
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = x ⊗ₜ[R] m

Tactic:
rcases x with ⟨x, (hx : l23 x = 0)⟩
    have mem : x ⊗ₜ[R] m ∈ LinearMap.ker (l23.rTensor M) := by simp [hx]
    rw [LinearMap.exact_iff.1 ex] at mem
    obtain ⟨y, hy⟩ := mem
    refine ⟨LinearMap.rTensor M (LinearMap.rangeRestrict _ ∘ₗ LinearMap.rangeRestrict l12) y,
      Module.Flat.rTensor_preserves_injective_linearMap (LinearMap.ker l23).subtype
      Subtype.val_injective ?_⟩
    simp only [LinearMap.comp_codRestrict, LinearMap.rTensor_tmul, Submodule.coe_subtype, ← hy]
    rw [← LinearMap.comp_apply, ← LinearMap.rTensor_def, ← LinearMap.rTensor_comp,
      ← LinearMap.comp_apply, ← LinearMap.rTensor_comp, LinearMap.comp_assoc,
      LinearMap.subtype_comp_codRestrict, ← LinearMap.comp_assoc, Submodule.subtype_comp_inclusion,
      LinearMap.subtype_comp_codRestrict]

Goal state after: