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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[T;T⁻¹]
⊢ r • f = C r * f

Tactic:
by
  induction f using LaurentPolynomial.induction_on' with
  | add _ _ hp hq =>
    rw [smul_add, mul_add, hp, hq]
  | C_mul_T n s =>
    rw [← mul_assoc, ← smul_mul_assoc, mul_left_inj_of_invertible, ← map_mul, ← single_eq_C,
      AddMonoidAlgebra.smul_single']
    rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ trunc (C r * T n) = if 0 ≤ n then (monomial n.toNat) r else 0

Tactic:
apply (toFinsuppIso R).injective
  simp only [← single_eq_C_mul_T, trunc, AddMonoidHom.coe_comp, Function.comp_apply,
    RingHom.toAddMonoidHom_eq_coe, RingEquiv.toRingHom_eq_coe,
    AddMonoidHom.coe_coe, RingHom.coe_coe, RingEquiv.apply_symm_apply, toFinsuppIso_apply]
  split_ifs with hn
  · lift n to ℕ using hn
    simp [toFinsupp_monomial, -single_eq_C_mul_T]
  · ext a
    have : a ≠ n := by lia
    simp [-single_eq_C_mul_T, single_eq_of_ne this]

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 α
inst✝ : Nontrivial n
i j : n
⊢ (cramer 0 ∘ₗ LinearMap.single α (fun i ↦ α) i) 1 j = (0 ∘ₗ LinearMap.single α (fun i ↦ α) i) 1 j

Tactic:
obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j

Goal state after:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ (cramer 0 ∘ₗ LinearMap.single α (fun i ↦ α) i) 1 j = (0 ∘ₗ LinearMap.single α (fun i ↦ α) i) 1 j
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case mul_T
R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f✝ : R →+* S
x : Sˣ
f : R[X]
n : ℕ
⊢ ∃ x, toLaurent f * T (-↑n) * (algebraMap R[X] R[T;T⁻¹]) ↑x.2 = (algebraMap R[X] R[T;T⁻¹]) x.1

Tactic:
| _ f n
       => 

Goal state after:
case mul_T
R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f✝ : R →+* S
x : Sˣ
f : R[X]
n : ℕ
⊢ ∃ x, toLaurent f * T (-↑n) * (algebraMap R[X] R[T;T⁻¹]) ↑x.2 = (algebraMap R[X] R[T;T⁻¹]) x.1
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
L : List (TransvectionStruct n R)
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1

Tactic:
induction L with
  | nil => simp
  | cons t L IH =>
    suffices
      (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (t.inv.toMatrix * t.toMatrix) *
          (L.map toMatrix).prod = 1
      by simpa [Matrix.mul_assoc]
    simpa [inv_mul] using IH

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 α
inst✝ : Nontrivial n
i j : n
⊢ adjugate 0 i j = 0 i j

Tactic:
obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j

Goal state after:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ adjugate 0 i j = 0 i j
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup 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
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
hpT : Algebra.algebraMapSubmonoid T p ≤ T⁰
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
by
  rw [← lift_inj.{_, max uS uT uN}, lift_lift, lift_lift]
  let ST := S ⊗[R] T
  conv_rhs => rw [← lift_lift.{uN, max uS uT uP}, ← IsLocalizedModule.lift_rank_eq p f hp,
    ← IsLocalization.rank_eq S p hp, lift_lift, ← lift_lift.{max uS uT, max uM uP},
    ← rank_baseChange (R := ST), ← lift_id'.{max uS uT, max uS uT uN} (Module.rank ..),
    lift_lift, ← lift_lift.{max uS uT uP, uM}]
  let _ : Algebra T ST := Algebra.TensorProduct.rightAlgebra
  set pT := Algebra.algebraMapSubmonoid T p
  rw [← lift_lift.{max uS uT, max uM uN}, ← lift_umax.{uP},
    ← IsLocalizedModule.lift_rank_eq pT (mk T ST P 1) hpT,
    ← IsLocalization.rank_eq ST pT hpT, lift_id'.{uP, max uS uT},
    ← lift_id'.{max uS uT, max uS uT uP} (Module.rank ..), lift_lift,
    ← lift_lift.{max uS uT uN, uM}, lift_inj]
  exact LinearEquiv.lift_rank_eq <| AlgebraTensorModule.congr (.refl ST ST) bc.equiv.symm ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange .. ≪≫ₗ (AlgebraTensorModule.cancelBaseChange ..).symm ≪≫ₗ
    AlgebraTensorModule.congr (.refl ..) ((isLocalizedModule_iff_isBaseChange p S f).mp ‹_›).equiv

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

Goal state before:
pp: n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i 1 = ⇑f ∘ Pi.single i 1

Tactic:
← f.map_one

Goal state after:
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i (f 1) = ⇑f ∘ Pi.single i 1
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ 0 * (A.submatrix j.succAbove h.succAbove).det = 0

Tactic:
zero_mul

Goal state after:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ 0 = 0
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 + C * V * ⅟A * U * C)
⊢ U * C * V * ⅟A -
      (A * (⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) +
        U * C * V * (⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A)) =
    0

Tactic:
sub_eq_zero

Goal state after:
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 + C * V * ⅟A * U * C)
⊢ U * C * V * ⅟A =
    A * (⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) +
      U * C * V * (⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟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✝⁴ : 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 + C * V * ⅟A * U * C)
⊢ ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A * A -
      (⅟A * (U * C * V) - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A * (U * C * V)) =
    0

Tactic:
sub_eq_zero

Goal state after:
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 + C * V * ⅟A * U * C)
⊢ ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A * A =
    ⅟A * (U * C * V) - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A * (U * C * V)
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 α
B : Matrix n m α
h : IsUnit A.det
⊢ A * (A⁻¹ * B) = B

Tactic:
simp [← Matrix.mul_assoc, mul_nonsing_inv A h]

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

Goal state before:
pp: case neg.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h✝ : IsEmpty n
⊢ A⁻¹.det = A.det⁻¹ʳ

Tactic:
det_isEmpty,

Goal state after:
case neg.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h✝ : IsEmpty n
⊢ 1 = A.det⁻¹ʳ
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case neg.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h✝ : IsEmpty n
⊢ 1 = A.det⁻¹ʳ

Tactic:
det_isEmpty,

Goal state after:
case neg.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h✝ : IsEmpty n
⊢ 1 = 1⁻¹ʳ
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case pos
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : b k < b i
⊢ 0 * N k j = 0

Tactic:
zero_mul

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

Goal state before:
pp: α : 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' ⋯
⊢ image b univ = insert k ((image b univ).erase k)

Tactic:
insert_erase

Goal state after:
α : 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' ⋯
⊢ image b univ = image b univ

α : 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' ⋯
⊢ k ∈ image b univ
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
M : Matrix n n R
k : ℕ
i j : n
⊢ (matPolyEquiv M.charmatrix).coeff k i j = (X - C M).coeff k i j

Tactic:
simp only [matPolyEquiv_coeff_apply, coeff_sub]

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j
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
⊢ eval t M.charmatrix.det = ((scalar m) t - M).det

Tactic:
← Polynomial.coe_evalRingHom,

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) M.charmatrix.det = ((scalar m) t - M).det
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).mapMatrix M.charmatrix).det = ((scalar m) t - M).det

Tactic:
Matrix.charmatrix

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 ((scalar m) X - C.mapMatrix M)).det = ((scalar m) t - M).det
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u v : n → R
h✝ : Nonempty n
h : 1 ≤ Fintype.card n
⊢ (replicateCol Unit u * replicateRow Unit v).charpoly = X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)

Tactic:
charpoly_mul_comm_of_le (n := Unit) _ _ h,

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u v : n → R
h✝ : Nonempty n
h : 1 ≤ Fintype.card n
⊢ X ^ (Fintype.card n - Fintype.card Unit) * (replicateRow Unit v * replicateCol Unit u).charpoly =
    X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: case e_a.e_a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (f.sum fun e a ↦ a * x ^ e) = eval x f

Tactic:
rw [← eval_eq_sum]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : 1 = 0
⊢ 0 * e = 0

Tactic:
zero_mul

Goal state after:
case zero
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : 1 = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case pos
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : m ≤ i
⊢ 0 * y ^ j = 0

Tactic:
zero_mul

Goal state after:
case pos
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : m ≤ i
⊢ 0 = 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
M : Matrix n n R
inst✝ : Nontrivial R
i j : n
⊢ (M.charmatrix i j).natDegree = if i = j then 1 else 0

Tactic:
by
  by_cases h : i = j <;> simp [h]

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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C A.det * ((scalar n) X - C.mapMatrix A⁻¹).det) =
    C A⁻¹.det * (C.mapMatrix A * ((scalar n) X - C.mapMatrix A⁻¹)).det

Tactic:
simp [RingHom.map_det]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ 0 * i.choose l = 0

Tactic:
zero_mul

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r✝ : R
f : R[X]
r : R
P : R[X]
⊢ (taylorAlgHom (-r)) ((↑↑(taylorAlgHom r).toRingHom).toFun P) = P

Tactic:
simp [taylor, comp_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r✝ : R
f : R[X]
r : R
P : R[X]
⊢ (↑↑(taylorAlgHom r).toRingHom).toFun ((taylorAlgHom (-r)) P) = P

Tactic:
simp [taylor, comp_assoc]

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

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

Tactic:
simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]

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

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

Tactic:
simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]

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
⊢ (algebraMap R N) a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R S) a

Tactic:
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: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : f.natDegree = 0 ∧ g.natDegree = 0
⊢ f.Splits ∧ g.Splits

Tactic:
exact ⟨.of_natDegree_eq_zero hn.1, .of_natDegree_eq_zero hn.2⟩

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

Goal state before:
pp: case pos
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
hp : f p.leadingCoeff = 0
⊢ f.IsIntegralElem (0 * x)

Tactic:
zero_mul

Goal state after:
case pos
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
hp : f p.leadingCoeff = 0
⊢ f.IsIntegralElem 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : v' * (algebraMap R Rₘ) ↑⟨v, ⋯⟩ = 1
⊢ (algebraMap Rₘ Sₘ) v' * (algebraMap S Sₘ) u = 1

Tactic:
replace hv' := congr_arg (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S)) hv'
    rw [map_mul, map_one, localizationAlgebraMap_def, IsLocalization.map_eq] at hv'
    exact hv.2 ▸ hv'

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:
have h : (f /ₘ (X - C x)).natDegree = 1 := by
    rw [natDegree_divByMonic f (monic_X_sub_C x), h₁, natDegree_X_sub_C]

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
h : (f /ₘ (X - C x)).natDegree = 1
⊢ f.Splits
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : p.coeff n = 0
⊢ 0 * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
zero_mul

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : p.coeff n = 0
⊢ 0 ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ comap (mapRingHom (Quotient.mk (comap C P))) (map (mapRingHom (Quotient.mk (comap C P))) P) = P

Tactic:
rw [comap_map_of_surjective (mapRingHom (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))))
      (map_surjective (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))) Ideal.Quotient.mk_surjective)]

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ P ⊔ comap (mapRingHom (Quotient.mk (comap C P))) ⊥ = P
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : (aeval x) p = 0
⊢ 0 * (aeval x) (C p.leadingCoeff⁻¹) = 0

Tactic:
zero_mul

Goal state after:
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : (aeval x) p = 0
⊢ 0 = 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✝
ι : Type u_1
inst✝³ : Nonempty ι
M : ι → Type u_2
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), FaithfullyFlat R (M i)
⊢ FaithfullyFlat R (⨁ (i : ι), M i)

Tactic:
rw [iff_flat_and_lTensor_faithful]
  refine ⟨inferInstance, fun N _ _ hN ↦ ?_⟩
  obtain ⟨i⟩ := ‹Nonempty ι›
  obtain ⟨x, y, hxy⟩ := Nontrivial.exists_pair_ne (α := M i ⊗[R] N)
  have : Nontrivial (⨁ (i : ι), M i ⊗[R] N) :=
    ⟨DirectSum.of _ i x, DirectSum.of _ i y, fun h ↦ hxy (DirectSum.of_injective i h)⟩
  apply (TensorProduct.directSumLeft R R M N).toEquiv.nontrivial

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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
⊢ ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

Tactic:
choose r hr int using fun x ↦ (alg.1 x).exists_integral_multiple

Goal state after:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
⊢ ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
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:
· refine _root_.trans (comap_map_of_surjective _ Quotient.mk_surjective _) (sup_eq_left.2 ?_)
    simpa [← RingHom.ker_eq_comap_bot] using hIP

Goal state after: