mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
⊢ Irreducible (f * X i + g)

Tactic:
classical
  let S := MvPolynomial { j // j ≠ i } R
  let e : MvPolynomial n R ≃ₐ[R] S[X] :=
    (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R _)
  have he : e.symm.toAlgHom.comp Polynomial.CAlgHom = rename (↑) := by ext; simp [e, S]
  obtain ⟨f, rfl⟩ : f ∈ (e.symm.toAlgHom.comp Polynomial.CAlgHom).range :=
    he ▸ exists_rename_eq_of_vars_subset_range _ _ Subtype.val_injective (by simpa [Set.subset_def])
  obtain ⟨g, rfl⟩ : g ∈ (e.symm.toAlgHom.comp Polynomial.CAlgHom).range :=
    he ▸ exists_rename_eq_of_vars_subset_range _ _ Subtype.val_injective (by simpa [Set.subset_def])
  refine .of_map (f := e) ?_
  simpa [e, S] using Polynomial.irreducible_C_mul_X_add_C (by aesop)
    (IsRelPrime.of_map Polynomial.C (IsRelPrime.of_map e.symm h))

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n k : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
i : Fin n
r : R
⊢ (aeval fun i ↦ esymm σ R (↑i + 1)) ((monomial fun₀ | i => k) r) = C r * esymm σ R (↑i + 1) ^ k

Tactic:
aeval_monomial,

Goal state after:
σ : Type u_1
R : Type u_3
n k : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
i : Fin n
r : R
⊢ ((algebraMap R (MvPolynomial σ R)) r * (fun₀ | i => k).prod fun i k ↦ esymm σ R (↑i + 1) ^ k) =
    C r * esymm σ R (↑i + 1) ^ k
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hp'
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
r : R
hr : ∀ (i : n →₀ ℕ), r ∣ coeff i (sumSMulX c)
i : n
⊢ r ∣ c i

Tactic:
simpa [coeff_sumSMulX] using hr (Finsupp.single i 1)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v
      (((single 1) 1 ^ s)⁻¹ * (ofPowerSeries ℤ K) F -
        (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ s)⁻¹ * (algebraMap K⟮X⟯ K⸨X⸩) ↑P) <
    ↑γ

Tactic:
inv_eq_one_div (RatFunc.X ^ s),

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v
      (((single 1) 1 ^ s)⁻¹ * (ofPowerSeries ℤ K) F -
        (algebraMap K⟮X⟯ K⸨X⸩) (1 / RatFunc.X ^ s) * (algebraMap K⟮X⟯ K⸨X⸩) ↑P) <
    ↑γ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
j : Fin m
⊢ (Finsupp.indicator (Iic ⟨↑i, him⟩) fun x x_1 ↦ 1) j = (accumulate n m) (⇑fun₀ | i => 1) j

Tactic:
Finsupp.indicator_apply,

Goal state after:
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
j : Fin m
⊢ (if hi : j ∈ Iic ⟨↑i, him⟩ then 1 else 0) = (accumulate n m) (⇑fun₀ | i => 1) j
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ pairMap σ t ≠ t

Tactic:
rw [pairMap]
  split_ifs with h1
  all_goals by_contra ht; rw [← ht] at h1; simp_all

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
| constantCoeff ((expand p hp) φ)

Tactic:
← coeff_zero_eq_constantCoeff,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
| (coeff 0) ((expand p hp) φ)
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial x') (MvPolynomial.coeff x' f)))).natDegree ≤
      ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).natDegree
⊢ ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree

Tactic:
intro x hx

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial x') (MvPolynomial.coeff x' f)))).natDegree ≤
      ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).natDegree
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1))
      ((X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n))

Tactic:
simp only [map_sum, map_sub, map_mul, map_pow (bind₁ _), bind₁_C_right]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    ((bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (X n) -
        ∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      C (⅟↑p ^ n)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ((bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars ⊆
    Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
intro x hx

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ ((bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
⊢ x ∈ Finset.univ ×ˢ Finset.range (n + 1)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ C ↑p ^ (j + 1) * (C ↑((p ^ (n - i)).choose (j + 1)) * (C ↑p ^ i * C ⅟↑p ^ n)) =
    C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) * C ↑p

Tactic:
simp only [← map_pow, ← C_mul]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ C (↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * ⅟↑p ^ n))) =
    C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) * ↑p)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ ∀ x ∈ ⨅ i, RingHom.ker (WittVector.truncate i), x = 0

Tactic:
intro x hx

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
hx : x ∈ ⨅ i, RingHom.ker (WittVector.truncate i)
⊢ x = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n : ℕ
⊢ (hermite n).degree = ↑n

Tactic:
degree_eq_of_le_of_coeff_ne_zero

Goal state after:
n : ℕ
⊢ ↑?m.6 = ↑n

case pn
n : ℕ
⊢ (hermite n).degree ≤ ↑?m.6

case p1
n : ℕ
⊢ (hermite n).coeff ?m.6 ≠ 0

n : ℕ
⊢ ℕ
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ Chebyshev.T ℚ ↑n = C ⅟2 * 2 * Chebyshev.T ℚ ↑n

Tactic:
C_half_mul_two_eq_one,

Goal state after:
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ Chebyshev.T ℚ ↑n = 1 * Chebyshev.T ℚ ↑n
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 ((ZMod.castHom ⋯ K) 1) p = map (ZMod.castHom ⋯ K) (X ^ p)

Tactic:
Polynomial.map_pow,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 ((ZMod.castHom ⋯ K) 1) p = map (ZMod.castHom ⋯ K) X ^ p
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * (n + 1) - 1)‼ * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * (n + 1) - 1)‼ * (2 * (n + 1) + k).choose k + (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))

Tactic:
rw [(by grind : 2 * (n + 1) - 1 = 2 * n + 1),
        Nat.doubleFactorial_add_one, mul_comm (2 * n + 1)]

Goal state after:
case e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + k).choose k +
      (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
h : 1 = (ZMod.castHom ⋯ R) 1
⊢ map (ZMod.castHom ⋯ R) (X ^ p) = X ^ p

Tactic:
Polynomial.map_pow,

Goal state after:
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
h : 1 = (ZMod.castHom ⋯ R) 1
⊢ map (ZMod.castHom ⋯ R) X ^ p = X ^ p
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ IsCancelMulZero R[X] ↔ IsCancelMulZero R ∧ IsCancelAdd R

Tactic:
simp_rw [isCancelMulZero_iff, isLeftCancelMulZero_iff, isRightCancelMulZero_iff]
  rw [and_and_and_comm, and_self]

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

Goal state before:
pp: case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 :
  (aeval z) (C ↑(-1)) * (aeval z) (X ^ 0) + (aeval z) (C ↑(-1)) * (aeval z) (X ^ 1) +
      (aeval z) (C ↑1) * (aeval z) (X ^ n) =
    0
h2 :
  (aeval z) (C ↑1) * (aeval z) (X ^ 0) + (aeval z) (C ↑(-1)) * (aeval z) (X ^ (n - 1 + 0)) +
      (aeval z) (C ↑(-1)) * (aeval z) (X ^ n) =
    0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Tactic:
aeval_X_pow,

Goal state after:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (aeval z) (C ↑(-1)) * z ^ 0 + (aeval z) (C ↑(-1)) * z ^ 1 + (aeval z) (C ↑1) * z ^ n = 0
h2 : (aeval z) (C ↑1) * z ^ 0 + (aeval z) (C ↑(-1)) * z ^ (n - 1 + 0) + (aeval z) (C ↑(-1)) * z ^ n = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: case neg.refine_2
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (X ^ n) - map (Int.castRingHom ℚ) X - map (Int.castRingHom ℚ) 1)
⊢ Irreducible (X ^ n - X - 1)

Tactic:
Polynomial.map_pow,

Goal state after:
case neg.refine_2
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) X ^ n - map (Int.castRingHom ℚ) X - map (Int.castRingHom ℚ) 1)
⊢ Irreducible (X ^ n - X - 1)
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
| constantCoeff ((expand p hp) φ)

Tactic:
← coeff_zero_eq_constantCoeff,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
| (coeff 0) ((expand p hp) φ)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g f : M →ₚₗ[R] N
⊢ f + 0 = f

Tactic:
ext; simp only [add_def, add_zero, zero_def]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: ⊢ largeSchroderSeries = 1 + X * largeSchroderSeries + X * largeSchroderSeries ^ 2

Tactic:
by
  ext n
  by_cases hn : n = 0
  · aesop
  · have hn' : 0 < n := by omega
    simp only [coeff_largeSchroderSeries, map_add, coeff_one, hn, ↓reduceIte, zero_add]
    rw [coeff_X_mul_largeSchroderSeriesSeries_sq _ hn', coeff_X_mul_largeSchroderSeries _ hn',
      show n = n - 1 + 1 by omega, largeSchroder_succ (n - 1)]
    simp only [add_tsub_cancel_right, Nat.add_left_cancel_iff]
    rw [Iic_eq_Icc, Nat.bot_eq_zero, ← range_succ_eq_Icc_zero]

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

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
M : Type u_1
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_2
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
S : Type v
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝³ : CommSemiring A
inst✝² : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
q : B ⊗[R] M
ψ : B →ₐ[R] S
h : φ.range ≤ ψ.range
hpq :
  (rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ ψ.range.val.comp (Subalgebra.inclusion h) = (AlgHom.id R S).comp φ.range.val

Tactic:
by ext x; simp

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
⊢ s + -(g * ↑⋯.unit⁻¹ * s₁) = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹

Tactic:
nth_rw 1 [g.eq_X_pow_mul_shift_add_trunc n]

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
⊢ s + -(((X ^ n * mk fun i ↦ (coeff (i + n)) g) + ↑((trunc n) g)) * ↑⋯.unit⁻¹ * s₁) =
    ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ A ⊔ Algebra.adjoin R ↑{s}
⊢ ∃ n ψ p q, (rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

Tactic:
← hgen

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (φ R gen).range
⊢ ∃ n ψ p q, (rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  (↑⋯.unit⁻¹ * mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) *
        X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
      q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ (k + 1)

Tactic:
IsUnit.val_inv_mul,

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  1 * X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ (k + 1)
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
len : (x :: rs').length = n + 1
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList (x :: rs') • ⊤)) = projectiveDimension M + ↑(n + 1)

Tactic:
simp only [List.length_cons, Nat.add_right_cancel_iff] at len

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
len : rs'.length = n
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList (x :: rs') • ⊤)) = projectiveDimension M + ↑(n + 1)
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
⊢ ∀ x ∈ rs, x ∈ maximalIdeal R

Tactic:
intro x hx

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
x : R
hx : x ∈ rs
⊢ x ∈ maximalIdeal R
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: case refine_3
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
w✝ : Set (Submodule R M)
hs : w✝ ⊆ isotypicComponents R M
⊢ (sSup w✝).IsFullyInvariant

Tactic:
exact (fullyInvariantSubmodule R M).sSupClosed fun _ h ↦ .of_mem_isotypicComponents (hs h)

Goal state after:
Module: Mathlib.RingTheory.Valuation.Minpoly

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
⊢ v ((minpoly K x).coeff 0) ^ (finrank K L / (minpoly K x).natDegree) ≠ 0

Tactic:
have hdeg := Nat.div_pos (natDegree_le x) (natDegree_pos hx₀)

Goal state after:
K : Type u_1
inst✝⁴ : Field K
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
hdeg : 0 < finrank K L / (minpoly K x).natDegree
⊢ v ((minpoly K x).coeff 0) ^ (finrank K L / (minpoly K x).natDegree) ≠ 0
Module: Mathlib.RingTheory.Valuation.Quotient

Goal state before:
pp: case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ v.supp ≤ Ideal.comap (Ideal.Quotient.mk J) (v.onQuot hJ).supp

Tactic:
intro x hx

Goal state after:
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x : R
hx : x ∈ v.supp
⊢ x ∈ Ideal.comap (Ideal.Quotient.mk J) (v.onQuot hJ).supp
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
this : ∀ {x : R} (h : x ∈ I * J), f (J.toCotangent ⟨x, ⋯⟩) = 0
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker

Tactic:
intro x hx

Goal state after:
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
this : ∀ {x : R} (h : x ∈ I * J), f (J.toCotangent ⟨x, ⋯⟩) = 0
x : J.Cotangent
hx : x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
⊢ x ∈ f.ker