mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case mk
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
⊢ A'.det = ∑ j, A' (e i) j * A'.adjugate j (e i)

Tactic:
rw [det_succ_row A' (e i)]

Goal state after:
case mk
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
⊢ ∑ j, (-1) ^ (↑(e i) + ↑j) * A' (e i) j * (A'.submatrix (e i).succAbove j.succAbove).det =
    ∑ j, A' (e i) j * A'.adjugate j (e i)
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 α
inst✝ : Invertible A
u v : n → α
hM : u = A *ᵥ v
⊢ A⁻¹ *ᵥ A *ᵥ v = v

Tactic:
Matrix.mulVec_mulVec,

Goal state after:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
u v : n → α
hM : u = A *ᵥ v
⊢ (A⁻¹ * A) *ᵥ v = v
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
i✝ j✝ : n
⊢ ∑ i, a₁✝ * a₂✝ * ((algebraMap R A) (b₁✝ i✝ i) * (algebraMap R A) (b₂✝ i j✝)) =
    ∑ x, a₁✝ * (algebraMap R A) (b₁✝ i✝ x) * (a₂✝ * (algebraMap R A) (b₂✝ x j✝))

Tactic:
_root_.mul_assoc,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
i✝ j✝ : n
⊢ ∑ x, a₁✝ * (a₂✝ * ((algebraMap R A) (b₁✝ i✝ x) * (algebraMap R A) (b₂✝ x j✝))) =
    ∑ x, a₁✝ * ((algebraMap R A) (b₁✝ i✝ x) * (a₂✝ * (algebraMap R A) (b₂✝ x j✝)))
Module: Mathlib.RingTheory.Polynomial.Nilpotent

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

Tactic:
rw [← commute_X P]
  exact isNilpotent_X_mul_iff

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

Goal state before:
pp: case left
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
h : P.coeff 0 * Q.coeff 0 = (P * Q).coeff 0
⊢ P.coeff 0 * Q.coeff 0 = 1

Tactic:
rwa [hQ, coeff_one_zero] at h

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

Tactic:
obtain ⟨p, hp, hx⟩ := hx
  exact ⟨p, hp, by simp_rw [← hom_eval₂, eval₂_eq_eval_map] at hx ⊢; simp [hx]⟩

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

Goal state before:
pp: case mp
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral R a
this✝ : Algebra R T := φ.toRingHom.toAlgebra
this : IsScalarTower R T S :=
  {
    smul_assoc := fun r t s ↦
      Eq.mpr
        (id
          (congr
            (congrArg Eq
              (Eq.trans
                (Eq.trans (congrFun' (congrArg HSMul.hSMul (Algebra.smul_def r t)) s)
                  (Algebra.smul_def ((algebraMap R T) r * t) s))
                (Eq.trans (congrFun' (congrArg HMul.hMul (map_mul (algebraMap T S) ((algebraMap R T) r) t)) s)
                  (mul_assoc ((algebraMap T S) ((algebraMap R T) r)) ((algebraMap T S) t) s))))
            (Eq.trans
              (Eq.trans (congrArg (HSMul.hSMul r) (Algebra.smul_def t s)) (Algebra.smul_def r ((algebraMap T S) t * s)))
              (congrFun' (congrArg HMul.hMul (congrFun' (congrArg DFunLike.coe (Eq.symm h)) r))
                ((algebraMap T S) t * s)))))
        (Eq.refl ((algebraMap T S) ((algebraMap R T) r) * ((algebraMap T S) t * s))) }
⊢ IsIntegral T a

Tactic:
exact IsIntegral.tower_top ha

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

Goal state before:
pp: case mpr
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this✝ : Algebra T R := φ.symm.toRingHom.toAlgebra
this : IsScalarTower T R S :=
  {
    smul_assoc := fun r t s ↦
      Eq.mpr
        (id
          (congr
            (congrArg Eq
              (Eq.trans
                (Eq.trans (congrFun' (congrArg HSMul.hSMul (Algebra.smul_def r t)) s)
                  (Algebra.smul_def ((algebraMap T R) r * t) s))
                (Eq.trans (congrFun' (congrArg HMul.hMul (map_mul (algebraMap R S) ((algebraMap T R) r) t)) s)
                  (mul_assoc ((algebraMap R S) ((algebraMap T R) r)) ((algebraMap R S) t) s))))
            (Eq.trans
              (Eq.trans (congrArg (HSMul.hSMul r) (Algebra.smul_def t s)) (Algebra.smul_def r ((algebraMap R S) t * s)))
              (congrFun' (congrArg HMul.hMul (congrFun' (congrArg DFunLike.coe h') r)) ((algebraMap R S) t * s)))))
        (Eq.refl ((algebraMap R S) ((algebraMap T R) r) * ((algebraMap R S) t * s))) }
⊢ IsIntegral R a

Tactic:
exact IsIntegral.tower_top ha

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

Goal state before:
pp: case empty
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
his : ∀ x ∈ ∅, IsIntegral R x
x : A
⊢ x ∈ R ∙ 1 ↔ x ∈ Subalgebra.toSubmodule ⊥

Tactic:
← one_eq_span,

Goal state after:
case empty
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
his : ∀ x ∈ ∅, IsIntegral R x
x : A
⊢ x ∈ 1 ↔ x ∈ Subalgebra.toSubmodule ⊥
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : (aeval x.1) p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : (aeval x.2) p₂ = 0
⊢ (0, (aeval x.2) p₁ * 0) = 0

Tactic:
mul_zero,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : (aeval x.1) p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : (aeval x.2) p₂ = 0
⊢ (0, 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
hn : Fintype.card n = 2
⊢ M.charpoly = X ^ 2 - C M.trace * X + C M.det

Tactic:
by
  have : Nonempty n := by rw [← Fintype.card_pos_iff]; lia
  ext i
  by_cases hi : i ∈ Finset.range 3
  · 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
  · rw [Finset.mem_range, not_lt, Nat.succ_le_iff] at hi
    suffices M.charpoly.coeff i = 0 by
      simpa [show i ≠ 2 by lia, show 1 ≠ i by lia, show i ≠ 0 by lia, coeff_X, coeff_C]
    apply coeff_eq_zero_of_natDegree_lt
    simpa [charpoly_natDegree_eq_dim, hn] using hi

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, map f q = p ∧ q.degree = p.degree

Tactic:
obtain ⟨q, hq, hq'⟩ := exists_support_eq_of_mem_lifts hlifts
  exact ⟨q, hq, congrArg Finset.max hq'⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
⊢ ∀ (x y : ↥A'),
    { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } (x * y) =
      { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } x *
        { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } y

Tactic:
by intro x y; ext; apply mul_smul

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

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this✝ : Algebra R S := f.toAlgebra
this : (Subalgebra.toSubmodule (Algebra.adjoin R ({x} ∪ {y}))).FG
⊢ f.IsIntegralElem z

Tactic:
Set.singleton_union

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this✝ : Algebra R S := f.toAlgebra
this : (Subalgebra.toSubmodule R[x, y]).FG
⊢ f.IsIntegralElem z
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (x • 1 ⊗ₜ[R] y)

Tactic:
exact smul _ (h.map_of_comp_eq (algebraMap R A)
    (Algebra.TensorProduct.includeRight (R := R) (A := A) (B := B)).toRingHom
    Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap)

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

Goal state before:
pp: case succ.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)

Tactic:
rw [← choose_symm_of_eq_add this, choose_succ_right_eq, mul_comm]

Goal state after:
case succ.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (n + k + 1).choose n * (k + 1) = (n + k + 1).choose n * (n + k + 1 - n)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max (Finset.fold max 0 (fun x ↦ 0) ({x ∈ p.support | ↑(x.choose n) * p.coeff x = 0}))
      (Finset.fold max 0 (fun x ↦ x - n) ({i ∈ p.support | ¬↑(i.choose n) * p.coeff i = 0})) ≤
    p.natDegree - n

Tactic:
Finset.fold_const

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max (if {x ∈ p.support | ↑(x.choose n) * p.coeff x = 0} = ∅ then 0 else max 0 0)
      (Finset.fold max 0 (fun x ↦ x - n) ({i ∈ p.support | ¬↑(i.choose n) * p.coeff i = 0})) ≤
    p.natDegree - n

case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 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
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
n✝ : ℕ
i j : n
⊢ (if i ∈ s then (X • M.map ⇑C) i else 1 i) j =
    if i ∈ s then X * (if i ∈ s then M.map (⇑C) i else 1 i) j else (if i ∈ s then M.map (⇑C) i else 1 i) j

Tactic:
split_ifs <;> rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
mem_antidiagonal

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x.1 + x.2 = k
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
⊢ (hasseDeriv k) (f * g) = ∑ ij ∈ antidiagonal k, (hasseDeriv ij.1) f * (hasseDeriv ij.2) g

Tactic:
by
  let D k := (@hasseDeriv R _ k).toAddMonoidHom
  let Φ := @AddMonoidHom.mul R[X] _
  change
    (compHom (D k)).comp Φ f g =
      ∑ ij ∈ antidiagonal k, ((compHom.comp ((compHom Φ) (D ij.1))).flip (D ij.2) f) g
  simp only [← finsetSum_apply]
  congr 2
  clear f g
  ext m r n s : 4
  simp only [Φ, D, finsetSum_apply, coe_mulLeft, coe_comp, flip_apply, Function.comp_apply,
             hasseDeriv_monomial, LinearMap.toAddMonoidHom_coe, compHom_apply_apply,
             coe_mul, monomial_mul_monomial]
  have aux :
    ∀ x : ℕ × ℕ,
      x ∈ antidiagonal k →
        monomial (m - x.1 + (n - x.2)) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
          monomial (m + n - k) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s)) := by
    intro x hx
    rw [mem_antidiagonal] at hx
    subst hx
    by_cases! hm : m < x.1
    · simp only [Nat.choose_eq_zero_of_lt hm, Nat.cast_zero, zero_mul,
                 monomial_zero_right]
    by_cases! hn : n < x.2
    · simp only [Nat.choose_eq_zero_of_lt hn, Nat.cast_zero, zero_mul,
                 mul_zero, monomial_zero_right]
    rw [tsub_add_eq_add_tsub hm, ← add_tsub_assoc_of_le hn, ← tsub_add_eq_tsub_tsub,
      add_comm x.2 x.1, mul_assoc, ← mul_assoc r, ← (Nat.cast_commute _ r).eq, mul_assoc, mul_assoc]
  rw [Finset.sum_congr rfl aux]
  rw [← map_sum, ← Finset.sum_mul]
  congr
  rw_mod_cast [← Nat.add_choose_eq]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i : ι
⊢ (tensorEquivSum R σ ι S) (1 ⊗ₜ[R] X i) = X (Sum.inr i)

Tactic:
by
  simp [tensorEquivSum, algebraTensorAlgEquiv, sumAlgEquiv, renameEquiv, rename, X, C, monomial]

Goal state after:
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₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1) *
        (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) *
      p.coeff n ∈
    Set.range ⇑(algebraMap R Rₘ)

Tactic:
_root_.mul_assoc,

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₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1) *
      ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) * p.coeff n) ∈
    Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case ha
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
z : R
hz : z ∈ f.roots
⊢ x - z ≠ 0

Tactic:
aesop (add simp sub_eq_zero)

Goal state after:
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
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : p.coeff 0 = 0
a_ne_zero : a ≠ 0
a✝¹ : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p + C a ≠ 0
hp : eval₂ f r (p + C a) = 0
⊢ ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I

Tactic:
refine ⟨0, ?_, coeff_zero_mem_comap_of_root_mem hr hp⟩

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : p.coeff 0 = 0
a_ne_zero : a ≠ 0
a✝¹ : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p + C a ≠ 0
hp : eval₂ f r (p + C a) = 0
⊢ (p + C a).coeff 0 ≠ 0
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
⊢ IsAlgebraic K x → IsIntegral K x

Tactic:
rintro ⟨p, hp, hpx⟩

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
⊢ IsIntegral K x
Module: Mathlib.RingTheory.Algebraic.Integral

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

Tactic:
have : IsAlgebraic (integralClosure R S) a := by
    refine ⟨p, ?_, ?_⟩
    · simpa only [← Polynomial.map_ne_zero_iff (f := Subring.subtype _) (p := p)
        Subtype.val_injective, p, map_toSubring, smul_ne_zero_iff] using And.intro hr hp
    rw [← eval_map_algebraMap, Subalgebra.algebraMap_eq, ← map_map, ← Subalgebra.toSubring_subtype,
      map_toSubring, eval_map_algebraMap, ← AlgHom.restrictScalars_apply R,
      map_smul, AlgHom.restrictScalars_apply, eval0, smul_zero]

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

Goal state before:
pp: 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 := ⋯
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := ⋯
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := ⋯
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ (t ^ N * q.sum fun x1 x2 ↦ t ^ x1 * φ.toRingHom x2) = 0

Tactic:
mul_comm (t ^ _),

Goal state after:
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
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ (q.sum fun x1 x2 ↦ φ.toRingHom x2 * t ^ x1) * t ^ N = 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ R[y]
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (r • z)
⊢ IsAlgebraic R z

Tactic:
exact this.of_smul (mem_nonZeroDivisors_of_ne_zero hr)

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
S : Type u_1
N : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfullyFlat R S
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
I : Ideal R
⊢ Ideal.map (algebraMap R S) I • ⊤ ≠ ⊤ ↔ I • ⊤ ≠ ⊤

Tactic:
simpa only [← Submodule.Quotient.subsingleton_iff.not] using not_congr <|
    (tensorQuotEquivQuotSMul N (I.map (algebraMap R S))).symm ≪≫ₗ TensorProduct.comm S N _ ≪≫ₗ
      hf.tensorEquiv _ ≪≫ₗ AlgebraTensorModule.congr (I.qoutMapEquivTensorQout S) (.refl R M) ≪≫ₗ
        AlgebraTensorModule.assoc R R S S _ M ≪≫ₗ (TensorProduct.comm R _ M).baseChange R S _ _ ≪≫ₗ
          (tensorQuotEquivQuotSMul M I).baseChange R S _ _ |>.subsingleton_congr.trans <|
            subsingleton_tensorProduct_iff_right R S

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
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
⊢ 1 ⊗ₜ[R] (1 • 1) * 0 = 0 ⊗ₜ[R] 1

Tactic:
mul_zero,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
⊢ 0 = 0 ⊗ₜ[R] 1
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ 1 ⊗ₜ[R] (r₁ • t₁) * 1 ⊗ₜ[R] (r₂ • t₂) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)

Tactic:
mul_add,

Goal state after:
case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ 1 ⊗ₜ[R] (r₁ • t₁) * 1 ⊗ₜ[R] (r₂ • t₂) * x₁ + 1 ⊗ₜ[R] (r₁ • t₁) * 1 ⊗ₜ[R] (r₂ • t₂) * x₂ =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)