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

Goal state before:
pp: case h₁
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit ((Ideal.Quotient.mk I) x)
⊢ IsUnit x

Tactic:
obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (↑H.unit⁻¹ : S ⧸ I)

Goal state after:
case h₁
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit ((Ideal.Quotient.mk I) x)
y : S
hy : (Ideal.Quotient.mk I) y = ↑H.unit⁻¹
⊢ IsUnit x
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: 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
I : Ideal R
hI : I.IsPrimary
hM : ∃ x ∈ ↑M, x ∈ ↑I.radical
⊢ ∃ x ∈ ↑M, x ∈ ↑I

Tactic:
obtain ⟨a, ha, k, hk⟩ := hM

Goal state after:
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
I : Ideal R
hI : I.IsPrimary
a : R
ha : a ∈ ↑M
k : ℕ
hk : a ^ k ∈ I
⊢ ∃ x ∈ ↑M, x ∈ ↑I
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
⊢ 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
  refine Not.imp_symm I.exists_le_maximal fun ⟨P, hP, le⟩ ↦ ?_
  obtain ⟨a, ha, s, e⟩ := h P
  rw [← IsLocalizedModule.mk'_one P.primeCompl, IsLocalizedModule.mk'_eq_mk'_iff] at e
  obtain ⟨t, ht⟩ := e
  simp_rw [smul_smul] at ht
  exact (t * s).2 (le <| by apply ht ▸ smul_mem _ _ ha)

Goal state after:
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 = ⊤
Rₚ : ↑s → Type u_4
inst✝⁷ : (r : ↑s) → CommSemiring (Rₚ r)
inst✝⁶ : (r : ↑s) → Algebra R (Rₚ r)
inst✝⁵ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)
Mₚ : ↑s → Type u_5
inst✝⁴ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝³ : (r : ↑s) → Module R (Mₚ r)
inst✝² : (r : ↑s) → Module (Rₚ r) (Mₚ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
N : Submodule R M
h : ∀ (r : ↑s), localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N = ⊥
x✝ : ↑s
⊢ localized' (Rₚ x✝) (Submonoid.powers ↑x✝) (f x✝) N = localized' (Rₚ x✝) (Submonoid.powers ↑x✝) (f x✝) ⊥

Tactic:
simp only [h, Submodule.localized'_bot]

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 :
  (algebraMap R (Localization.Away s)) x * (algebraMap R (Localization.Away s)) ↑(y, ⟨(fun x ↦ s ^ x) n, ⋯⟩).2 =
    (algebraMap R (Localization.Away s)) ↑(y, ⟨(fun x ↦ s ^ x) n, ⋯⟩).1
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Tactic:
dsimp only at 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 : ℕ
e :
  (algebraMap R (Localization.Away s)) x * (algebraMap R (Localization.Away s)) (s ^ n) =
    (algebraMap R (Localization.Away s)) ↑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.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * (Ideal.Quotient.mk (Ideal.under R I)) rn = 1
⊢ (Ideal.quotientMap I (algebraMap R S) H) ((Ideal.Quotient.mk J) (r * rn)) = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

Tactic:
replace hn := congr_arg (Ideal.quotientMap I (algebraMap R S) le_rfl) hn

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.Quotient.mk (Ideal.under R I)) rn) =
    (Ideal.quotientMap I (algebraMap R S) ⋯) 1
⊢ (Ideal.quotientMap I (algebraMap R S) H) ((Ideal.Quotient.mk J) (r * rn)) = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)
Module: Mathlib.RingTheory.Flat.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝³ : AddCommMonoid P
x✝² : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) N.subtype.range)
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) N.subtype.range) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
x✝¹ : S
x✝ : ↥N
⊢ ((AlgebraTensorModule.curry (lTensor S N.subtype)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((Submodule.localized₀ p ((TensorProduct.mk R S P) 1) N.subtype.range).subtype ∘ₗ ↑e))
        x✝¹)
      x✝

Tactic:
change _ = (h.equiv _).1

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝³ : AddCommMonoid P
x✝² : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) N.subtype.range)
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) N.subtype.range) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
x✝¹ : S
x✝ : ↥N
⊢ ((AlgebraTensorModule.curry (lTensor S N.subtype)) x✝¹) x✝ =
    ↑(h.equiv (↑(LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯)) (((TensorProduct.mk R S ↥N) x✝¹) x✝)))
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : R
y : ↥I.primeCompl
⊢ (localRingHom I J f hIJ) (mk x y) = mk (f x) ⟨f ↑y, ⋯⟩

Tactic:
simp_rw [mk_eq_mk', localRingHom_mk']

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

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

Tactic:
exact ⟨x, Submodule.subset_span hx, 1, by rw [mk'_one, map_one, one_smul]⟩

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

Goal state before:
pp: case e'_3
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i, A (g i) i = (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n * 1)

Tactic:
convert! (coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm

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

case e'_3.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∀ p ∈ Finset.univ, ((X • A.map ⇑C + B.map ⇑C) (g p) p).natDegree ≤ 1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
hn : ¬0 ≤ n
a : ℕ
⊢ ((comapDomainAddMonoidHom Nat.cast trunc._proof_1) (AddMonoidAlgebra.single n r)).coeff a = (toFinsupp 0).coeff a

Tactic:
have : a ≠ n := by lia

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
hn : ¬0 ≤ n
a : ℕ
this : ↑a ≠ n
⊢ ((comapDomainAddMonoidHom Nat.cast trunc._proof_1) (AddMonoidAlgebra.single n r)).coeff a = (toFinsupp 0).coeff a
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : B * A = 1
⊢ B.det * A.det = 1

Tactic:
rw [← det_mul, h, det_one]

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

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A * B = 1
⊢ A.det * B.det = 1

Tactic:
rw [← det_mul, h, det_one]

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

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹

Tactic:
by
  obtain ⟨_⟩ := hA.nonempty_invertible
  obtain ⟨ih⟩ := h.nonempty_invertible
  simp only [← invOf_eq_nonsing_inv] at ih
  let := invertibleAddMulMul' A U C V
  simp only [← invOf_eq_nonsing_inv]
  apply invOf_add_mul_mul'

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

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

Tactic:
have : M' = fromBlocks M'' 0 0 (diagonal fun _ => c) := by
    rw [← fromBlocks_toBlocks M', hM.1, hM.2]
    rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (-(r + 1))

Tactic:
neg_add'

Goal state after:
R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (-r - 1)
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case inl
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h1 : ⨅ s, ⨅ (_ : span R s = p), s.encard = ⊤
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑(↑s).card

Tactic:
rw [h1, eq_comm]

Goal state after:
case inl
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h1 : ⨅ s, ⨅ (_ : span R s = p), s.encard = ⊤
⊢ ⨅ s, ↑(↑s).card = ⊤
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.spanFinrank = 1
⊢ p ≠ ⊥

Tactic:
grind [spanFinrank_bot]

Goal state after:
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
⊢ eval₂ (g.comp f) (g x) p = 0

Tactic:
← hom_eval₂,

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₂ f x p = 0
⊢ g (eval₂ f x p) = 0
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
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (M.charpoly - ∏ i, (X - C (M i i)) + ∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)

Tactic:
rw [degree_add_eq_right_of_degree_lt]

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
h1 : (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)

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
h1 : (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (M.charpoly - ∏ i, (X - C (M i i))).degree < (∏ i, (X - C (M i i))).degree
Module: Mathlib.Algebra.Polynomial.Eval.Subring

Goal state before:
pp: case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : f c = p.coeff i
⊢ C (f c) * map f (X ^ i) = C (p.coeff i) * X ^ i

Tactic:
hc,

Goal state after:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : f c = p.coeff i
⊢ C (p.coeff i) * map f (X ^ i) = C (p.coeff i) * X ^ i
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case right
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
⊢ eval₂ ((algebraMap A B).comp (algebraMap R A)) ((algebraMap A B) x) f = 0

Tactic:
← hom_eval₂,

Goal state after:
case right
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
⊢ (algebraMap A B) (eval₂ (algebraMap R A) x f) = 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
⊢ IsIntegral R r ↔ ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r

Tactic:
by
  constructor <;> intro hr
  · rcases hr with ⟨p, hmp, hpr⟩
    refine ⟨_, Finset.finite_toSet _, p.restriction, monic_restriction.2 hmp, ?_⟩
    rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr]
  rcases hr with ⟨s, _, hsr⟩
  exact hsr.of_subring _

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 : ℕ
⊢ M ^ k = (aeval M) (X ^ k %ₘ M.charpoly)

Tactic:
← aeval_eq_aeval_mod_charpoly,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
⊢ M ^ k = (aeval M) (X ^ k)
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).leadingCoeff = 0 ↔ f.leadingCoeff = 0

Tactic:
leadingCoeff_taylor

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ f.leadingCoeff = 0 ↔ f.leadingCoeff = 0
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:
Matrix.map_neg C (map_neg C) M,

Goal state after:
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
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
i : ℕ
⊢ i ∈ (p.toSubring T hp).support ↔ i ∈ p.support

Tactic:
simp only [mem_support_iff, not_iff_not, Ne]

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
⊢ (p.toSubring T hp).coeff i = 0 ↔ p.coeff i = 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hmg : ∀ y ∈ mg, y ∈ {x | ∃ a, X + C a = x}
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
⊢ ∃ m, C a * mg.prod = C (C a * mg.prod).leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod

Tactic:
choose! j hj using hmg

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
⊢ ∃ m, C a * mg.prod = C (C a * mg.prod).leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
hx : IsIntegral R x
⊢ R[x] ≤ integralClosure R A

Tactic:
rw [Algebra.adjoin_le_iff]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
hx : IsIntegral R x
⊢ {x} ⊆ ↑(integralClosure R A)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case mp
R : Type u_1
A : Type u_2
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : A ≃ₐ[R] S
y : S
⊢ (∃ x ∈ integralClosure R A, ↑f x = y) → y ∈ integralClosure R S

pp: case mpr
R : Type u_1
A : Type u_2
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : A ≃ₐ[R] S
y : S
⊢ y ∈ integralClosure R S → ∃ x ∈ integralClosure R A, ↑f x = y

Tactic:
· rintro ⟨x, hx, rfl⟩
    exact hx.map f

Goal state after:
case mpr
R : Type u_1
A : Type u_2
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : A ≃ₐ[R] S
y : S
⊢ y ∈ integralClosure R S → ∃ x ∈ integralClosure R A, ↑f x = y
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↥(integralClosure R A)
p : R[X]
hpm : p.Monic
hpx : eval₂ (algebraMap R A) (↑x) p = 0
⊢ ↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) = ↑0

Tactic:
rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx

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

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
p : R[X]
x : S
inst✝ : Algebra R S
h : (aeval x) p = 0
⊢ IsIntegral R (p.leadingCoeff • x)

Tactic:
rw [aeval_def] at h
  rw [Algebra.smul_def]
  exact (algebraMap R S).isIntegralElem_leadingCoeff_mul p x h

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
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x y : S
⊢ mk' A ((algebraMap S B) (x + y)) ⋯ = mk' A ((algebraMap S B) x) ⋯ + mk' A ((algebraMap S B) y) ⋯

Tactic:
simp_rw [← mk'_add, map_add]

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

Goal state before:
pp: case inr.refine_3
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ : Polynomial.map (algebraMap R Rₘ) p' = p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))
hp'₂ : p'.Monic
⊢ eval₂ ((algebraMap Rₘ S).comp (algebraMap R Rₘ)) (commonDenom M p.support p.coeff • x) p' = 0

Tactic:
← Polynomial.eval₂_map,

Goal state after:
case inr.refine_3
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ : Polynomial.map (algebraMap R Rₘ) p' = p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))
hp'₂ : p'.Monic
⊢ eval₂ (algebraMap Rₘ S) (commonDenom M p.support p.coeff • x) (Polynomial.map (algebraMap R Rₘ) p') = 0