mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x✝ : 𝕎 k
n : ℕ
h : ∀ (n : ℕ), x✝ ≡ 0 [SMOD Ideal.span {↑p} ^ n]
this : ∀ m < n + 1, x✝.coeff m = 0
⊢ x✝.coeff n = coeff 0 n

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x✝ : 𝕎 k
n : ℕ
h : ∀ (n : ℕ), x✝ ≡ 0 [SMOD Ideal.span {↑p} ^ n]
this : ∀ m < n + 1, x✝.coeff m = 0
⊢ x✝.coeff n = 0
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
n : ℕ
x : R♭
⊢ (ghostComponentModPPow n) ((teichmuller p) ((PreTilt.coeff n) x)) = (Ideal.Quotient.mk (𝔭 ^ (n + 1))) (untilt x)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
n : ℕ
x : R♭
⊢ (ghostComponentModPPow n) ((teichmuller p) ((PreTilt.coeff n) x)) = (Ideal.Quotient.mk (𝔭 ^ (n + 1))) (untilt x)
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
n : ℕ
x : R
⊢ ((teichmuller p) x * ↑p ^ n).coeff n = x ^ p ^ n

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
n : ℕ
x : R
⊢ ((teichmuller p) x * ↑p ^ n).coeff n = x ^ p ^ n
Module: Mathlib.RingTheory.Perfectoid.BDeRham

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete (span {↑p}) R
⊢ IsUnit (((algebraMap R (Localization.Away ↑p)).comp (fontaineTheta R p)) ↑p)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete (span {↑p}) R
⊢ IsUnit ↑p
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
ne : ¬i = f.natDegree
lt : i < f.natDegree
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (X ^ f.natDegree).coeff i

Tactic:
simpa using

Goal state after:
case neg.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
ne : ¬i = f.natDegree
lt : i < f.natDegree
⊢ f.coeff i ∈ I
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
ne : ¬i = f.natDegree
lt : i < f.natDegree
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (X ^ f.natDegree).coeff i

Tactic:
simpa [ne, eq_zero_iff_mem] using (distinguish.mem lt)

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

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

Tactic:
delta hilbertPoly
  induction d with
  | zero => simp only [add_zero]
  | succ d _ =>
      simp only
      rw [← sum_def _ fun _ r => r • _]
      exact sum_add_index _ _ _ (fun _ => zero_smul ..) (fun _ _ _ => add_smul ..)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
ht : ∀ (r : R), (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a
⊢ b = c

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
ht : ∀ (r : R), (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a
⊢ b = c
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (X ^ n - X - 1)

Tactic:
by
  by_cases hn0 : n = 0
  · rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]
    exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X
  have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by
    simp only [trinomial, C_neg, C_1]; ring
  have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
  have h := (IsPrimitive.Int.irreducible_iff_irreducible_map_cast ?_).mp
    (X_pow_sub_X_sub_one_irreducible hn1)
  · rwa [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one,
      Polynomial.map_X] at h
  · exact hp.symm ▸ (trinomial_monic zero_lt_one hn).isPrimitive

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
hp_natDegree : p.natDegree = 2
hp_roots_card : p.roots.card = p.natDegree
⊢ b = -a * (x1 + x2)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
hp_natDegree : p.natDegree = 2
hp_roots_card : p.roots.card = p.natDegree
⊢ b = -(a * (x2 + x1))
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
hp_natDegree : p.natDegree = 2
hp_roots_card : p.roots.card = p.natDegree
⊢ c = a * x1 * x2

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
p : R[X] := C a * X ^ 2 + C b * X + C c
hp_natDegree : p.natDegree = 2
hp_roots_card : p.roots.card = p.natDegree
⊢ c = a * (x1 * x2)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
x : R
⊢ (aeval x) (shiftedLegendre n) = (-1) ^ n * (aeval (1 - x)) (shiftedLegendre n)

Tactic:
have := congr(aeval x $(neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq n))

Goal state after:
n : ℕ
R : Type u_1
inst✝ : Ring R
x : R
this : (aeval x) ((-1) ^ n * (shiftedLegendre n).comp (1 - X)) = (aeval x) (shiftedLegendre n)
⊢ (aeval x) (shiftedLegendre n) = (-1) ^ n * (aeval (1 - x)) (shiftedLegendre n)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
x : R
this : (aeval x) ((-1) ^ n * (shiftedLegendre n).comp (1 - X)) = (aeval x) (shiftedLegendre n)
⊢ (aeval x) (shiftedLegendre n) = (-1) ^ n * (aeval (1 - x)) (shiftedLegendre n)

Tactic:
simpa using

Goal state after:
n : ℕ
R : Type u_1
inst✝ : Ring R
x : R
this : (aeval x) ((-1) ^ n * (shiftedLegendre n).comp (1 - X)) = (aeval x) (shiftedLegendre n)
⊢ (aeval x) (shiftedLegendre n) = (-1) ^ n * (aeval (1 - x)) (shiftedLegendre n)
Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
hg : ∀ i ≤ n, (coeff i) g ∈ I
⊢ ∀ i ≤ n, (coeff i) (f * g) ∈ I

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
hg : ∀ i ≤ n, (coeff i) g ∈ I
⊢ ∀ i ≤ n, (coeff i) (f * g) ∈ I
Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I : Ideal A
f g : A⟦X⟧
hg : ∀ (i : ℕ), (coeff i) g ∈ I
⊢ ∀ (i : ℕ), (coeff i) (f * g) ∈ I

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : Semiring A
I : Ideal A
f g : A⟦X⟧
hg : ∀ (i : ℕ), (coeff i) g ∈ I
⊢ ∀ (i : ℕ), (coeff i) (f * g) ∈ I
Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem

Goal state before:
pp: A : Type u_1
inst✝¹ : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
inst✝ : I.IsTwoSided
hf : ∀ i ≤ n, (coeff i) f ∈ I
⊢ ∀ i ≤ n, (coeff i) (f * g) ∈ I

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝¹ : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
inst✝ : I.IsTwoSided
hf : ∀ i ≤ n, (coeff i) f ∈ I
⊢ ∀ i ≤ n, (coeff i) (f * g) ∈ I
Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem

Goal state before:
pp: A : Type u_1
inst✝¹ : Semiring A
I : Ideal A
f g : A⟦X⟧
inst✝ : I.IsTwoSided
hf : ∀ (i : ℕ), (coeff i) f ∈ I
⊢ ∀ (i : ℕ), (coeff i) (f * g) ∈ I

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝¹ : Semiring A
I : Ideal A
f g : A⟦X⟧
inst✝ : I.IsTwoSided
hf : ∀ (i : ℕ), (coeff i) f ∈ I
⊢ ∀ (i : ℕ), (coeff i) (f * g) ∈ I
Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem

Goal state before:
pp: A : Type u_1
inst✝¹ : Semiring A
I : Ideal A
f g : A⟦X⟧
inst✝ : I.IsTwoSided
hf : ∀ (i : ℕ), (coeff i) f ∈ I
⊢ ∀ (i : ℕ), (coeff i) (f * g) ∈ I

Tactic:
by
  simpa only [Ideal.IsTwoSided.mul_one] using
    coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (J := 1) (g := g) hf (by simp)

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 =
      if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0

Tactic:
intro x a

Goal state after:
n : ℕ
hn : 0 < n
x : ℕ
a : x ∈ range n
⊢ (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
h : (rTensor N P.subtype) t = (rTensor N P.subtype) 0
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = 0

Tactic:
simpa using

Goal state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
h : (rTensor N P.subtype) t = (rTensor N P.subtype) 0
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = 0
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case e'_3
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
f : M →ₚₗ[R] N
S : Type u
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (rTensor M (Algebra.algHom R R S).toLinearMap) (1 ⊗ₜ[R] x)

Tactic:
· rw [rTensor_tmul, toLinearMap_apply, map_one]

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

Goal state before:
pp: n : ℕ
⊢ radical n ≤ 1 ↔ n ≤ 1

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ radical n ≤ 1 ↔ n ≤ 1
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ n < radical n ↔ n = 0

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ n < radical n ↔ n = 0
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ radical z ≤ 1 ↔ z.natAbs ≤ 1

Tactic:
simpa using

Goal state after:
z : ℤ
⊢ radical z ≤ 1 ↔ z.natAbs ≤ 1
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : Module S N
inst✝⁵ : IsScalarTower R S N
p : Ideal R
inst✝⁴ : p.IsPrime
inst✝³ : IsLocalization.AtPrime S p
inst✝² : Nontrivial N
inst✝¹ : Module.Finite S N
f : M →ₗ[R] N
inst✝ : IsLocalizedModule.AtPrime p f
rs : List R
reg : IsWeaklyRegular M rs
mem : ∀ r ∈ rs, r ∈ p
this : IsLocalRing S
x✝ : S
hr✝ : x✝ ∈ List.map (⇑(algebraMap R S)) rs
r : R
hr : r ∈ rs
eq : (algebraMap R S) r = x✝
⊢ x✝ ∈ IsLocalRing.maximalIdeal S

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : Module S N
inst✝⁵ : IsScalarTower R S N
p : Ideal R
inst✝⁴ : p.IsPrime
inst✝³ : IsLocalization.AtPrime S p
inst✝² : Nontrivial N
inst✝¹ : Module.Finite S N
f : M →ₗ[R] N
inst✝ : IsLocalizedModule.AtPrime p f
rs : List R
reg : IsWeaklyRegular M rs
mem : ∀ r ∈ rs, r ∈ p
this : IsLocalRing S
x✝ : S
hr✝ : x✝ ∈ List.map (⇑(algebraMap R S)) rs
r : R
hr : r ∈ rs
eq : (algebraMap R S) r = x✝
⊢ r ∈ p
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
h : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) g ∈ I

Tactic:
simpa using

Goal state after:
case pos
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
h : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) g ∈ I
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
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
kerf : f.ker = x • ⊤
fg : g.ker.FG
y : I →₀ R
this✝ : y ∈ x • ⊤
z : I →₀ R
left✝ : z ∈ ⊤
hz : x • z = y
hy : x • g z = 0
this : z ∈ g.ker
⊢ y ∈ x • g.ker

Tactic:
simpa using

Goal state after:
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
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
kerf : f.ker = x • ⊤
fg : g.ker.FG
y : I →₀ R
this✝ : y ∈ x • ⊤
z : I →₀ R
left✝ : z ∈ ⊤
hz : x • z = y
hy : x • g z = 0
this : z ∈ g.ker
⊢ y ∈ x • g.ker
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⟧
inst✝ : IsPrecomplete I A
k i : ℕ
⊢ (coeff i) (H.div f - H.seq f k) ∈ I ^ k

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsPrecomplete I A
k i : ℕ
⊢ ↑(H.divCoeff f i) - (coeff i) (H.seq f k) ∈ I ^ k
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : ¬IsField R
x : R
hx : maximalIdeal R = R ∙ x
⊢ ↑(Submodule.spanFinrank (maximalIdeal R)) ≤ ringKrullDim R

Tactic:
simpa using

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : ¬IsField R
x : R
hx : maximalIdeal R = R ∙ x
⊢ (R ∙ x).spanFinrank ≤ {x}.ncard
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
R' : Type u_2
inst✝¹ : CommRing R'
e : R ≃+* R'
inst✝ : IsRegularRing R
⊢ IsRegularRing R'

Tactic:
have := isNoetherianRing_of_ringEquiv R e
  rw [isRegularRing_iff]
  intro p hp
  exact IsRegularLocalRing.of_ringEquiv <| IsLocalization.ringEquivOfRingEquiv
    (Localization.AtPrime (p.comap e)) (Localization.AtPrime p) e (e.map_primeCompl_comap_eq p)

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

Goal state before:
pp: 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)
⊢ q ≤ p

Tactic:
simpa using

Goal state after:
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)
⊢ Ideal.map C (comap C p) ≤ p
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: 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
⊢ (comap C p).IsMaximal

Tactic:
simpa using

Goal state after:
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
⊢ (maximalIdeal R).IsMaximal
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n✝ : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := ⋯
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
this : ∀ (L : ModuleCat R), Subsingleton (Ext S.X₁ L (n + 1)) ↔ Subsingleton (Ext M L (n + 2))
⊢ ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext S.X₁ L (n + 1))

Tactic:
simpa using

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n✝ : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
this : ∀ (L : ModuleCat R), Subsingleton (Ext S.X₁ L (n + 1)) ↔ Subsingleton (Ext M L (n + 2))
⊢ ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 2))
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
inst✝ : IsAdicComplete I A
⊢ H.div 0 = 0

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsAdicComplete I A
⊢ H.div 0 = 0
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
inst✝ : IsAdicComplete I A
⊢ H.mod 0 = 0

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsAdicComplete I A
⊢ H.mod 0 = 0
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
inst✝ : IsAdicComplete I A
r : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
h1 : (H.mod ↑r).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
h2 : ↑r = g * H.div ↑r + ↑(H.mod ↑r)
⊢ g * H.div ↑r + ↑(H.mod ↑r) = g * 0 + ↑r

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsAdicComplete I A
r : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
h1 : (H.mod ↑r).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
h2 : ↑r = g * H.div ↑r + ↑(H.mod ↑r)
⊢ g * H.div ↑r + ↑(H.mod ↑r) = ↑r
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
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
L : ModuleCat R
a✝ : Module.Finite R ↑L
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
this✝ : S.f = x • 𝟙 M
epi : Function.Surjective ⇑((Ext.mk₀ (x • 𝟙 M)).precomp L ⋯)
ntr : Nontrivial (Ext M L (n + 1))
this : x ∈ (annihilator R (Ext M L (n + 1))).jacobson
y : Ext M L (n + 1)
hy : y ∈ ⊤
z : Ext (M.smulShortComplex x).X₂ L (n + 1)
hz : x • z = y
⊢ y ∈ x • ⊤

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
L : ModuleCat R
a✝ : Module.Finite R ↑L
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
this✝ : S.f = x • 𝟙 M
epi : Function.Surjective ⇑((Ext.mk₀ (x • 𝟙 M)).precomp L ⋯)
ntr : Nontrivial (Ext M L (n + 1))
this : x ∈ (annihilator R (Ext M L (n + 1))).jacobson
y : Ext M L (n + 1)
hy : y ∈ ⊤
z : Ext (M.smulShortComplex x).X₂ L (n + 1)
hz : x • z = y
⊢ x • z ∈ x • ⊤