mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ ∀ b ∈ p.coeff.support, b ≠ a → (Finsupp.single b (p.coeff b)) a = 0

Tactic:
intro b _ hb

Goal state after:
case h₀
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a b : ℤ
a✝ : b ∈ p.coeff.support
hb : b ≠ a
⊢ (Finsupp.single b (p.coeff b)) a = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case map_smul
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
c✝ : α
x✝ : n → α
i : n
⊢ A.cramerMap (c✝ • x✝) i = (c✝ • A.cramerMap x✝) i

Tactic:
apply (cramerMap_is_linear A i).2

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ motive (toLaurent f' * T (-↑n))

Tactic:
exact mul_T ..

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
a : R
⊢ (C a).degree = if a = 0 then ⊥ else 0

Tactic:
by
  split_ifs with h <;> simp only [h, map_zero, degree_zero, degree_C, Ne, not_false_iff]

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 α
A : Matrix n n α
b : n → α
⊢ A *ᵥ A.adjugate *ᵥ b = A.det • b

Tactic:
mulVec_mulVec,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ (A * A.adjugate) *ᵥ b = A.det • b
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
k : ℕ
hk : k ≤ r
⊢ ((List.drop k (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
induction hk using Nat.decreasingInduction with

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) * (A + U * C * V) = 1

Tactic:
calc
    (⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V)
    _ = ⅟A*A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*A + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V := by
      simp_rw [add_sub_assoc, _root_.mul_add, _root_.sub_mul, Matrix.mul_assoc]
    _ = (1 + ⅟A*U*C*V) - (⅟A*U*⅟(⅟C + V*⅟A*U)*V + ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V) := by
      rw [invOf_mul_self, Matrix.invOf_mul_cancel_right]
      abel
    _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(V + V*⅟A*U*C*V) := by
      rw [sub_right_inj, Matrix.mul_add]
      simp_rw [Matrix.mul_assoc]
    _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(⅟C + V*⅟A*U)*C*V := by
      simp only [Matrix.mul_add, Matrix.add_mul, ← Matrix.mul_assoc,
        Matrix.invOf_mul_cancel_right]
    _ = 1 := by
      rw [Matrix.invOf_mul_cancel_right]
      abel

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
k : ℕ
hk : k ≤ r
⊢ ((List.drop k (listTransvecCol M)).prod * M) (inl i) (inr ()) = if k ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
induction hk using Nat.decreasingInduction with

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

Goal state before:
pp: α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
A : Matrix l m α
b : ℕ
⊢ (blockDiagonal fun i ↦ A <• ↑b) = blockDiagonal fun x ↦ b •> A

Tactic:
by
    congr! 2
    ext
    simp [(Nat.cast_commute b _).eq]

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 α
A : Matrix n n α
inst✝ : Invertible A
B C : Matrix n m α
h : A⁻¹ * B = C
⊢ B = A * C

Tactic:
rw [← h, mul_inv_cancel_left_of_invertible]

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A.det * B.det)⁻¹ʳ • (B.adjugate * A.adjugate) = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)

Tactic:
Ring.mul_inverse_rev

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate) = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
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 α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible A
⊢ A.submatrix ⇑e₁ ⇑e₂ * (⅟A).submatrix ⇑e₂ ⇑e₁ = 1

Tactic:
Matrix.submatrix_mul_equiv,

Goal state after:
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 α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible A
⊢ (A * ⅟A).submatrix ⇑e₁ ⇑e₁ = 1
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 α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
this : A = (A.submatrix ⇑e₁ ⇑e₂).submatrix ⇑e₁.symm ⇑e₂.symm
⊢ (A.submatrix ⇑e₁ ⇑e₂).submatrix ⇑e₁.symm ⇑e₂.symm * (⅟(A.submatrix ⇑e₁ ⇑e₂)).submatrix ⇑e₂.symm ⇑e₁.symm = 1

Tactic:
Matrix.submatrix_mul_equiv,

Goal state after:
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 α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
this : A = (A.submatrix ⇑e₁ ⇑e₂).submatrix ⇑e₁.symm ⇑e₂.symm
⊢ (A.submatrix ⇑e₁ ⇑e₂ * ⅟(A.submatrix ⇑e₁ ⇑e₂)).submatrix ⇑e₁.symm ⇑e₁.symm = 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✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : M.BlockTriangular b
⊢ M.det = ∏ k, (M.toSquareBlock b k).det

Tactic:
by
  refine h.det.trans (prod_subset (subset_univ _) fun a _ ha => ?_)
  have : IsEmpty { i // b i = a } := ⟨fun i => ha <| mem_image.2 ⟨i, mem_univ _, i.2⟩⟩
  exact det_isEmpty

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 : α
⊢ ((M⁻¹.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) * M.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) = 1

Tactic:
let p i := b i < k
  have h_sum :
    M⁻¹.toBlock p p * M.toBlock p p +
        (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p =
      1 := by
    rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
  have h_zero : M.toBlock (fun i => ¬p i) p = 0 := by
    ext i j
    simpa using hM (lt_of_lt_of_le j.2 (le_of_not_gt i.2))
  simpa [h_zero] using h_sum

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
⊢ (matPolyEquiv.symm p i j).coeff k = p.coeff k i j

Tactic:
have t : p = matPolyEquiv (matPolyEquiv.symm p) := by simp

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = matPolyEquiv (matPolyEquiv.symm p)
⊢ (matPolyEquiv.symm p i j).coeff k = p.coeff k i j
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.map ⇑f).charpoly = Polynomial.map f M.charpoly

Tactic:
by
  rw [charpoly, charmatrix_map, ← Polynomial.coe_mapRingHom, charpoly, RingHom.map_det,
    RingHom.mapMatrix_apply]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u v : n → R
⊢ (vecMulVec u v).charpoly = X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)

Tactic:
by
  cases isEmpty_or_nonempty n
  · simp
  · have h : 1 ≤ Fintype.card n := NeZero.one_le
    rw [vecMulVec_eq (ι := Unit), charpoly_mul_comm_of_le (n := Unit) _ _ h, charpoly, charmatrix]
    simp [-Matrix.map_mul, mul_sub, ← pow_succ, h, dotProduct_comm, smul_eq_C_mul]

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) * (x ^ (n + 1) + (↑n + 1) * x ^ n * y + z * y ^ 2) =
    x ^ (n + 2) + (↑n + 2) * x ^ (n + 1) * y + (x * z + (↑n + 1) * x ^ n + z * y) * y ^ 2

Tactic:
ring!

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

Goal state before:
pp: m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

Tactic:
nth_rewrite 1 [← Matrix.mul_one A]
  rwa [← Matrix.mul_nonsing_inv_cancel_left A (replicateCol ι u * replicateRow ι v),
    ← Matrix.mul_add, det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]

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

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : MulActionWithZero R S
inst✝¹ : SMulCommClass R S S
inst✝ : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
⊢ t ^ k • a ^ k = 0

Tactic:
ha,

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : MulActionWithZero R S
inst✝¹ : SMulCommClass R S S
inst✝ : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
⊢ t ^ k • 0 = 0
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j✝ : ι
s : Finset ι
hj✝ : j✝ ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j✝ s, IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ insert j✝ s → j ∈ insert j✝ s → Commute (f i) (f j)
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ j ∈ insert j✝ s

Tactic:
simp [hj]

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
inst✝ : Subsingleton R
p : Submodule R M
this : Subsingleton M
⊢ p.spanFinrank = 0

Tactic:
simp [Submodule.eq_bot_of_subsingleton]

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
g : S →+* T
hg : Function.Injective ⇑g
x : S
hx : (g.comp f).IsIntegralElem (g x)
⊢ f.IsIntegralElem x

Tactic:
by
  obtain ⟨p, hp, hx⟩ := hx
  exact ⟨p, hp, hg <| by simp [Polynomial.hom_eval₂, hx]⟩

Goal state after:
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
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i))).Monic
⊢ M.charpoly.Monic

Tactic:
← sub_add_cancel (∏ i : n, (X - C (M i i))) M.charpoly

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
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).Monic
⊢ M.charpoly.Monic
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hl : (monomial n) 0 ∈ lifts f
⊢ ∃ q, map f q = (monomial n) 0 ∧ q.degree = ((monomial n) 0).degree

Tactic:
exact ⟨0, by simp⟩

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

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

Tactic:
exact ⟨q, hq, congrArg Finset.max hq'⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
by_cases hnik : n = i + k

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0

case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
⊢ (hasseDeriv k) ((monomial n) r) = (monomial (n - k)) (↑(n.choose k) * r)

Tactic:
by
  ext i
  simp only [hasseDeriv_coeff, coeff_monomial]
  by_cases hnik : n = i + k
  · grind
  · rw [if_neg hnik, mul_zero]
    by_cases! hkn : k ≤ n
    · rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik
      rw [if_neg hnik]
    · rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, zero_mul, ite_self]

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

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

Tactic:
by
  by_cases hf : f = 0
  · rw [hf, map_zero, coeff_natDegree]
  · rw [taylor_coeff, hasseDeriv_natDegree_eq_C, eval_C]

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

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

Tactic:
rw [hp, zero_scaleRoots]

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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ (algebraMap R A) r ^ p.natDegree * (aeval a) p = 0

pp: case hsa
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ Commute ((algebraMap R A) r) a

pp: case hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ ∀ (s₁ s₂ : R), Commute ((algebraMap R A) s₁) ((algebraMap R A) s₂)

Tactic:
ha,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ (algebraMap R A) r ^ p.natDegree * 0 = 0

case hsa
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ Commute ((algebraMap R A) r) a

case hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ ∀ (s₁ s₂ : R), Commute ((algebraMap R A) s₁) ((algebraMap R A) s₂)
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: S : Type v
inst✝ : CommSemiring S
p : S[X]
⊢ p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff

Tactic:
rw [Algebra.smul_def, algebraMap_eq, mul_comm, integralNormalization_mul_C_leadingCoeff]

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

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

Tactic:
refine mt (by simp +contextual [pow_succ]) hp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: case C
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
a : R
⊢ (aeval fun x ↦ 1 ⊗ₜ[R] f x) (C a) = 1 ⊗ₜ[R] (aeval f) (C a)

Tactic:
simp only [algHom_C, Algebra.TensorProduct.algebraMap_apply]
    rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : R →+* S
hi✝ : Function.Injective ⇑i
hf : (map i f).Splits
hi : ∀ a ∈ (map i f).roots, a ∈ i.range
⊢ f.Splits

Tactic:
choose j hj using hi
  rw [splits_iff_exists_multiset]
  refine ⟨(f.map i).roots.pmap j fun _ ↦ id, map_injective i hi ?_⟩
  conv_lhs => rw [hf.eq_prod_roots, leadingCoeff_map_of_injective hi]
  simp [Multiset.pmap_eq_map, hj, Multiset.map_pmap, Polynomial.map_multiset_prod]

Goal state after:
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
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral R M.det

Tactic:
rw [Matrix.det_apply]
  exact IsIntegral.sum _ fun σ _hσ ↦ (IsIntegral.prod _ fun i _hi => h _ _).zsmul _

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

Goal state before:
pp: 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
R' : Type u_3
inst✝³ : CommRing R'
inst✝² : Algebra R R'
inst✝¹ : Algebra S R'
inst✝ : IsScalarTower R S R'
p : S[X]
x : R'
hx : (aeval x) p = 0
⊢ eval₂ (algebraMap R R') x (integerNormalization M p) = 0

Tactic:
IsScalarTower.algebraMap_eq R S R',

Goal state after:
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
R' : Type u_3
inst✝³ : CommRing R'
inst✝² : Algebra R R'
inst✝¹ : Algebra S R'
inst✝ : IsScalarTower R S R'
p : S[X]
x : R'
hx : (aeval x) p = 0
⊢ eval₂ ((algebraMap S R').comp (algebraMap R S)) x (integerNormalization M p) = 0
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ Nontrivial N → Nontrivial (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N

Tactic:
simp only [← not_subsingleton_iff_nontrivial]; tauto

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ Nontrivial N → Nontrivial (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N

Tactic:
simp only [← not_subsingleton_iff_nontrivial]; tauto

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case zero
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = 0

Tactic:
exact ⟨0, by simp⟩

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
inst✝ : P.IsMaximal
⊢ (Ideal.under A P).IsMaximal

Tactic:
exact isMaximal_comap_of_isIntegral_of_isMaximal P

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

Goal state before:
pp: 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
s : S
a : A
ha : IsAlgebraic R a
inst✝ : FaithfulSMul R S
⊢ IsAlgebraic S (s ⊗ₜ[R] a)

Tactic:
by
  rw [← mul_one s, ← smul_eq_mul, ← TensorProduct.smul_tmul']
  have ⟨p, h, eval0⟩ := ha
  refine .smul ⟨p.map (algebraMap R S),
    (Polynomial.map_ne_zero_iff <| FaithfulSMul.algebraMap_injective ..).mpr h, ?_⟩ _
  rw [← Algebra.TensorProduct.includeRight_apply, ← AlgHom.coe_toRingHom (A := A),
    ← map_aeval_eq_aeval_map (by ext; simp), eval0, map_zero]

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

Goal state before:
pp: 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 S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
⊢ s ⊆ ↑(Subalgebra.restrictScalars R Rts)

Tactic:
by apply subset_adjoin

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
⊢ FaithfullyFlat R M

Tactic:
by
  rw [iff_zero_iff_lTensor_zero]
  refine ⟨Module.Flat.trans R S M, @fun N _ _ N' _ _ f => ⟨fun aux => ?_, fun eq => eq ▸ by simp⟩⟩
  rw [zero_iff_lTensor_zero (R := R) (M := S) f,
    show f.lTensor S = (AlgebraTensorModule.map (A := S) LinearMap.id f).restrictScalars R by aesop,
    show (0 :  S ⊗[R] N →ₗ[R] S ⊗[R] N') = (0 : S ⊗[R] N →ₗ[S] S ⊗[R] N').restrictScalars R by rfl,
    restrictScalars_inj, zero_iff_lTensor_zero (R := S) (M := M)]
  ext m n
  apply_fun AlgebraTensorModule.cancelBaseChange R S S M N' using LinearEquiv.injective _
  simpa using congr($aux (m ⊗ₜ[R] n))

Goal state after: