mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem.add
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) = ⊤
m : M
x✝ : DividedPowerAlgebra R M
k : ℕ
i : ι
x y : DividedPowerAlgebra R M
hxmem : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hymem : y ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hx : x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hy : y * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ x * dp R k (v i) + y * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
]

Goal state after:
case dp.mem.add
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) = ⊤
m : M
x✝ : DividedPowerAlgebra R M
k : ℕ
i : ι
x y : DividedPowerAlgebra R M
hxmem : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hymem : y ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hx : x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hy : y * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ x * dp R k (v i) + y * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
⊢ map f I ≤ J →
    ((∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)) ↔
      ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a))

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
⊢ map f I ≤ J →
    ((∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)) ↔
      ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a))
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : n = 0
a✝ : A
ha : a✝ ∈ I
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : n = 0
⊢ ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)

pp: case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : ¬n = 0
⊢ ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)

Tactic:
· intro _ ha
    rw [hn, hI.dpow_zero ha, hJ.dpow_zero (hIJ (mem_map_of_mem f ha)), map_one]

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : ¬n = 0
⊢ ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
C : Type u_3
inst✝ : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
n✝ : ℕ
a : A
ha : a ∈ I
⊢ g (hJ.dpow n✝ (f a)) = g (hJ.dpow n✝ (f a))

pp: case a
A : Type u_1
B : Type u_2
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
C : Type u_3
inst✝ : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
n✝ : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ J

Tactic:
]

Goal state after:
case a
A : Type u_1
B : Type u_2
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
C : Type u_3
inst✝ : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
n✝ : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ J
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem.smul
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) = ⊤
m : M
x✝ : DividedPowerAlgebra R M
k : ℕ
i : ι
r : R
x : DividedPowerAlgebra R M
hxmem : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hx : x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ r • (x * dp R k (v i)) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
]

Goal state after:
case dp.mem.smul
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) = ⊤
m : M
x✝ : DividedPowerAlgebra R M
k : ℕ
i : ι
r : R
x : DividedPowerAlgebra R M
hxmem : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hx : x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ r • (x * dp R k (v i)) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case insert.h
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 : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ dpow (Multiset.count a ↑m) (x a) * ∏ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) =
    dpow (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)

Tactic:
]

Goal state after:
case insert.h
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 : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ dpow (Multiset.count a ↑m) (x a) * ∏ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) =
    dpow (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case mk.mk
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' : ⇑toRingHom✝¹ = ⇑toRingHom✝
x✝ : A
⊢ toRingHom✝ x✝ = toRingHom✝ x✝

Tactic:
]

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

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
h : f.comp ((toAddMonoidEnd R M) r) = AddMonoidHom.comp ((toAddMonoidEnd S M₂) s) f
⊢ AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup =
    AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup

Tactic:
]

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

Goal state before:
pp: case dp.add
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) = ⊤
m✝ m n : M
hm_mem : m ∈ Submodule.span R (Set.range v)
hn_mem : n ∈ Submodule.span R (Set.range v)
hm :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k m ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hn :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ ∑ i ∈ antidiagonal k, x * (dp R i.1 m * dp R i.2 n) ∈
    Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
]

Goal state after:
case dp.add
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) = ⊤
m✝ m n : M
hm_mem : m ∈ Submodule.span R (Set.range v)
hn_mem : n ∈ Submodule.span R (Set.range v)
hm :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k m ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hn :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ ∑ i ∈ antidiagonal k, x * (dp R i.1 m * dp R i.2 n) ∈
    Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
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) = ⊤
m✝ m n : M
hm_mem : m ∈ Submodule.span R (Set.range v)
hn_mem : n ∈ Submodule.span R (Set.range v)
hm :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k m ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hn :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
c : ℕ × ℕ
hc : c ∈ antidiagonal k
⊢ x * dp R c.1 m * dp R c.2 n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
]

Goal state after:
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) = ⊤
m✝ m n : M
hm_mem : m ∈ Submodule.span R (Set.range v)
hn_mem : n ∈ Submodule.span R (Set.range v)
hm :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k m ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hn :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
c : ℕ × ℕ
hc : c ∈ antidiagonal k
⊢ x * dp R c.1 m * dp R c.2 n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
a✝ b✝ : A
hx : a✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n a✝) = hJ.dpow n (f a✝)
hy : b✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n b✝) = hJ.dpow n (f b✝)
n : ℕ
⊢ ∑ x ∈ Finset.antidiagonal n, f (hI.dpow x.1 a✝ * hI.dpow x.2 b✝) =
    ∑ k ∈ Finset.antidiagonal n, hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝)

Tactic:
]

Goal state after:
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
a✝ b✝ : A
hx : a✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n a✝) = hJ.dpow n (f a✝)
hy : b✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n b✝) = hJ.dpow n (f b✝)
n : ℕ
⊢ ∑ x ∈ Finset.antidiagonal n, f (hI.dpow x.1 a✝ * hI.dpow x.2 b✝) =
    ∑ k ∈ Finset.antidiagonal n, hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
k : ℕ
⊢ ↑(Nat.multinomial univ fun _i ↦ n) * dp R (∑ _i, n) m = ↑(Nat.multinomial (range k) fun x ↦ n) * dp R (k * n) m

Tactic:
]

Goal state after:
R : Type u_4
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
k : ℕ
⊢ ↑(Nat.multinomial univ fun _i ↦ n) * dp R (∑ _i, n) m = ↑(Nat.multinomial (range k) fun x ↦ n) * dp R (k * n) m
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
a✝ b✝ : A
hx : a✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n a✝) = hJ.dpow n (f a✝)
hy : b✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n b✝) = hJ.dpow n (f b✝)
n : ℕ
k : ℕ × ℕ
⊢ hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝) = hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝)

Tactic:
]

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 : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
p q : MvPolynomial (ℕ × M) R
h : Rel R M p q
⊢ (eval₂AlgHom R f) p = (eval₂AlgHom R f) q

Tactic:
rcases h <;>
  simp_all

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

Goal state before:
pp: case zero
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
⊢ 1 = 1

Tactic:
]

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
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
⊢ Rel R M ≤ ⇑(RingCon.ker (eval₂AlgHom R f).toRingHom)

Tactic:
]

Goal state after:
α : Type u_1
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 : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
⊢ Rel R M ≤ ⇑(RingCon.ker (eval₂AlgHom R f).toRingHom)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case succ
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
n : ℕ
a✝ : f (hI.dpow n 0) = hJ.dpow n 0
⊢ 0 = 0

Tactic:
]

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 : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
m : M
⊢ f (n, m) = f (n, m)

Tactic:
]

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 : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ s = s

Tactic:
]

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
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
n : ℕ
r : R
m : M
⊢ r ^ n • hI.dpow n (g m) = r ^ n • hI.dpow n (g m)

Tactic:
]

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
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
n p : ℕ
m : M
⊢ ((n, m).1 + (p, m).1).choose (n, m).1 • hI.dpow ((n, m).1 + (p, m).1) (g m) =
    (n + p).choose n • hI.dpow (n + p, m).1 (g (n + p, m).2)

Tactic:
]

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

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx : x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
n : ℕ
⊢ f r ^ n * hJ.dpow n (f x) = f r ^ n * hJ.dpow n (f x)

Tactic:
]

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
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
p : MvPolynomial (ℕ × M) R
⊢ (aeval fun nm ↦ hI.dpow nm.1 (g nm.2)) p = (aeval fun nm ↦ hI.dpow nm.1 (g nm.2)) p

Tactic:
]

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

Goal state before:
pp: A : Type u_1
inst✝³ : CommSemiring A
ι : Type u_2
inst✝² : DecidableEq ι
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
⊢ ∑ k ∈ x.support.sym n, ∏ i ∈ x.support, hJ.dpow (Multiset.count i ↑k) (x i • b i) =
    ∑ k ∈ x.support.sym n, x.prod fun i r ↦ r ^ Multiset.count i ↑k • hJ.dpow (Multiset.count i ↑k) (b i)

Tactic:
]

Goal state after:
A : Type u_1
inst✝³ : CommSemiring A
ι : Type u_2
inst✝² : DecidableEq ι
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
⊢ ∑ k ∈ x.support.sym n, ∏ i ∈ x.support, hJ.dpow (Multiset.count i ↑k) (x i • b i) =
    ∑ k ∈ x.support.sym n, x.prod fun i r ↦ r ^ Multiset.count i ↑k • hJ.dpow (Multiset.count i ↑k) (b i)
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
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
n : ℕ
m : M
⊢ hI.dpow (n, m).1 (g (n, m).2) = hI.dpow n (g m)

Tactic:
]

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
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), f (dp R n m) = hI.dpow n (g m)
x✝¹ : ℕ
x✝ : M
⊢ hI.dpow x✝¹ (g x✝) = hI.dpow x✝¹ (g x✝)

Tactic:
]

Goal state after: