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

Goal state before:
pp: case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Finset b✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝) →
    ∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Tactic:
intro h s hs hs'

Goal state after:
case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h : ∀ (s : Finset b✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Set b✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)
⊢ P e✝
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective ⇑f
this✝ : Algebra R S := f.toAlgebra
this : IsLocalization (Submonoid.powers 1) R
⊢ P f

Tactic:
have := IsLocalization.isLocalization_of_algEquiv (.powers (1 : R))
    (AlgEquiv.ofBijective (Algebra.ofId R S) hf)

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective ⇑f
this✝¹ : Algebra R S := f.toAlgebra
this✝ : IsLocalization (Submonoid.powers 1) R
this : IsLocalization (Submonoid.powers 1) S
⊢ P f
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : x ∈ ⨅ p, ⨅ (x : p.IsPrime), ⨅ (_ : I ≤ p), RingHom.ker (algebraMap R (Localization.AtPrime p))
m : Ideal R
hm : m.IsMaximal
⊢ (algebraMap R (Localization.AtPrime m)) x ∈ map (algebraMap R (Localization.AtPrime m)) I

Tactic:
simp only [Submodule.mem_iInf, RingHom.mem_ker] at hx

Goal state after:
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
⊢ (algebraMap R (Localization.AtPrime m)) x ∈ map (algebraMap R (Localization.AtPrime m)) I
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
t : R
n : ℤ
⊢ (Finsupp.single 0 t) n = if n = 0 then t else 0

Tactic:
aesop

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

Goal state before:
pp: 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

Tactic:
exact ⟨0, Polynomial.C a * X ^ n, by simp⟩

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

Goal state before:
pp: case pos.e_f.e_t
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j' ↔ j' = j'
⊢ 1 = Pi.single (σ j') 1 (σ j')

Tactic:
Pi.single_eq_same

Goal state after:
case pos.e_f.e_t
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j' ↔ j' = j'
⊢ 1 = 1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
m : ℕ
hn : -↑m < 0
⊢ ↑x⁻¹ ^ m = ↑(x ^ (-↑m))

Tactic:
zpow_neg,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
m : ℕ
hn : -↑m < 0
⊢ ↑x⁻¹ ^ m = ↑(x ^ ↑m)⁻¹
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: p : Type u_4
R : Type u_6
inst✝³ : Fintype p
inst✝² : AddCommMonoid R
inst✝¹ : DecidableEq p
m : p → Type u_8
inst✝ : (i : p) → Fintype (m i)
M : (i : p) → Matrix (m i) (m i) R
⊢ (blockDiagonal' M).trace = ∑ i, (M i).trace

Tactic:
by
  simp [blockDiagonal', trace, Finset.sum_sigma']

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✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) * (A + U * C * V) =
    ⅟A * A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * A + ⅟A * U * C * V -
      ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V

Tactic:
by
      simp_rw [add_sub_assoc, _root_.mul_add, _root_.sub_mul, Matrix.mul_assoc]

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
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
let L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
    List.ofFn fun i : Fin r =>
      ⟨inl i, inr unit, by simp, -M (inl i) (inr unit) / M (inr unit) (inr unit)⟩
  let L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
    List.ofFn fun i : Fin r =>
      ⟨inr unit, inl i, by simp, -M (inr unit) (inl i) / M (inr unit) (inr unit)⟩
  refine ⟨L, L', ?_⟩
  have A : L.map toMatrix = listTransvecCol M := by simp [L, listTransvecCol, Function.comp_def]
  have B : L'.map toMatrix = listTransvecRow M := by simp [L', listTransvecRow, Function.comp_def]
  rw [A, B]
  exact isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow M hM

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
⊢ A.det • b ᵥ* A⁻¹ᵀᵀ = Aᵀ.cramer b

Tactic:
vecMul_transpose,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
⊢ A.det • A⁻¹ᵀ *ᵥ b = Aᵀ.cramer b
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
k : ℕ
i : n
⊢ X.coeff k - (C (M i i)).coeff k = (X.coeff k - (C M).coeff k) i i

Tactic:
simp only [coeff_X, coeff_C]

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
k : ℕ
i : n
⊢ ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i i
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

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

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

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

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

Tactic:
simpa only [Matrix.toBlocks_fromBlocks₂₂, Matrix.zero_mul, zero_add, ← fromBlocks_one] using
        congr_arg Matrix.toBlocks₂₂ this

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
⊢ ∀ (p : n × n), i = p.1 ∧ j = p.2 ↔ p = (i, j)

Tactic:
aesop

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✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : StarRing R
x : Matrix m m R ⊗[R] Matrix n n R
⊢ ∀ (x : Matrix m m R) (y : Matrix n n R),
    (kroneckerAlgEquiv m n R) (star (x ⊗ₜ[R] y)) = star ((kroneckerAlgEquiv m n R) (x ⊗ₜ[R] y))

Tactic:
simp [star_eq_conjTranspose, conjTranspose_kronecker]

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

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

Tactic:
· simp [mul_geom_sum, hn]

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ (-∑ i ∈ Finset.range n, r ^ i) * (r - 1) = 1
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
hdeg₂ : P.eraseLead.natDegree < P.natDegree
⊢ P.eraseLead.natDegree < P.natDegree

Tactic:
hdeg₂

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
⊢ ∃ q, map f q = p ∧ q.support = p.support

Tactic:
by
  rw [lifts_iff_coeff_lifts] at hlifts
  let g : ℕ → R := fun k ↦ (hlifts k).choose
  have hg : ∀ k, f (g k) = p.coeff k := fun k ↦ (hlifts k).choose_spec
  let q : R[X] := ∑ k ∈ p.support, monomial k (g k)
  have hq : map f q = p := by simp_rw [q, Polynomial.map_sum, map_monomial, hg, ← as_sum_support]
  have hq' : q.support = p.support := by
    simp_rw [Finset.ext_iff, mem_support_iff, q, finsetSum_coeff, coeff_monomial,
      Finset.sum_ite_eq', ite_ne_right_iff, mem_support_iff, and_iff_left_iff_imp, not_imp_not]
    exact fun k h ↦ by rw [← hg, h, map_zero]
  exact ⟨q, hq, hq'⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
r : R
hk : 0 < k
⊢ (hasseDeriv k) ((monomial 0) r) = 0

Tactic:
hasseDeriv_monomial,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
r : R
hk : 0 < k
⊢ (monomial (0 - k)) (↑(choose 0 k) * r) = 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
hk : 1 < k
⊢ (hasseDeriv k) ((monomial 1) 1) = 0

Tactic:
hasseDeriv_monomial,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
hk : 1 < k
⊢ (monomial (1 - k)) (↑(choose 1 k) * 1) = 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1)) =
    ↑k ! * (↑((n + k + 1).choose (n + 1)) * (↑(n + 1) * f.coeff (n + k + 1)))

Tactic:
simp only [← mul_assoc]

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * ↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1) =
    ↑k ! * ↑((n + k + 1).choose (n + 1)) * ↑(n + 1) * f.coeff (n + k + 1)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case mem
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : R →+* S
x✝ : R[X]
h✝ : x✝ ∈ {x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x}
⊢ (map i x✝).Splits

Tactic:
aesop

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

Goal state before:
pp: case one
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : R →+* S
⊢ (map i 1).Splits

Tactic:
aesop

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

Goal state before:
pp: case mul
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : 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})
a✝¹ : (map i x✝).Splits
a✝ : (map i y✝).Splits
⊢ (map i (x✝ * y✝)).Splits

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ (C ⋯.choose).Splits

Tactic:
aesop

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = p.coeff n

Tactic:
rw [h]
    rfl

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

Goal state before:
pp: case mem
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
this : ∀ (i : R), (X + C r + C i).Splits
x✝ : R[X]
h✝ : x✝ ∈ {x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x}
⊢ ((Polynomial.taylor r) x✝).Splits

Tactic:
aesop

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

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
this : ∀ (i : R), (X + C r + C i).Splits
⊢ ((Polynomial.taylor r) 1).Splits

Tactic:
aesop

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

Goal state before:
pp: case mul
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
this : ∀ (i : R), (X + C r + C i).Splits
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})
a✝¹ : ((Polynomial.taylor r) x✝).Splits
a✝ : ((Polynomial.taylor r) y✝).Splits
⊢ ((Polynomial.taylor r) (x✝ * y✝)).Splits

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
r : R
hr : IsUnit r
a : R
this : Function.Bijective fun x ↦ r * x
⊢ Multiset.count a (p.scaleRoots r).roots = Multiset.count a (Multiset.map (fun x ↦ r * x) p.roots)

Tactic:
obtain ⟨a, rfl⟩ := this.2 a

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
r : R
hr : IsUnit r
this : Function.Bijective fun x ↦ r * x
a : R
⊢ Multiset.count ((fun x ↦ r * x) a) (p.scaleRoots r).roots =
    Multiset.count ((fun x ↦ r * x) a) (Multiset.map (fun x ↦ r * x) p.roots)
Module: Mathlib.Algebra.Polynomial.Splits

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

Tactic:
obtain ⟨m, rfl⟩ := Multiset.exists_cons_of_mem ha
    rw [Multiset.map_cons, Multiset.prod_cons] at hm
    rw [hm] at h
    simp only [irreducible_mul_iff, IsUnit.mul_iff, not_isUnit_X_add_C, false_and, and_false,
      or_false, false_or, ← Multiset.prod_toList, List.prod_isUnit_iff] at h
    have : m = 0 := by simpa [not_isUnit_X_add_C, ← Multiset.eq_zero_iff_forall_notMem] using h.1.2
    grw [hm, this, natDegree_mul_le]
    simp

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
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), i (j a a_1) = a
⊢ C (i f.leadingCoeff) * (Multiset.map (fun x ↦ X - C x) (map i f).roots).prod =
    map i (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) (Multiset.pmap j (map i f).roots ⋯)).prod)

Tactic:
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
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
⊢ x * y ≠ 0

Tactic:
aesop

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
hf : ((X - C a) * f).Splits
hf₀ : f = 0
⊢ f.Splits

Tactic:
aesop

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
hf : ((X - C a) * f).Splits
hf₀ : ¬f = 0
this : (X - C a) * f = (X - C a) * (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod)
⊢ (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod).Splits

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : ((X - C a) * (f * g)).natDegree = n + 1
ha : eval a ((X - C a) * (f * g)) = 0
⊢ X - C a ≠ 0

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : ((X - C a) * (f * g)).natDegree = n + 1
ha : eval a ((X - C a) * (f * g)) = 0
⊢ f * g ≠ 0

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a ((X - C a) * (f * g)) = 0
⊢ f ≠ 0

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this✝ : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a ((X - C a) * (f * g)) = 0
this : f.Splits ∧ g.Splits
⊢ ((X - C a) * f).Splits ∧ g.Splits

Tactic:
aesop

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 = (Multiset.map (fun x ↦ X - C x) g.roots).prod
⊢ (Multiset.map (fun x ↦ (Multiset.map (fun x_1 ↦ x - x_1) g.roots).prod) s).prod =
    (Multiset.map (fun x ↦ (Multiset.map (eval x ∘ fun x ↦ X - C x) g.roots).prod) s).prod

Tactic:
congr! with x hx

Goal state after:
case a.e'_3.a
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
x : R
hx : x ∈ s
x✝ : R
a✝ : x✝ ∈ g.roots
⊢ HSub.hSub x = eval x ∘ fun x ↦ X - C x
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.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).coeff n ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
rw [Polynomial.coeff_scaleRoots]

Goal state after:
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ₘ)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
h : (f /ₘ (X - C x)).natDegree = 1
⊢ f /ₘ (X - C x) ≠ 0

Tactic:
aesop

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Field R
⊢ Splits 0

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p ∈ I
⊢ p.coeff 0 ∈ comap f I

Tactic:
← p.divX_mul_X_add,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r (p.divX * X + C (p.coeff 0)) ∈ I
⊢ p.coeff 0 ∈ comap f I
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 : I = ⊤
⊢ Nontrivial (N ⊗[R] M)

pp: case neg
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 : ¬I = ⊤
⊢ Nontrivial (N ⊗[R] M)

Tactic:
· rw [Ideal.eq_top_iff_one, Submodule.mem_annihilator_span_singleton, one_smul] at I_ne_top
    contradiction

Goal state after:
case neg
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 : ¬I = ⊤
⊢ Nontrivial (N ⊗[R] M)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
I : Ideal S
inst✝³ : Algebra R S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
hx0 : ¬x = 0
⊢ x ∈ ⊥

Tactic:
exact absurd hI (comap_ne_bot_of_integral_mem hx0 hx (Algebra.IsIntegral.isIntegral x))

Goal state after: