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

Goal state before:
pp: p : ℕ
R : Type u
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n : ℕ
⊢ (algebraMap R (MvPolynomial ℕ R)) (MvPolynomial.constantCoeff (wittPolynomial p R n)) = 0

Tactic:
constantCoeff_wittPolynomial,

Goal state after:
p : ℕ
R : Type u
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n : ℕ
⊢ (algebraMap R (MvPolynomial ℕ R)) 0 = 0
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
h : (↑p ^ i).coeff i = 1
⊢ (↑p ^ (i + 1)).coeff (i + 1) = 1

Tactic:
rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]

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

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : ((⇑verschiebung)^[k] x).coeff (k✝ + k) = x.coeff k✝
⊢ ((⇑verschiebung)^[k + 1] x).coeff (k✝ + (k + 1)) = x.coeff k✝

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case succ
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 : PreTilt O p
h : ∃ n, (coeff n) f ≠ 0
k : ℕ
ih :
  (coeff (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (Nat.find h + (k + 1))) f ≠ 0
⊢ ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))

Tactic:
| succ k ih =>

Goal state after:
case succ
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 : PreTilt O p
h : ∃ n, (coeff n) f ≠ 0
k : ℕ
ih :
  (coeff (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (Nat.find h + (k + 1))) f ≠ 0
⊢ ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))
Module: Mathlib.RingTheory.WittVector.Domain

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
ih : (∀ i < k, x.coeff i = 0) → x = (⇑verschiebung)^[k] (x.shift k)
h : ∀ i < k + 1, x.coeff i = 0
⊢ x = (⇑verschiebung)^[k + 1] (x.shift (k + 1))

Tactic:
| succ k ih =>

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

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ (teichmullerFun p 1).coeff (n✝ + 1) = coeff 1 (n✝ + 1)

Tactic:
rw [one_coeff_eq_of_pos _ _ _ (Nat.succ_pos _)]; rfl

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
x✝ : ∃ c, x = c * ↑p
u : 𝕎 k
hu : x = u * ↑p
⊢ (u * ↑p).coeff 0 = 0

Tactic:
mul_charP_coeff_zero

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
x✝ : ∃ c, x = c * ↑p
u : 𝕎 k
hu : x = u * ↑p
⊢ 0 = 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 ghostComponentModPPow_map_mk n
    (teichmuller p ((((_root_.frobeniusEquiv _ p).symm ^ n) x).untilt))

Goal state after:
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
inst✝¹ : PerfectRing R p
S : Type u_2
inst✝ : CommRing S
f g : 𝕎 R →+* S
h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)
n : ℕ
hn : ↑p ^ n = 0
x c : 𝕎 R
hc : x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i = ↑p ^ (n + 1) * c
⊢ f x =
    f (x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i) +
      f (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ DifferentiableAt ℝ (fun y ↦ -(y ^ 2 / 2)) x

Tactic:
by simp

Goal state after:
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
inst✝¹ : PerfectRing R p
S : Type u_2
inst✝ : CommRing S
f g : 𝕎 R →+* S
h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)
n : ℕ
hn : ↑p ^ n = 0
x c : 𝕎 R
hc : x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i = ↑p ^ (n + 1) * c
⊢ g (x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i) +
      g (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i) =
    g x

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: x✝ : ℕ
⊢ (hermite (2 * 0 + x✝)).coeff x✝ = (-1) ^ 0 * ↑(2 * 0 - 1)‼ * ↑((2 * 0 + x✝).choose x✝)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : Rᵐᵒᵖ
⊢ (opRingEquiv R) ((opRingEquiv R).symm ((monomial n) r)) = (opRingEquiv R) (op ((monomial n) (unop r)))

Tactic:
by simp

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

Goal state before:
pp: case inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
⊢ False

pp: case inr.inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ False

pp: case inr.inr
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ False

Tactic:
· exact z_ne_zero (by rwa [key, right_eq_add] at h1)

Goal state after:
case inr.inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ False

case inr.inr
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ False
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
⊢ 2 ≤ p.natDegree

Tactic:
by convert! p.card_roots'; rw [hroots, Multiset.card_pair]

Goal state after:
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 ∈ ⊤

Tactic:
by simp

Goal state after:
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 ∈ ⊤

Tactic:
by simp

Goal state after:
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) g ∈ 1

Tactic:
by simp

Goal state after:
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) g ∈ 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq { P // P.FG }
x : M
⊢ (Module.DirectLimit.lift R { P // P.FG } (fun P ↦ ↥↑P) (fun ⦃P Q⦄ h ↦ inclusion h) (fun P ↦ (↑P).subtype) ⋯)
      ((Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P) (fun ⦃P Q⦄ h ↦ inclusion h) ⟨R ∙ x, ⋯⟩) ⟨x, ⋯⟩) =
    x

Tactic:
by simp

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
⊢ (expand 1 ⋯) f = f

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
H : Tendsto ((fun n ↦ ‖(coeff n) f‖ * c ^ n) ∘ ⇑(Finsupp.uniqueEquiv ())) cofinite (𝓝 0)
n : ℕ
⊢ (((fun n ↦ ‖(coeff n) f‖ * c ^ n) ∘ ⇑(Finsupp.uniqueEquiv ())) ∘ ⇑(Finsupp.uniqueEquiv ()).symm) n =
    ‖(coeff n) f‖ * c ^ n

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (coeff 1) (log A) = 1

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : Nontrivial A
⊢ (coeff 1) (log A) ≠ 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
⊢ (φ R s).range = Algebra.adjoin R ↑s

Tactic:
simp only [φ]

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
⊢ (aeval fun n ↦ ↑(s.equivFin.symm n)).range = Algebra.adjoin R ↑s
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P'
⊢ (Subalgebra.toSubmodule A).subtype p ∈ P₁

Tactic:
by
        simp only [coe_subtype, Submodule.map_sup, P₁]
        exact Submodule.mem_sup_right ⟨p, hp, rfl⟩

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

Goal state before:
pp: z : ℤ
hz : z ≠ 0
n : ℕ
pn : Nat.Prime n
dn : n ∣ z.natAbs
⊢ 0 ≤ ↑n

Tactic:
by simp

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

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

Tactic:
by
  rw [← radical_le_one_iff]
  grind [radical_pos z]

Goal state after:
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Flat R S
x : R
tail✝ : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : Module R M] [inst_2 : AddCommGroup N]
    [inst_3 : Module R N] [inst_4 : Module S N] [inst_5 : IsScalarTower R S N] {f : M →ₗ[R] N},
    IsBaseChange S f → IsWeaklyRegular M tail✝ → IsWeaklyRegular N (List.map (⇑(algebraMap R S)) tail✝)
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsSMulRegular M x ∧ IsWeaklyRegular (QuotSMulTop x M) tail✝
e : TensorProduct R S (QuotSMulTop x M) ≃ₗ[S] QuotSMulTop ((algebraMap R S) x) N
x✝ : QuotSMulTop x M
⊢ e (1 ⊗ₜ[R] x✝) = (↑R ↑e ∘ₗ (TensorProduct.mk R S (QuotSMulTop x M)) 1) x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Flat R S
x : R
tail✝ : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : Module R M] [inst_2 : AddCommGroup N]
    [inst_3 : Module R N] [inst_4 : Module S N] [inst_5 : IsScalarTower R S N] {f : M →ₗ[R] N},
    IsBaseChange S f → IsWeaklyRegular M tail✝ → IsWeaklyRegular N (List.map (⇑(algebraMap R S)) tail✝)
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsSMulRegular M x ∧ IsWeaklyRegular (QuotSMulTop x M) tail✝
e : TensorProduct R S (QuotSMulTop x M) ≃ₗ[S] QuotSMulTop ((algebraMap R S) x) N
hg : IsBaseChange S (↑R ↑e ∘ₗ (TensorProduct.mk R S (QuotSMulTop x M)) 1)
⊢ IsSMulRegular N ((algebraMap R S) x) ∧
    IsWeaklyRegular (QuotSMulTop ((algebraMap R S) x) N) (List.map (⇑(algebraMap R S)) tail✝)

Tactic:
exact ⟨reg.1.of_flat_of_isBaseChange hf, ih hg reg.2⟩

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.IsDistinguishedAt I
hI : I ≠ ⊤
⊢ ↑g = ↑g * 1

Tactic:
by 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⁻¹
key : f - g * q' = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
i✝ i : ℕ
⊢ i + n ≥ n

Tactic:
by 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✝ i : ℕ
⊢ i + ((map (Ideal.Quotient.mk I)) g).order.toNat ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsRegularRing R
⊢ IsRegularLocalRing R

Tactic:
let e : R ≃ₐ[R] (Localization.AtPrime (maximalIdeal R)) :=
    IsLocalization.atUnits R (maximalIdeal R).primeCompl (fun x ↦ by simpa using! fun a ↦ a)

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsRegularRing R
e : R ≃ₐ[R] Localization.AtPrime (maximalIdeal R) := IsLocalization.atUnits R (maximalIdeal R).primeCompl ⋯
⊢ IsRegularLocalRing R
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
heq : g * q = ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ (k + 1)

Tactic:
| succ k ih =>

Goal state after:
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))
⊢ False

Tactic:
have : x ∈ (Module.annihilator R (Ext M L (n + 1))).jacobson :=
        (IsLocalRing.maximalIdeal_le_jacobson _) mem

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
⊢ False
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
⊢ ↑g = ↑g * 1

Tactic:
by simp

Goal state after:
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 [← hz] using Submodule.smul_mem_pointwise_smul _ _ ⊤ trivial

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f : A⟦X⟧
inst✝ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
⊢ ¬(map (IsLocalRing.residue A)) 0 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
⊢ {(n, 0)} ⊆ Finset.antidiagonal n

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p.1 = n
⊢ (n, 0) ∈ Finset.antidiagonal n

Tactic:
by simp

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < f.natDegree
⊢ f.coeff i ∈ IsLocalRing.maximalIdeal A

Tactic:
rw [hfdeg] at hi
    simp_rw [f, Polynomial.coeff_sub, Polynomial.coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff]
    have := H.coeff_f_sub_r_mem hi
    rwa [map_sub, coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff, Polynomial.coeff_coe] at this

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N✝ : Type u_3
S : Type u_4
inst✝¹⁰ : CommSemiring R₀
inst✝⁹ : Ring R
inst✝⁸ : Algebra R₀ R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N✝
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
ι : Type u_5
inst✝ : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : ⨆ i, N i = ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : Module.End R M
x : M
⊢ ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm)
        ((fun f i ↦ LinearMap.restrict f ⋯) f))
      0 =
    f 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ IsSimpleRing R ∧ IsArtinianRing R ↔ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

Tactic:
by
  refine ⟨fun ⟨_, _⟩ ↦ ?_, fun ⟨_, _, _⟩ ↦ ?_⟩
  on_goal 1 => have := IsSimpleRing.isSemisimpleRing_iff_isArtinianRing.mpr ‹_›
  all_goals simp_rw [isIsotypic_iff_isFullyInvariant_imp_bot_or_top,
      isFullyInvariant_iff_isTwoSided, isSimpleRing_iff_isTwoSided_imp] at *
  · exact ⟨this, by rwa [and_comm]⟩
  · exact ⟨⟨‹_›, ‹_›⟩, inferInstance⟩

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case e_t.e_a
n : ℕ
⊢ (factors n).card = ArithmeticFunction.cardFactors n

Tactic:
simp [Nat.factors_eq, ArithmeticFunction.cardFactors_apply]

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
inj : Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))
comm1 :
  (↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f =
    f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)
⊢ f x = 0

Tactic:
f.mem_ker.mp hx.1

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
inj : Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))
comm1 :
  (↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f =
    f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)
⊢ 0 = 0