mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ map R (g ∘ₗ f) = (map R g).comp (map R 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
⊢ map R LinearMap.id = AlgHom.id R (DividedPowerAlgebra R M)

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
S : Type u_4
inst✝⁷ : CommSemiring S
N : Type u_5
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
f : M →ₗ[R] N
inst✝³ : Algebra R S
inst✝² : IsScalarTower R S N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : M ≃ₗ[R] N
⊢ (map R ↑g).comp (map R ↑g.symm) = AlgHom.id R (DividedPowerAlgebra R 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
⊢ IsRegular M (r :: rs) ↔
    IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)

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
S : Type u_4
inst✝⁷ : CommSemiring S
N : Type u_5
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
f : M →ₗ[R] N
inst✝³ : Algebra R S
inst✝² : IsScalarTower R S N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : M ≃ₗ[R] N
⊢ (map R ↑g.symm).comp (map R ↑g) = AlgHom.id R (DividedPowerAlgebra R 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
hI : DividedPowers I
ι : Type u_3
r : ι → A
s : Finset ι
hs : s.Nonempty
hs' : ∀ i ∈ s, r i ∈ I
n : ℕ
⊢ hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
m : ℕ
x : A
hx : x ∈ I
⊢ dpow I m x = (↑m !)⁻¹ʳ * x ^ m

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
m : ℕ
x : A
hx : x ∉ I
⊢ dpow I m x = 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
x : A
hx : x ∈ I
⊢ dpow I 0 x = 1

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
x : A
hx : x ∈ I
⊢ dpow I 1 x = x

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
⊢ dpow I m x ∈ I

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ : B
hx : x✝ ∉ J
⊢ e (hI.dpow n✝ (e.symm x✝)) = 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x✝ : B
hx : x✝ ∈ J
⊢ e (hI.dpow 0 (e.symm x✝)) = 1

Tactic:
by

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

Goal state before:
pp: A : Type u_3
B : Type u_4
C : Type u_5
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
⊢ hJ.IsDPMorphism hK g

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
rs₁ rs₂ : List R
⊢ IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂

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
inst✝ : Nontrivial M
h : ⊤ = Ideal.ofList [] • ⊤
⊢ False

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x✝ : B
hx : x✝ ∈ J
⊢ e (hI.dpow 1 (e.symm x✝)) = x✝

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ : B
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ e (hI.dpow n✝ (e.symm x✝)) ∈ J

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
inst✝ : IsArtinian R M
r : R
rs : List R
h : IsRegular M (r :: rs)
⊢ r :: rs = []

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module.Flat R M₂
rs : List R
h : IsWeaklyRegular M rs
⊢ IsWeaklyRegular (M₂ ⊗[R] M) rs

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ y✝ : B
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ e (hI.dpow n✝ (e.symm (x✝ + y✝))) = ∑ k ∈ antidiagonal n✝, e (hI.dpow k.1 (e.symm x✝)) * e (hI.dpow k.2 (e.symm y✝))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module.Flat R M₂
rs : List R
h : IsWeaklyRegular M rs
⊢ IsWeaklyRegular (M ⊗[R] M₂) rs

Tactic:
by

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

Goal state before:
pp: case e_a.e_a
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ ↑(m.choose k.1) = ↑m ! * (↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ

Tactic:
exact castChoose_eq (hn_fac.natCast_factorial_of_lt hmn) hk

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
a✝ x✝ : B
hx : x✝ ∈ J
⊢ e (hI.dpow n✝ (e.symm (a✝ * x✝))) = a✝ ^ n✝ * e (hI.dpow n✝ (e.symm x✝))

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y

Tactic:
by

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

Goal state before:
pp: A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
⊢ hI' = hI

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m✝ n✝ : ℕ
x✝ : B
hx : x✝ ∈ J
⊢ e (hI.dpow m✝ (e.symm x✝)) * e (hI.dpow n✝ (e.symm x✝)) = ↑((m✝ + n✝).choose m✝) * e (hI.dpow (m✝ + n✝) (e.symm x✝))

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n✝ : ℕ
x✝ : A
hx : x✝ ∉ I
⊢ (if hx : x✝ ∈ I then ⋯.choose else 0) = 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
x : A
hx : x ∈ I
⊢ (if hx : x ∈ I then ⋯.choose else 0) = 1

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
x✝ : A
hx : x✝ ∈ I
⊢ (if hx : x✝ ∈ I then ⋯.choose else 0) = x✝

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
x : A
hn : n ≠ 0
hx : x ∈ I
⊢ (if hx : x ∈ I then ⋯.choose else 0) ∈ I

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ (if hx : x + y ∈ I then ⋯.choose else 0) =
    ∑ k ∈ Finset.antidiagonal n, (if hx : x ∈ I then ⋯.choose else 0) * if hx : y ∈ I then ⋯.choose else 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
a x : A
hx : x ∈ I
⊢ (if hx : a * x ∈ I then ⋯.choose else 0) = a ^ n * if hx : x ∈ I then ⋯.choose else 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
⊢ (x + y) ^ m = 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
m✝ n✝ : ℕ
x✝ : A
hx : x✝ ∈ I
⊢ ((if hx : x✝ ∈ I then ⋯.choose else 0) * if hx : x✝ ∈ I then ⋯.choose else 0) =
    ↑((m✝ + n✝).choose m✝) * if hx : x✝ ∈ I then ⋯.choose else 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m✝ n✝ : ℕ
x✝ : B
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ e (hI.dpow m✝ (e.symm (e (hI.dpow n✝ (e.symm x✝))))) = ↑(m✝.uniformBell n✝) * e (hI.dpow (m✝ * n✝) (e.symm x✝))

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a : A
⊢ (ofRingEquiv h hI).dpow n (e a) = e (hI.dpow n a)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
⊢ ofRingEquiv ⋯ (ofRingEquiv h hI) = hI

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hJ : DividedPowers J
⊢ ofRingEquiv h (ofRingEquiv ⋯ hJ) = hJ

Tactic:
by

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

Goal state before:
pp: case cons
R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs✝ : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
r : R
rs : List R
h₄ : IsSMulRegular M✝ r
h2✝ : IsWeaklyRegular (QuotSMulTop r M✝) rs
ih :
  ∀ {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂]
    [inst_2 : AddCommGroup M₃] [inst_3 : Module R M] [inst_4 : Module R M₂] [inst_5 : Module R M₃] {f₁ : M →ₗ[R] M₂}
    {f₂ : M₂ →ₗ[R] M₃} {f₃ : M₃ →ₗ[R] QuotSMulTop r M✝},
    Exact ⇑f₁ ⇑f₂ →
      Exact ⇑f₂ ⇑f₃ →
        Surjective ⇑f₃ →
          Exact ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₁ ⋯)
            ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₂ ⋯)
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
⊢ Exact ⇑((Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₁ ⋯)
    ⇑((Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₂ ⋯)

Tactic:
| cons r rs h₄ _ ih =>

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
⊢ (if hx : (if hx : x ∈ I then ⋯.choose else 0) ∈ I then ⋯.choose else 0) =
    ↑(n.uniformBell m) * if hx : x ∈ I then ⋯.choose else 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
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✝⁵ : AddCommGroup M₃
inst✝⁴ : AddCommGroup M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
rs : List R
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M₄
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
h₄ : IsWeaklyRegular M₄ rs
⊢ Exact ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₁ ⋯)
    ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₂ ⋯)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
m : ℕ
a x : A
hx : x ∈ I
⊢ dpow I m (a * x) = a ^ m * dpow I m x

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
n✝ : ℕ
x✝ : A
hx : x✝ ∉ J
⊢ (if x✝ ∈ J then hI.dpow n✝ x✝ else 0) = 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
x✝ : A
hx : x✝ ∈ J
⊢ (if x✝ ∈ J then hI.dpow 0 x✝ else 0) = 1

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
⊢ ↑(padicValNat p n !) < ↑n

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
x✝ : A
hx : x✝ ∈ J
⊢ (if x✝ ∈ J then hI.dpow 1 x✝ else 0) = x✝

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
n✝ : ℕ
x✝ : A
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ (if x✝ ∈ J then hI.dpow n✝ x✝ else 0) ∈ J

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
⊢ 0 < ‖↑n !‖

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
n✝ : ℕ
x✝ y✝ : A
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ (if x✝ + y✝ ∈ J then hI.dpow n✝ (x✝ + y✝) else 0) =
    ∑ k ∈ Finset.antidiagonal n✝, (if x✝ ∈ J then hI.dpow k.1 x✝ else 0) * if y✝ ∈ J then hI.dpow k.2 y✝ else 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
n✝ : ℕ
a✝ x✝ : A
hx : x✝ ∈ J
⊢ (if a✝ * x✝ ∈ J then hI.dpow n✝ (a✝ * x✝) else 0) = a✝ ^ n✝ * if x✝ ∈ J then hI.dpow n✝ x✝ else 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
m✝ n✝ : ℕ
x✝ : A
hx : x✝ ∈ J
⊢ ((if x✝ ∈ J then hI.dpow m✝ x✝ else 0) * if x✝ ∈ J then hI.dpow n✝ x✝ else 0) =
    ↑((m✝ + n✝).choose m✝) * if x✝ ∈ J then hI.dpow (m✝ + n✝) x✝ else 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
m✝ n✝ : ℕ
x✝ : A
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ (if (if x✝ ∈ J then hI.dpow n✝ x✝ else 0) ∈ J then hI.dpow m✝ (if x✝ ∈ J then hI.dpow n✝ x✝ else 0) else 0) =
    ↑(m✝.uniformBell n✝) * if x✝ ∈ J then hI.dpow (m✝ * n✝) x✝ else 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
n : ℕ
a : A
ha : a ∈ J
⊢ (dividedPowers hI hJ).dpow n a = hI.dpow n a

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

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
a b : R
h1 : IsWeaklyRegular M [a, b]
h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥
⊢ IsWeaklyRegular M [b, a]

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
by
  have hm : m < n := lt_of_le_of_lt le_self_add hkm
  have hk : k < n := lt_of_le_of_lt le_add_self hkm
  rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx,
    mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m),
    ← pow_add, ← mul_assoc, ← mul_assoc]
  apply congr_arg₂ _ _ rfl
  rw [eq_mul_inverse_iff_mul_eq _ _ _ (hn_fac.natCast_factorial_of_lt hkm),
      mul_assoc,
      inverse_mul_eq_iff_eq_mul _ _ _ (hn_fac.natCast_factorial_of_lt hm),
      inverse_mul_eq_iff_eq_mul _ _ _ (hn_fac.natCast_factorial_of_lt hk)]
  norm_cast; apply congr_arg
  rw [← Nat.add_choose_mul_factorial_mul_factorial, mul_comm, mul_comm _ (m !), Nat.choose_symm_add]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
inst✝ : (x : A) → Decidable (x ∈ J)
hJ : hI.IsSubDPIdeal J
x✝² : ℕ
x✝¹ : x✝² ≠ 0
x✝ : A
ha : x✝ ∈ J
⊢ hI.dpow x✝² x✝ = (dividedPowers hI hJ).dpow x✝² x✝

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
inst✝ : (x : A) → Decidable (x ∈ J)
hJ : hI.IsSubDPIdeal J
⊢ (dividedPowers hI hJ).IsDPMorphism hI (RingHom.id A)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ‖dpow' p n ↑x‖ ≤ (↑p)⁻¹

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
⊢ hI.IsSubDPIdeal (J ⊓ I) ↔ ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ‖dpow' p n ↑x‖ ≤ 1

Tactic:
by

Goal state after: