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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    Function.Exact ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
      ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G)
⊢ Function.Exact ⇑F ⇑G

Tactic:
by
  simp only [LinearMap.exact_iff] at H ⊢
  apply Submodule.eq_of_isLocalized₀_span s spn Nₚ g
  intro r
  rw [← LinearMap.range_localizedMap_eq_localized₀_range _ (f r) (g r) F]
  rw [← LinearMap.ker_localizedMap_eq_localized₀_ker (.powers r.1) (g r) (h r) G]
  have := SetLike.ext_iff.mp <| H r
  ext x
  simp only [mem_range, mem_ker] at this ⊢
  exact this x

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ Nonempty (OreSet S) ↔ ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

Tactic:
constructor
  · exact fun ⟨_⟩ ↦ fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩
  · intro H
    choose r' s' h using H
    exact ⟨oreSetOfNoZeroDivisors r' s' h⟩

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

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ P f ∧ Q f

Tactic:
exact ⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩

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

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
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] f ↦ P f ∧ Q f) (Localization.awayMap f ↑r)
⊢ P f ∧ Q f

Tactic:
exact ⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩

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

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

Tactic:
nsmul_eq_mul

Goal state after:
R : Type u_1
inst✝ : Semiring R
m : ℤ
n : ℕ
⊢ AddMonoidAlgebra.single (↑n * m) 1 = AddMonoidAlgebra.single (↑n * m) 1
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
apply le_antisymm <;>
    rw [Module.rank_def, lift_iSup bddAbove_of_small]

Goal state after:
case inr.a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ⨆ i, Cardinal.lift.{uM, uN} #↑↑i ≤ Cardinal.lift.{uN, uM} (Module.rank R M)

case a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ⨆ i, Cardinal.lift.{uN, uM} #↑↑i ≤ Cardinal.lift.{uM, uN} (Module.rank R N)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (p q : R[T;T⁻¹]),
    (∃ n f', toLaurent f' = p * T ↑n) → (∃ n f', toLaurent f' = q * T ↑n) → ∃ n f', toLaurent f' = (p + q) * T ↑n

Tactic:
rintro f g ⟨m, fn, hf⟩ ⟨n, gn, hg⟩
    refine ⟨m + n, fn * X ^ n + gn * X ^ m, ?_⟩
    simp only [hf, hg, add_mul, add_comm (n : ℤ), map_add, map_mul, Polynomial.toLaurent_X_pow,
      mul_T_assoc, Int.natCast_add]

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

Tactic:
by rw [← Matrix.mul_assoc, mul_invOf_self, Matrix.one_mul]

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

Goal state before:
pp: case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
hn' : n < (listTransvecCol M).length
⊢ ((List.drop n (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
List.drop_eq_getElem_cons hn'

Goal state after:
case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
hn' : n < (listTransvecCol M).length
⊢ (((listTransvecCol M)[n] :: List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case of_succ
𝕜 : 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⟩
⊢ ((List.drop n (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
List.drop_eq_getElem_cons hn'

Goal state after:
case of_succ
𝕜 : 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⟩
⊢ (((listTransvecCol M)[n] :: List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
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 α)ˣ
⊢ ↑A⁻¹ = (↑A)⁻¹

Tactic:
let := A.invertible

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : (Matrix n n α)ˣ
this : Invertible ↑A := A.invertible
⊢ ↑A⁻¹ = (↑A)⁻¹
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case refine_1
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : Function.Injective fun v ↦ v ᵥ* A
⊢ IsUnit A

pp: case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : IsUnit A
⊢ Function.Injective fun v ↦ v ᵥ* A

Tactic:
· rw [← vecMul_surjective_iff_isUnit]
    exact LinearMap.surjective_of_injective (f := A.vecMulLinear) h

Goal state after:
case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : IsUnit A
⊢ Function.Injective fun v ↦ v ᵥ* A
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
⊢ (M.toSquareBlockProp fun i ↦ b i = k).det * (M.toSquareBlockProp fun i ↦ ¬b i = k).det =
    ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
have : univ.image b = insert k ((univ.image b).erase k) := by
      rw [insert_erase]
      apply max'_mem

Goal state after:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
⊢ (M.toSquareBlockProp fun i ↦ b i = k).det * (M.toSquareBlockProp fun i ↦ ¬b i = k).det =
    ∏ a ∈ image b univ, (M.toSquareBlock b a).det
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
⊢ ∀ (i : m), b i = k → ∀ (j : m), ¬b j = k → M i j = 0

Tactic:
· intro i hi j hj
    apply hM
    rw [hi]
    apply lt_of_le_of_ne _ hj
    exact Finset.le_max' (univ.image b) _ (mem_image_of_mem _ (mem_univ _))

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

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
⊢ (M⁻¹ * M).toBlock p p = 1

Tactic:
inv_mul_of_invertible M,

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
⊢ toBlock 1 p p = 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
⊢ (M⁻¹ * M).toBlock q p = 0

Tactic:
inv_mul_of_invertible M,

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
⊢ toBlock 1 q p = 0
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
p : a = b
H : a' + b = b' + a
⊢ a' = b'

Tactic:
by
  rw [p] at H
  exact add_right_cancel H

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
⊢ IsNilpotent P

Tactic:
← sum_monomial_eq P

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
⊢ IsNilpotent (P.sum fun n a ↦ (monomial n) a)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent ((p * X).coeff i)

Tactic:
rcases i with - | i
    · simp
    simpa using hnp (isNilpotent_mul_X_iff.mp hpX) i

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
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ x, 1 = #univ

Tactic:
sum_const,

Goal state after:
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
⊢ #univ • 1 = #univ
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case h
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
⊢ ∏ i, (X - C (M i i)).leadingCoeff ≠ 0

Tactic:
(monic_X_sub_C _).leadingCoeff

Goal state after:
case h
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
⊢ ∏ x, 1 ≠ 0
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
inst✝ : Nonempty n
M : Matrix n n R
⊢ M.trace = - -∑ i, M i i

Tactic:
neg_neg,

Goal state after:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
M : Matrix n n R
⊢ M.trace = ∑ i, M i i
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ (-1) ^ ↑i * (eval 0 (derivative 0) + M 0 i) * eval 0 0 = 0

pp: case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ ∀ (i_1 : Fin (n + 1)), submatrix 1 Fin.succ i.succAbove i_1 0 = 0

Tactic:
eval_zero,

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

case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ ∀ (i_1 : Fin (n + 1)), submatrix 1 Fin.succ i.succAbove i_1 0 = 0
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
h : f r ∈ Set.range ⇑f
⊢ (mapRingHom f) ((monomial n) r) = (monomial n) (f r)

Tactic:
simp only [coe_mapRingHom, map_monomial]

Goal state after:
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
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : i ∈ range 3
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i

pp: case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : i ∉ range 3
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i

Tactic:
· fin_cases hi
    · simp [det_eq_sign_charpoly_coeff, hn]
    · simp [trace_eq_neg_charpoly_coeff, hn]
    · simpa [leadingCoeff, charpoly_natDegree_eq_dim, hn, coeff_X] using
        M.charpoly_monic.leadingCoeff

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : i ∉ range 3
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i
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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det =
    C A⁻¹.det * ((-1) ^ Fintype.card n * (1 - (scalar n) X * C.mapMatrix A).det)

Tactic:
by
    rw [← neg_sub, det_neg, det_one_sub_mul_comm]

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 : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - (X • M.map ⇑C) ^ k

Tactic:
rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) ↑((i - l).choose k * i.choose l) =
    (monomial (i - (k + l))) ((k + l).choose k • ↑(i.choose (k + l)))

Tactic:
nsmul_eq_mul

Goal state after:
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) ↑((i - l).choose k * i.choose l) =
    (monomial (i - (k + l))) (↑((k + l).choose k) * ↑(i.choose (k + l)))
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
hn : n ≤ (p + q).natDegree
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
add_comm (_ - n),

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
hn : n ≤ (p + q).natDegree
⊢ (p.coeff n + q.coeff n) * r ^ (p.natDegree - (p + q).natDegree + ((p + q).natDegree - n)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)
Module: Mathlib.Algebra.Polynomial.Splits

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

Tactic:
simp [leadingCoeff_eq_zero.mp hf₀]

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
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
h'' : p = 0
⊢ False

Tactic:
rw [h'', natDegree_zero] at h'

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ 0
h'' : p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hg : g.Splits
hg₀ : g ≠ 0
hfg : f ∣ g
⊢ f.Splits

Tactic:
obtain ⟨g, rfl⟩ := hfg

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
g : R[X]
hg : (f * g).Splits
hg₀ : f * g ≠ 0
⊢ f.Splits
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✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
inst✝ : IsScalarTower R A B
f : R[X]
hf : (map (algebraMap R A) f).Splits
⊢ Multiset.map (⇑(algebraMap A B)) (f.aroots A) = f.aroots B

Tactic:
by
  rw [← aroots_map B A, aroots, aroots,
    hf.roots_map_of_injective (FaithfulSMul.algebraMap_injective A B)]

Goal state after:
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
⊢ f.Splits

Tactic:
by
  have h : (f /ₘ (X - C x)).natDegree = 1 := by
    rw [natDegree_divByMonic f (monic_X_sub_C x), h₁, natDegree_X_sub_C]
  rw [← mul_divByMonic_eq_iff_isRoot.mpr h₂, splits_mul (X_sub_C_ne_zero x) (by aesop)]
  exact ⟨Splits.X_sub_C x, Splits.of_natDegree_eq_one h⟩

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
i : ℕ
hi : i ∈ q.support
⊢ (q.coeff i).natDegree ≤ N

pp: case neg
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
i : ℕ
hi : i ∉ q.support
⊢ (q.coeff i).natDegree ≤ N

Tactic:
· exact Finset.le_sup (f := (q.coeff · |>.natDegree)) hi

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
i : ℕ
hi : i ∉ q.support
⊢ (q.coeff i).natDegree ≤ N
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : x ∈ zeroLocus s
⊢ False

Tactic:
mem_zeroLocus

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ False
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsLocalRing R
inst✝⁴ : CommRing S
inst✝³ : IsLocalRing S
inst✝² : CommRing T
inst✝¹ : IsLocalRing T
f : R →+* S
inst✝ : IsLocalHom f
a : R
ha : a ∈ maximalIdeal R
⊢ f a ∈ maximalIdeal S

Tactic:
exact map_nonunit f a ha

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
H : ∀ (P : Ideal S), P.IsPrime → ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
I : Ideal S
hI : I ≠ ⊤
s : S
M : Ideal S
hM : M.IsMaximal
hIM : I ≤ M
⊢ ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

Tactic:
obtain ⟨x, r, c, hc, hr, e⟩ := H M hM.isPrime s

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
H : ∀ (P : Ideal S), P.IsPrime → ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
I : Ideal S
hI : I ≠ ⊤
s : S
M : Ideal S
hM : M.IsMaximal
hIM : I ≤ M
x r : R
c : S
hc : c ∉ M
hr : f r ∉ M
e : c * f r * s = c * f x
⊢ ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x