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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ P) (Localization.awayMap f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
x✝ : (r : R) → Algebra (Localization.Away r) (Localization.Away ((algebraMap R S) r)) :=
  fun r ↦ (Localization.awayMap (algebraMap R S) r).toAlgebra
r : R
hr : r ∈ s
⊢ algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S) =
    (↑(IsLocalization.Away.tensorRightEquiv S r (Localization.Away r)).symm).comp
      (algebraMap (Localization.Away r) (Localization.Away ((algebraMap R S) r)))

Tactic:
apply IsLocalization.ringHom_ext (Submonoid.powers r)

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ P) (Localization.awayMap f ↑r)
algInst✝ : Algebra R S := ⋯
x✝ : (r : R) → Algebra (Localization.Away r) (Localization.Away ((algebraMap R S) r)) := ⋯
r : R
hr : r ∈ s
⊢ (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S)).comp (algebraMap R (Localization.Away r)) =
    ((↑(IsLocalization.Away.tensorRightEquiv S r (Localization.Away r)).symm).comp
          (algebraMap (Localization.Away r) (Localization.Away ((algebraMap R S) r)))).comp
      (algebraMap R (Localization.Away r))
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.span (⇑f '' s) = ⊤
r : R
hr : r ∈ s
⊢ P ((IsLocalization.map (Localization.Away ↑⟨f r, ⋯⟩) f ?m.175).comp (algebraMap R (Localization.Away r)))

Tactic:
apply hP' _ r
    exact hs' ⟨r, hr⟩

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
⊢ P (IsLocalization.map Sᵣ f ⋯)

Tactic:
algebraize [f, IsLocalization.map (S := Rᵣ) Sᵣ f M.le_comap_map,
    (IsLocalization.map (S := Rᵣ) Sᵣ f M.le_comap_map).comp (algebraMap R Rᵣ)]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rᵣ Sᵣ := (IsLocalization.map Sᵣ f ⋯).toAlgebra
algInst✝ : Algebra R Sᵣ := ((IsLocalization.map Sᵣ f ⋯).comp (algebraMap R Rᵣ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rᵣ Sᵣ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sᵣ))
⊢ P (IsLocalization.map Sᵣ f ⋯)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ IsLocalization.mk' R[T;T⁻¹] 1 ⟨X, ⋯⟩ = T (-1)

Tactic:
by
  convert! mk'_one_X_pow 1
  exact (pow_one X).symm

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 α
M : Matrix n n α
v : n → α
h : M *ᵥ v = 0
i : n
hi : v i ∈ nonZeroDivisors α
⊢ M.det * v i = 0

Tactic:
simpa [adjugate_mul, smul_mulVec] using congr((M.adjugate *ᵥ $h) i)

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
inst✝ : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
refine mem_range_scalar_of_commute_single ?_
  intro i j hij
  simpa [transvection, mul_add, add_mul] using! (hM ⟨i, j, hij, 1⟩).eq

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✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ (⅟Aᵀ)ᵀ * A = (Aᵀ * ⅟Aᵀ)ᵀ

Tactic:
transpose_mul,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ (⅟Aᵀ)ᵀ * A = (⅟Aᵀ)ᵀ * Aᵀᵀ
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✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ A * (⅟Aᵀ)ᵀ = (⅟Aᵀ * Aᵀ)ᵀ

Tactic:
transpose_mul,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ A * (⅟Aᵀ)ᵀ = Aᵀᵀ * (⅟Aᵀ)ᵀ
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: R : Type u_6
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.trace = A 0 0 + A 1 1 + A 2 2

Tactic:
rw [← add_zero (A 2 2), add_assoc]
  rfl

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
i : Fin r
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
suffices H :
    ∀ k : ℕ,
      k ≤ r →
        (M * ((listTransvecRow M).take k).prod) (inr unit) (inl i) =
          if k ≤ i then M (inr unit) (inl i) else 0 by
    have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
    rw [← List.take_length (l := listTransvecRow M), A]
    have : ¬r ≤ i := by simp
    simpa only [this, ite_eq_right_iff] using! H r le_rfl

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
⊢ ((reindex e e) M).BlockTriangular b ↔ M.BlockTriangular (b ∘ ⇑e)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case refine_1
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : ((reindex e e) M).BlockTriangular b
⊢ M.BlockTriangular (b ∘ ⇑e)

case refine_2
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : M.BlockTriangular (b ∘ ⇑e)
⊢ ((reindex e e) M).BlockTriangular b
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 α
h : IsUnit A.det
⊢ A.adjugate⁻¹ = h.unit⁻¹ • A

Tactic:
by
  refine inv_eq_left_inv ?_
  rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul]

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

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

Tactic:
cases x <;> cases y <;>
    simp only [Matrix.reindex_apply, toBlock_apply, Equiv.symm_symm, Equiv.sumCompl_apply_inr,
      Equiv.sumCompl_apply_inl, fromBlocks_apply₁₁, fromBlocks_apply₁₂, fromBlocks_apply₂₁,
      fromBlocks_apply₂₂, Matrix.submatrix_apply]

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

Goal state before:
pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ (M.toSquareBlockProp fun i ↦ ¬¬p i).det * (M.toSquareBlockProp fun i ↦ ¬p i).det =
    (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i ↦ ¬p i).det

pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0

Tactic:
· congr 1
    exact equiv_block_det _ fun _ => not_not.symm

Goal state after:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ

Tactic:
have := isUnit_diagonal.mpr h
    cases this.nonempty_invertible
    cases h.nonempty_invertible
    rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_eq]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B 0 D)
⊢ ⅟(fromBlocks A B 0 D) = fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D

Tactic:
let := fromBlocksZero₂₁Invertible A B D

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B 0 D)
this : Invertible (fromBlocks A B 0 D) := A.fromBlocksZero₂₁Invertible B D
⊢ ⅟(fromBlocks A B 0 D) = fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D
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
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
x : Matrix l m R
y : Matrix n p R
⊢ (kroneckerLinearEquiv l m n p R).symm (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y) = x ⊗ₜ[R] y

Tactic:
by simp [LinearEquiv.symm_apply_eq]

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

Goal state before:
pp: case pos.intro.intro
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val✝¹ : Invertible A
val✝ : Invertible D
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

Tactic:
let := fromBlocksZero₂₁Invertible A B D

Goal state after:
case pos.intro.intro
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val✝¹ : Invertible A
val✝ : Invertible D
this : Invertible (fromBlocks A B 0 D) := A.fromBlocksZero₂₁Invertible B D
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: case add
n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A) x) = x
hy : invFun n R A ((toFunAlgHom n R A) y) = y
⊢ invFun n R A ((toFunAlgHom n R A) x + (toFunAlgHom n R A) y) = x + y

Tactic:
conv_rhs => rw [← hx, ← hy, ← invFun_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r ↑hu.unit⁻¹
⊢ IsNilpotent (r * ↑hu.unit⁻¹)

Tactic:
exact (hu.unit⁻¹.isUnit.isNilpotent_mul_unit_of_commute_iff h_comm).mpr hnil

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsUnit x
H : IsNilpotent x
⊢ False

Tactic:
simpa using H.isUnit_add_right_of_commute hx.neg (by simp)

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

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
nilp : IsNilpotent e
⊢ e = 0

Tactic:
obtain ⟨rfl | n, hn⟩ := nilp

Goal state after:
case zero
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : e ^ 0 = 0
⊢ e = 0

case succ
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
n : ℕ
hn : e ^ (n + 1) = 0
⊢ e = 0
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case pos
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
i : ℕ
hi : i ≠ 0
H : i ≤ P₁.natDegree
⊢ IsNilpotent (P₁.coeff i)

Tactic:
simp_rw [P₁, eraseLead_coeff_of_ne _ (ne_of_lt (lt_of_le_of_lt H hdeg₂)), hnil i hi]

Goal state after:
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
hp : ¬p.FG
⊢ p.spanFinrank = 0

Tactic:
refine toNat_eq_zero.2 ?_
  right
  by_contra! h
  exact hp (spanRank_finite_iff_fg.1 h)

Goal state after:
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
⊢ ⊤.spanFinrank = p.spanFinrank

Tactic:
simp [Submodule.spanFinrank]

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

Goal state before:
pp: case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) i j

Tactic:
rw [charmatrix_apply_ne _ _ _ hij, map_neg, expand_C, coeff_neg, coeff_C]

Goal state after:
case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
⊢ (-if m = 0 then (M ^ k) i j else 0) = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) i j
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x✝¹ : A
hx : ∀ n ∈ N, x✝¹ • n ∈ N
A' : Subalgebra R A := ⋯
x y : ↥A'
x✝ : ↥N
⊢ ↑(((DistribSMul.toLinearMap R M (x + y)).restrict ⋯) x✝) =
    ↑(((DistribSMul.toLinearMap R M x).restrict ⋯ + (DistribSMul.toLinearMap R M y).restrict ⋯) x✝)

Tactic:
exact add_smul _ _ _

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

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

Tactic:
← f.map_pow,

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

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

Tactic:
conv_lhs => rw [hf.eq_prod_roots]
  simp [eval_multiset_prod]

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

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

Tactic:
by
  conv_lhs => rw [hf.eq_prod_roots]
  simp [eval_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 : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map (fun ij ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)).prod =
    (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x ↦ eval x g) s).prod

Tactic:
rw [Multiset.prod_map_mul]

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
⊢ (Multiset.map (fun ij ↦ -1) (s ×ˢ g.roots)).prod * (Multiset.map (fun ij ↦ ij.1 - ij.2) (s ×ˢ g.roots)).prod =
    (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x ↦ eval x g) s).prod
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 J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
⊢ eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0

Tactic:
convert! Quotient.eq_zero_iff_mem.mpr hpI

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
⊢ eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    (Quotient.mk I) (eval₂ f r p)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ eval a (map (algebraMap S A) (map (↑(integralClosure R S).val) p)) = 0

Tactic:
← Subalgebra.toSubring_subtype,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ eval a (map (algebraMap S A) (map (integralClosure R S).toSubring.subtype p)) = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ ¬{f} ⊆ ↑I.asIdeal ↔ f ∉ I.asIdeal

Tactic:
Set.singleton_subset_iff

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ f ∉ ↑I.asIdeal ↔ f ∉ I.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus s ∩ zeroLocus {0} = zeroLocus s

Tactic:
zeroLocus_singleton_zero,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus s ∩ Set.univ = zeroLocus s
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case hgt
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
have hA_nont : Nontrivial A := IsDomain.toNontrivial

Goal state after:
case hgt
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥