mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
r : R
x : N
⊢ x ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x} →
    r • x ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x}

Tactic:
rintro ⟨m, hm, s, hx⟩

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
r : R
x : N
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
⊢ r • x ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x}
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
A : Matrix ι ι R
⊢ IsNilpotent (toLin' A) ↔ IsNilpotent A

Tactic:
have : A.toLin'.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι) = A := LinearMap.toMatrix'_toLin' A

Goal state after:
R : Type u_1
ι : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
A : Matrix ι ι R
this : (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A) = A
⊢ IsNilpotent (toLin' A) ↔ IsNilpotent A
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
n : ℕ
x : R
s✝ : ↥M
s : R
hs : s ∈ M
h : s * x ^ n ∈ I
⊢ (s * x) ^ (n + 1) ∈ I

Tactic:
convert! I.mul_mem_left (s ^ n * x) h; ring

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case hl
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
a : ↥m ⊗[R] N
b : M ⊗[R] ↥n
f : ↥m ⊗[R] N →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n) := map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
g : M ⊗[R] ↥n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n) := map m.mkQ n.mkQ ∘ₗ map LinearMap.id n.subtype
x : ↥m
y : N
⊢ ((AlgebraTensorModule.curry (f.coprod g ∘ₗ LinearMap.inl R (↥m ⊗[R] N) (M ⊗[R] ↥n))) x) y =
    ((AlgebraTensorModule.curry (0 ∘ₗ LinearMap.inl R (↥m ⊗[R] N) (M ⊗[R] ↥n))) x) y

Tactic:
simp [f, Submodule.Quotient.mk_eq_zero _ |>.2 x.2]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
p : Ideal R
inst✝⁴ : p.IsPrime
Rₚ : Type u_4
inst✝³ : CommSemiring Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
⊢ maximalIdeal Rₚ = Ideal.map (algebraMap R Rₚ) (under R (maximalIdeal Rₚ))

Tactic:
map_under p.primeCompl

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
p : Ideal R
inst✝⁴ : p.IsPrime
Rₚ : Type u_4
inst✝³ : CommSemiring Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
⊢ maximalIdeal Rₚ = maximalIdeal Rₚ
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case refine_2
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
n : ℕ
a : R
b : ↥p.primeCompl
hx : mk' Rₚ a b ∈ maximalIdeal Rₚ ^ n
⊢ (liftAlgHom ⋯) (mk' Rₚ a b) = 0

Tactic:
IsLocalization.mk'_mem_iff,

Goal state after:
case refine_2
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
n : ℕ
a : R
b : ↥p.primeCompl
hx : (algebraMap R Rₚ) a ∈ maximalIdeal Rₚ ^ n
⊢ (liftAlgHom ⋯) (mk' Rₚ a b) = 0
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A)ᵀ = (comp m m n n α) A ↔ Aᵀ = A.map fun x ↦ xᵀ

Tactic:
transpose_comp,

Goal state after:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
⊢ (comp m m n n α) (Aᵀ.map fun x ↦ xᵀ) = (comp m m n n α) A ↔ Aᵀ = A.map fun x ↦ xᵀ
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case mul_T
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
⊢ Q (toLaurent f * T (-↑n))

Tactic:
induction n with

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (C a * T n).coeff.support = {n}

Tactic:
by
  rw [← single_eq_C_mul_T]
  exact support_single _ a0

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
⊢ f = 0

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
n : ℤ
⊢ f.coeff n = (AddMonoidAlgebra.coeff 0) n
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (C r * p).smeval x = r • p.smeval x
hq : (C r * q).smeval x = r • q.smeval x
⊢ (C r * (p + q)).smeval x = r • (p + q).smeval x

Tactic:
rw [mul_add, smeval_add, smeval_add, smul_add, hp, hq]

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

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : AddCommMonoidWithOne R
⊢ ∑ i, diag 1 i = ↑(Fintype.card n)

Tactic:
diag_one,

Goal state after:
n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : AddCommMonoidWithOne R
⊢ ∑ x, 1 x = ↑(Fintype.card n)
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_6
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
A B : Matrix m n R
⊢ A = B ↔ ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace

Tactic:
by
  refine ⟨fun h x => h ▸ rfl, fun h => ?_⟩
  ext i j
  classical
  simpa [trace_mul_single] using h (single j i (1 : R))

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) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (List.take (listTransvecRow M).length (listTransvecRow M)).prod) i (inr ()) = M i (inr ())

Tactic:
A

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (List.take r (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
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
H : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
A : (listTransvecRow M).length = r
⊢ (M * (List.take (listTransvecRow M).length (listTransvecRow M)).prod) (inr ()) (inl i) = 0

Tactic:
A

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
H : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
A : (listTransvecRow M).length = r
⊢ (M * (List.take r (listTransvecRow M)).prod) (inr ()) (inl i) = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
⊢ A.adjugate.adjugate = A.det ^ (n✝ + 1 + 1 - 2) • A

Tactic:
rw [← h_card]

Goal state after:
case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
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
⊢ q ⊓ p ≤ ⊥

Tactic:
exact fun i h => h.1 h.2

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
m : Type u_3
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M : Matrix m m R
t : R
⊢ (evalRingHom t) M.charmatrix.det = ((scalar m) t - M).det

Tactic:
RingHom.map_det,

Goal state after:
R : Type u_1
inst✝² : CommRing R
m : Type u_3
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M : Matrix m m R
t : R
⊢ ((evalRingHom t).mapMatrix M.charmatrix).det = ((scalar m) t - M).det
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
⊢ (M.charmatrix.map ⇑(mapRingHom f)).det = (mapRingHom f) M.charmatrix.det

Tactic:
RingHom.map_det,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
⊢ (M.charmatrix.map ⇑(mapRingHom f)).det = ((mapRingHom f).mapMatrix M.charmatrix).det
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case succ
𝕜 : Type u_3
inst✝² : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
have e : n ≃ Fin r ⊕ Unit := by
      refine Fintype.equivOfCardEq ?_
      rw [hn]
      rw [@Fintype.card_sum (Fin r) Unit _ _]
      simp

Goal state after:
case succ
𝕜 : Type u_3
inst✝² : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
e : n ≃ Fin r ⊕ Unit
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case htransvec
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := ⋯
⊢ ∀ (t : TransvectionStruct n 𝕜), Q t.toMatrix

pp: case hmul
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := ⋯
⊢ ∀ (A B : Matrix n n 𝕜), Q A → Q B → Q (A * B)

Tactic:
· intro t
      exact ⟨by simp, htransvec t⟩

Goal state after:
case hmul
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := ⋯
⊢ ∀ (A B : Matrix n n 𝕜), Q A → Q B → Q (A * B)
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x y : R
hy : IsRadical y
h0 : y ≠ 0
hxy : x ∣ y
⊢ ∀ (x_1 : R), x ∣ x_1 ^ 2 → x ∣ x_1

Tactic:
obtain ⟨z, rfl⟩ := hxy

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
⊢ ∀ (x_1 : R), x ∣ x_1 ^ 2 → x ∣ x_1
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent P → IsNilpotent (X * P)

Tactic:
rintro ⟨k, hk⟩
    exact ⟨k, by simp [(commute_X P).mul_pow, hk]⟩

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
⊢ I = ⊥ → I.spanRank = 0

Tactic:
rintro rfl; rw [spanRank]
    exact Cardinal.iInf_eq_zero_iff.mpr (Or.inr ⟨⟨∅, by simp⟩, by simp⟩)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin n) R
⊢ eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace

Tactic:
induction n with

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
⊢ (evalRingHom 0) (1 - X • M.map ⇑C).det = 1

Tactic:
RingHom.map_det,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ((evalRingHom 0).mapMatrix (1 - X • M.map ⇑C)).det = 1
Module: Mathlib.Algebra.Polynomial.HasseDeriv

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

Tactic:
rw [← C_1, hasseDeriv_C k _ hk]

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

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

Tactic:
coeff_scaleRoots_natDegree

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this✝ : p.coeff p.natDegree ≠ 0
this : p.leadingCoeff = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

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

Tactic:
coeff_scaleRoots_natDegree

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ p.leadingCoeff ≠ 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).natDegree = p.natDegree

Tactic:
simp only [natDegree, degree_scaleRoots]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
⊢ (p.scaleRoots r).coeff p.natDegree = p.leadingCoeff

Tactic:
coeff_scaleRoots_natDegree

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
⊢ p.leadingCoeff = p.leadingCoeff
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.scaleRoots 0 = p.leadingCoeff • X ^ p.natDegree

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.scaleRoots 0).coeff n = (p.leadingCoeff • X ^ p.natDegree).coeff n
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ (r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r).coeff n =
    (p.scaleRoots r * q.scaleRoots r).coeff n
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
by_cases hp : p = 0; · simp [hp]
  by_cases hq : q = 0; · simp [hq]
  apply mul_scaleRoots'
  simp only [ne_eq, mul_eq_zero, leadingCoeff_eq_zero, hp, hq, or_self, not_false_eq_true]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
hp : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
induction n with

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
⊢ r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r = p.scaleRoots r + q.scaleRoots r

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r).coeff n = (p.scaleRoots r + q.scaleRoots r).coeff n
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (p.scaleRoots r).Splits

Tactic:
rw [hm, mul_scaleRoots', scaleRoots_C]

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod.scaleRoots r).Splits

case inr.inr.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (C p.leadingCoeff).leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod.leadingCoeff ≠ 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr.cons
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH : ((Multiset.map (fun x ↦ X + C x) s).prod.scaleRoots r).Splits
⊢ ((X + C (a * r)) * (Multiset.map (fun x ↦ X + C x) s).prod.scaleRoots r).Splits

Tactic:
exact .mul (.X_add_C _) IH

Goal state after:
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
⊢ map T.subtype (p.toSubring T hp) = p

Tactic:
ext n

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
⊢ ((Polynomial.taylor r) p).Splits

Tactic:
have (i : _) : (X + C r + C i).Splits := by simpa [add_assoc] using Splits.X_add_C (r + i)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
this : ∀ (i : R), (X + C r + C i).Splits
⊢ ((Polynomial.taylor r) p).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case mem
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
p : R[X]
hp : p ∈ {x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x}
hφ : map φ p ≠ 0
⊢ (map φ p).roots = Multiset.map (⇑φ) p.roots

Tactic:
obtain (⟨r, rfl⟩ | ⟨a, rfl⟩) := hp

Goal state after:
case mem.inl
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
r : R
hφ : map φ (C r) ≠ 0
⊢ (map φ (C r)).roots = Multiset.map (⇑φ) (C r).roots

case mem.inr
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
a : R
hφ : map φ (X + C a) ≠ 0
⊢ (map φ (X + C a)).roots = Multiset.map (⇑φ) (X + C a).roots
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
⊢ x ∈ A

Tactic:
by
  rw [← inv_inv x]; exact int.inv.inv_mem inv_mem

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
x y : B
hx : IsIntegral R x
hy : IsIntegral R y
⊢ (algebraMap A B) (mk' A (x * y) ⋯) = (algebraMap A B) (mk' A x hx * mk' A y hy)

Tactic:
by simp only [algebraMap_mk', map_mul]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap ((Quotient.mk I).comp (algebraMap R S)) Q' =
    comap (Quotient.mk (comap (algebraMap R S) I)) (comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q')

pp: case refine_2
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap (Quotient.mk (comap (algebraMap R S) I)) (map (Quotient.mk (comap (algebraMap R S) I)) P) = P

Tactic:
· rw [comap_comap]
    exact congr_arg (comap · Q') (RingHom.ext fun r => rfl)

Goal state after:
case refine_2
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap (Quotient.mk (comap (algebraMap R S) I)) (map (Quotient.mk (comap (algebraMap R S) I)) P) = P