mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case zero.refine_1
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : Injective M
m : MaximalSpectrum R
⊢ Injective (M.localizedModule m.asIdeal.primeCompl)

pp: case zero.refine_2
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
⊢ Injective M

Tactic:
· let _ : Small.{v} (Localization m.1.primeCompl) :=
        small_of_surjective Localization.mkHom_surjective
      let _ : Module.Injective R M := Module.injective_module_of_injective_object R M
      rw [← Module.injective_iff_injective_object]
      exact Module.injective_of_isLocalizedModule m.1.primeCompl
        (M.localizedModuleMkLinearMap m.1.primeCompl)

Goal state after:
case zero.refine_2
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
⊢ Injective M
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization S)
M : ModuleCat R
inst✝ : HasProjectiveDimensionLE M 0
projle : HasProjectiveDimensionLT M 1
⊢ HasProjectiveDimensionLT (M.localizedModule S) 1

Tactic:
← projective_iff_hasProjectiveDimensionLT_one,

Goal state after:
case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization S)
M : ModuleCat R
inst✝ : HasProjectiveDimensionLE M 0
projle : Projective M
⊢ Projective (M.localizedModule S)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: F : Type u
inst✝ : Field F
n : ℤ
⊢ (single n) 1 = (single 1) 1 ^ n

Tactic:
match n with
  | (n : ℕ) => apply single_one_eq_pow
  | -(n + 1 : ℕ) =>
    rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
b : MvPolynomial n R
hb₀ : b ≠ 0
r : R
hab : p = C r * b
hle : (C r).totalDegree ≤ b.totalDegree
ha₀ : C r ≠ 0
this : (C r).totalDegree + b.totalDegree = 1
i : n →₀ ℕ
⊢ r ∣ coeff i p

Tactic:
simp [hab]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hU₁ : {y | Valued.v.restrict (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -((embedding ↑γ).log - 1)
hD₀ : D = -((embedding ↑γ).log - 1)
hD : exp (-D) < embedding ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
n : ℤ
hn : n < D
⊢ (x✝ - limit hℱ).coeff n = 0

Tactic:
rw [HahnSeries.coeff_sub, sub_eq_zero, eq_comm]

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hU₁ : {y | Valued.v.restrict (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -((embedding ↑γ).log - 1)
hD₀ : D = -((embedding ↑γ).log - 1)
hD : exp (-D) < embedding ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
n : ℤ
hn : n < D
⊢ (limit hℱ).coeff n = x✝.coeff n
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r * esymm (Fin m) R (↑i + 1) ^ b✝))) =
    (accumulate n m) ⇑(f✝ + fun₀ | i => b✝)

Tactic:
Monic.supDegree_mul_of_ne_zero_left toLex.injective toLex_add,

Goal state after:
case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ ⇑(ofLex
        (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) + supDegree (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝))) =
    (accumulate n m) ⇑(f✝ + fun₀ | i => b✝)

case add_single.hq
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝)

case add_single.hp
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ esymmAlgHomMonomial (Fin m) f✝ r ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0✝ : p ≠ 0
h0 : ¬coeff (ofLex (supDegree (⇑toLex) p)) p = 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ coeff (?m.142 i j hle hlt) p ≠ 0

Tactic:
assumption

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

Goal state before:
pp: σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
⊢ #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)

Tactic:
rcases (em (t.snd ∈ t.fst)) with h1 | h1

Goal state after:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∈ t.1
⊢ #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)

case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∉ t.1
⊢ #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∈ t.1
⊢ #(t.1.erase t.2, t.2).1 ≤ k ∧ (#(t.1.erase t.2, t.2).1 = k → (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1)

Tactic:
simp only [h1, implies_true, and_true] at h

Goal state after:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #(t.1.erase t.2, t.2).1 ≤ k ∧ (#(t.1.erase t.2, t.2).1 = k → (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(pairMap σ t).1 * ((∏ a ∈ (pairMap σ t).1, X a) * X (pairMap σ t).2 ^ (k - #(pairMap σ t).1)) =
    0

Tactic:
rcases (em (t.snd ∈ t.fst)) with h1 | h1

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∈ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(pairMap σ t).1 * ((∏ a ∈ (pairMap σ t).1, X a) * X (pairMap σ t).2 ^ (k - #(pairMap σ t).1)) =
    0

case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(pairMap σ t).1 * ((∏ a ∈ (pairMap σ t).1, X a) * X (pairMap σ t).2 ^ (k - #(pairMap σ t).1)) =
    0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∈ t.1
h3 : 1 ≤ #t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - #t.1 + 1)) +
      (-1) ^ (#t.1 - 1) * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) =
    0

Tactic:
← tsub_tsub_assoc h.left h3,

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∈ t.1
h3 : 1 ≤ #t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) +
      (-1) ^ (#t.1 - 1) * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) =
    0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < embedding ↑d}
X_def : X = {f | Valued.v f < embedding ↑d}
x : K⟮X⟯
hx : (restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x = ↑d
⊢ Valued.v.restrict ((algebraMap K⟮X⟯ K⸨X⸩) x) ≠ 0

Tactic:
by
          simp only [ne_eq, map_eq_zero]
          intro h
          simp only [h, map_zero] at hx
          exact Units.ne_zero _ hx.symm

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

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ #t.1) + (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ (#t.1 + 1)) =
    0

Tactic:
rw [← neg_neg ((-1 : MvPolynomial σ R) ^ #t.1), h2]

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * -(-1) ^ (#t.1 + 1)) +
      (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ (#t.1 + 1)) =
    0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mpr.refine_2
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < embedding ↑d}
X_def : X = {f | Valued.v f < embedding ↑d}
x✝¹ : K⟮X⟯ × K⟮X⟯
x✝ : x✝¹ ∈ (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' (fun x ↦ x.2 - x.1) ⁻¹' X
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ((algebraMap K⟮X⟯ K⸨X⸩) x✝¹.2 - (algebraMap K⟮X⟯ K⸨X⸩) x✝¹.1) < embedding ↑d

Tactic:
assumption

Goal state after:
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ → A
n : ℕ
⊢ (aeval f) (W_ R n) = ∑ i ∈ range (n + 1), ↑p ^ i * f i ^ p ^ (n - i)

Tactic:
by
  simp [wittPolynomial, map_sum, aeval_monomial, Finsupp.prod_single_index]

Goal state after:
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n =
    C (1 / ↑p ^ n) *
      ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))

Tactic:
calc
    wittStructureRat p Φ n = C (1 / (p : ℚ) ^ n) * (wittStructureRat p Φ n * C ((p : ℚ) ^ n)) := ?_
    _ = _ := by rw [wittStructureRat_rec_aux]

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n = C (1 / ↑p ^ n) * (wittStructureRat p Φ n * C (↑p ^ n))
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittMul p n) = 0

Tactic:
apply constantCoeff_wittStructureInt p _ _ n
  simp only [mul_zero, map_mul, constantCoeff_X]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m : ℕ
hmn : m ≤ n
⊢ (coeffMonoidHom M p n) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p (n - m)) f

Tactic:
← coeffMonoidHom_iterate_powMonoidHom f (n - m) m,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m : ℕ
hmn : m ≤ n
⊢ (coeffMonoidHom M p n) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p (n - m + m)) ((⇑(powMonoidHom p))^[m] f)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Perfection R p
n : ℕ
hfn : (coeff R p n) f ≠ 0
k✝ k : ℕ
ih : (coeff R p (n + k)) f ≠ 0
h : (coeff R p (n + k).succ) f = 0
⊢ 0 ^ p = 0

Tactic:
zero_pow hp.1.ne_zero

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Perfection R p
n : ℕ
hfn : (coeff R p n) f ≠ 0
k✝ k : ℕ
ih : (coeff R p (n + k)) f ≠ 0
h : (coeff R p (n + k).succ) f = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
⊢ (ghostComponent 0) x.verschiebungFun = 0

Tactic:
by
  rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton,
    verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
⊢ v ↑p < v ((algebraMap O K) x) ↔ (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0

Tactic:
by
  rw [lt_iff_not_ge, not_iff_not, ← map_natCast (algebraMap O K) p, hv.le_iff_dvd,
    Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_1
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
⊢ (coeff (max m n)) f ≠ 0

Tactic:
assumption

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_2
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
⊢ (coeff (max m n)) g ≠ 0

Tactic:
assumption

Goal state after:
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ (truncateFun n x).out = init n x

Tactic:
ext i
  dsimp [TruncatedWittVector.out, init, select, coeff_mk]
  split_ifs with hi; swap; · rfl
  rw [coeff_truncateFun, Fin.val_mk]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff i ((truncate n) (liftFun f s)) = TruncatedWittVector.coeff i ((f n) s)

Tactic:
simp only [liftFun, TruncatedWittVector.coeff_mk, WittVector.truncate_mk']

Goal state after:
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff (Fin.last ↑i) ((f (↑i + 1)) s) = TruncatedWittVector.coeff i ((f n) s)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff (Fin.last ↑i) (((TruncatedWittVector.truncate ⋯).comp (f n)) s) =
    TruncatedWittVector.coeff i ((f n) s)

Tactic:
RingHom.comp_apply,

Goal state after:
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff (Fin.last ↑i) ((TruncatedWittVector.truncate ⋯) ((f n) s)) =
    TruncatedWittVector.coeff i ((f n) s)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
x✝ : S
⊢ ((truncate n).comp (lift f f_compat)) x✝ = (f n) x✝

Tactic:
RingHom.comp_apply,

Goal state after:
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
x✝ : S
⊢ (truncate n) ((lift f f_compat) x✝) = (f n) x✝
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) = ↑((n - k + d).choose d)

Tactic:
by
    rw [ascPochhammer_nat_eq_natCast_ascFactorial];
    simp [field, ascFactorial_eq_factorial_mul_choose]

Goal state after:
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)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit n (k + 2)

Tactic:
rw [(by ring : 2 * (n + 1) + k = 2 * n + (k + 2)), coeff_hermite_explicit n (k + 2)]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (p * (1 - X)).hilbertPoly (d + 1) = p.hilbertPoly d

Tactic:
apply eq_hilbertPoly_of_forall_coeff_eq_eval (p * (1 - X)).natDegree

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∀ n > (p * (1 - X)).natDegree,
    (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: ⊢ constantCoeff largeSchroderSeries = 1

Tactic:
by
  simp only [← coeff_zero_eq_constantCoeff_apply, coeff_largeSchroderSeries, largeSchroder_zero]

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder + (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
have : ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * largeSchroder (n - x) =
      ∑ x ∈ range n, if 0 < x then largeSchroder (x - 1) * largeSchroder (n - x) else 0 := by
    apply sum_congr rfl
    intro x a
    simp_all only [mem_range]
    split
    next h =>
      simp_all only [mul_eq_mul_right_iff]
      simp [coeff_X_mul_largeSchroderSeries x (by lia)]
    next h =>
      simp_all only [not_lt, nonpos_iff_eq_zero, coeff_zero_eq_constantCoeff, map_mul,
      constantCoeff_X, constantCoeff_largeSchroderSeries, mul_one, tsub_zero, zero_mul]

Goal state after:
n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
⊢ ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder + (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
f : A⟦X⟧
hf : constantCoeff f = 1
h : MvPowerSeries.constantCoeff (f - 1) = 0
⊢ constantCoeff (subst (f - 1) (log A)) = 0

Tactic:
exact constantCoeff_subst_eq_zero h _ constantCoeff_log

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: case inr
z : ℤ
hz : z ≠ 0
p : ℤ
⊢ Irreducible p ∧ normalize p = p ∧ p ∣ z ↔ p ∈ Finset.map Nat.castEmbedding z.natAbs.primeFactors

Tactic:
irreducible_iff_prime,

Goal state after:
case inr
z : ℤ
hz : z ≠ 0
p : ℤ
⊢ Prime p ∧ normalize p = p ∧ p ∣ z ↔ p ∈ Finset.map Nat.castEmbedding z.natAbs.primeFactors
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
⊢ Function.Surjective ⇑f

Tactic:
simpa [f] using! Finsupp.mapRange_surjective _ rfl (Submodule.mkQ_surjective (Ideal.span {x}))

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)

Tactic:
obtain ⟨y, _, hy⟩ := Polynomial.exists_monic_span_sup_map_eq R p this (by simpa [max])

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)