mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝² : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
x✝¹ : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this✝ : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x✝ : LocalizedModule.AtPrime p M
hx : maximalIdeal (Localization.AtPrime p) = ⊥.colon {x✝}
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
r : Rₚ
x : Nₚ'
⊢ g.toFun (r • x) = (RingHom.id Rₚ) r • g.toFun x

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
⊢ (if x✝¹ * x✝ = 0 ∧ n = 0 then 1 else 0) = x✝¹ ^ n * if x✝ = 0 ∧ n = 0 then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
hr : r ∈ I
hI : I • ⊤ ≠ ⊤
⊢ I • ⊤ ≠ ⊤

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
⊢ ((if x = 0 ∧ m = 0 then 1 else 0) * if x = 0 ∧ n = 0 then 1 else 0) =
    ↑((m + n).choose m) * if x = 0 ∧ m + n = 0 then 1 else 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
x✝ : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this✝ : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x : LocalizedModule.AtPrime p M
hx : maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField := to_res' ∘ₗ (maximalIdeal (Localization.AtPrime p) • ⊤).mkQ
⊢ ⊥.colon {x} = (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x).ker

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : a ∈ ⊥
⊢ (if (if a = 0 ∧ n = 0 then 1 else 0) = 0 ∧ m = 0 then 1 else 0) =
    ↑(m.uniformBell n) * if a = 0 ∧ m * n = 0 then 1 else 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : DecidableEq A
n : ℕ
a : A
⊢ (dividedPowersBot A).dpow n a = if a = 0 ∧ n = 0 then 1 else 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
⊢ hI = hI'

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h : (fun h ↦ h.dpow) hI = (fun h ↦ h.dpow) hI'
⊢ hI = hI'

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
hb : b ∈ I
⊢ hI.dpow n (a + b) = ∑ k ∈ range (n + 1), hI.dpow k a * hI.dpow (n - k) b

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
a b : A
dp : ℕ → A → A
dp_add : ∀ (n : ℕ), dp n (a + b) = ∑ k ∈ antidiagonal n, dp k.1 a * dp k.2 b
⊢ (PowerSeries.mk fun n ↦ dp n (a + b)) = (PowerSeries.mk fun n ↦ dp n a) * PowerSeries.mk fun n ↦ dp n b

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (b • a) = b ^ n • hI.dpow n a

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (a * b) = hI.dpow n a * b ^ n

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (a • b) = hI.dpow n a • b ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
i : ℕ
hi : i < n
⊢ i < n + 1

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ ↑n ! * hI.dpow n a = a ^ n

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
⊢ ↑n ! * hI.dpow n a = n • ↑(n - 1)! * hI.dpow n a

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
⊢ a ^ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
i : ℕ
hi : i < n
zero1 : IsZero (AddCommGrpCat.of (Ext N M i))
⊢ i + 1 < n + 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
x✝ : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this✝ : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField := to_res' ∘ₗ (maximalIdeal (Localization.AtPrime p) • ⊤).mkQ
hx :
  maximalIdeal (Localization.AtPrime p) = (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x).ker
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
inj1 : Function.Injective ⇑i
f : Nₚ →ₗ[Rₚ] Mₚ := i ∘ₗ to_res
⊢ f ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
⊢ ∀ i < n, Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
ha : a ∈ I • J
⊢ hI.dpow n a = hJ.dpow n a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
⊢ Subsingleton (N →ₗ[R] M) ↔ ∃ r ∈ annihilator R N, IsSMulRegular M r

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ ↑(C a) = (algebraMap R (DividedPowerAlgebra R M)) a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ (RingCon.mkₐ R (ringCon R M)) (C a) = (algebraMap R (DividedPowerAlgebra R M)) a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
n : ℕ
M : ModuleCat R
inst✝¹ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
N : ModuleCat R
inst✝ : Module.Finite R ↑N
h_supp : Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I
h_ext : ∀ i < n, Subsingleton (Ext N M i)
⊢ ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
⊢ P f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ dp R 0 m = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ dp R n (r • m) = r ^ n • dp R n m

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
s : Finset ι
n : ι → ℕ
ha : a ∈ I
⊢ ∏ i ∈ s, hI.dpow (n i) a = ↑(multinomial s n) * hI.dpow (s.sum n) a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ dp R n 0 = if n = 0 then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≠ 0
⊢ dp R n 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n p : ℕ
m : M
⊢ dp R n m * dp R p m = (n + p).choose n • dp R (n + p) m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ dp R n (x + y) = ∑ k ∈ antidiagonal n, dp R k.1 x * dp R k.2 y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
a : ι → R
x : ι → M
⊢ dp R q (∑ i ∈ s, a i • x i) =
    ∑ k ∈ s.sym q, (∏ i ∈ s, a i ^ Multiset.count i ↑k) • ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)

Tactic:
by

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

Goal state before:
pp: R : Type u_7
inst✝² : CommSemiring R
r : R
rs : List R
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ ofList (r :: rs) • N = r • N ⊔ ofList rs • N

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
r : R
rs : List R
⊢ map (r • ⊤).mkQ (Ideal.ofList rs • ⊤) = Ideal.ofList rs • ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
r : R
rs : List R
⊢ map (Ideal.ofList rs • ⊤).mkQ (r • ⊤) = r • ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
n : ι → ℕ
m : M
⊢ ∏ i ∈ s, dp R (n i) m = ↑(multinomial s n) * dp R (s.sum n) m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
⊢ i < n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ ⊤ = Ideal.ofList (r :: rs) • ⊤ ↔ ⊤ = Ideal.ofList rs • ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
⊢ Mono g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : M
⊢ ↑n ! * dp R n x = dp R 1 x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ x✝ : M
⊢ dp R 1 (x✝¹ + x✝) = dp R 1 x✝¹ + dp R 1 x✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ : R
x✝ : M
⊢ dp R 1 (x✝¹ • x✝) = (RingHom.id R) x✝¹ • dp R 1 x✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : f = g
x✝¹ : ℕ
x✝ : M
⊢ f (dp R x✝¹ x✝) = g (dp R x✝¹ x✝)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
mono_g : Mono g
gk : AddCommGrpCat.of (Ext N (M.smulShortComplex (a ^ k)).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex (a ^ k)).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex (a ^ k)).f).postcomp N ⋯)
⊢ Mono gk

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g ↔ ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
r : R
⊢ (fun n ↦ n.prod fun i k ↦ dp R k (v i)) 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
x : DividedPowerAlgebra R M
k : ℕ
m : M
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ m ∈ Submodule.span R (Set.range v)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : (i : Fin n.succ) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a ↦ s.sym (n - ↑a)
⊢ Sym.fill a m.fst m.snd ∈ (insert a s).sym n

Tactic:
by

Goal state after: