internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.IdealAdd.dpow_mem
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ c ∈ range (n + 1), hI.dpow c a * hJ.dpow (n - c) b ∈ I ⊔ J
Tactic:
intro k _
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ hI.dpow k a * hJ.dpow (n - k) b ∈ I ⊔ J
Theorem: DividedPowers.IdealAdd.dpow_mem
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ hI.dpow k a * hJ.dpow (n - k) b ∈ I ⊔ J
Tactic:
by_cases hk0 : k = 0
Proof state after:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : k = 0
⊢ hI.dpow k a * hJ.dpow (n - k) b ∈ I ⊔ J

case neg
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : ¬k = 0
⊢ hI.dpow k a * hJ.dpow (n - k) b ∈ I ⊔ J
Theorem: DividedPowers.IdealAdd.dpow_mem
Proof state before:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : k = 0
⊢ hI.dpow k a * hJ.dpow (n - k) b ∈ I ⊔ J
Tactic:
rw [hk0]
Proof state after:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : k = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ I ⊔ J
Theorem: DividedPowers.IdealAdd.dpow_mem
Proof state before:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : k = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ I ⊔ J
Tactic:
apply Submodule.mem_sup_right
Proof state after:
case pos.a
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : k = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ J
Theorem: DividedPowers.IdealAdd.dpow_mem
Proof state before:
case pos.a
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : k = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ J
Tactic:
apply Ideal.mul_mem_left
Proof state after:
case pos.a.a
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : k = 0
⊢ hJ.dpow (n - 0) b ∈ J
Theorem: DividedPowers.IdealAdd.dpow_mem
Proof state before:
case pos.a.a
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : k = 0
⊢ hJ.dpow (n - 0) b ∈ J
Tactic:
exact hJ.dpow_mem hn hb
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_mem
Proof state before:
case neg
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : ¬k = 0
⊢ hI.dpow k a * hJ.dpow (n - k) b ∈ I ⊔ J
Tactic:
apply Submodule.mem_sup_left
Proof state after:
case neg.a
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : ¬k = 0
⊢ hI.dpow k a * hJ.dpow (n - k) b ∈ I
Theorem: DividedPowers.IdealAdd.dpow_mem
Proof state before:
case neg.a
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : ¬k = 0
⊢ hI.dpow k a * hJ.dpow (n - k) b ∈ I
Tactic:
apply Ideal.mul_mem_right
Proof state after:
case neg.a.h
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : ¬k = 0
⊢ hI.dpow k a ∈ I
Theorem: DividedPowers.IdealAdd.dpow_mem
Proof state before:
case neg.a.h
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
hk0 : ¬k = 0
⊢ hI.dpow k a ∈ I
Tactic:
exact hI.dpow_mem hk0 ha
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
⊢ ∀ (n : ℕ) {c x : A}, x ∈ I + J → dpow hI hJ n (c * x) = c ^ n * dpow hI hJ n x
Tactic:
intro n c x
Proof state after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c x : A
⊢ x ∈ I + J → dpow hI hJ n (c * x) = c ^ n * dpow hI hJ n x
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c x : A
⊢ x ∈ I + J → dpow hI hJ n (c * x) = c ^ n * dpow hI hJ n x
Tactic:
rw [Ideal.add_eq_sup, Submodule.mem_sup]
Proof state after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c x : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → dpow hI hJ n (c * x) = c ^ n * dpow hI hJ n x
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c x : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → dpow hI hJ n (c * x) = c ^ n * dpow hI hJ n x
Tactic:
rintro ⟨a, ha, b, hb, rfl⟩
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * (a + b)) = c ^ n * dpow hI hJ n (a + b)
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * (a + b)) = c ^ n * dpow hI hJ n (a + b)
Tactic:
rw [dpow_eq hI hJ hIJ n ha hb]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * (a + b)) = c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * (a + b)) = c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
rw [mul_add]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * a + c * b) = c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * a + c * b) = c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
rw [dpow_eq hI hJ hIJ n (Ideal.mul_mem_left I c ha) (Ideal.mul_mem_left J c hb)]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) =
    c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) =
    c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
rw [Finset.mul_sum]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) =
    ∑ i ∈ range (n + 1), c ^ n * (hI.dpow i a * hJ.dpow (n - i) b)
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) =
    ∑ i ∈ range (n + 1), c ^ n * (hI.dpow i a * hJ.dpow (n - i) b)
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ x ∈ range (n + 1), hI.dpow x (c * a) * hJ.dpow (n - x) (c * b) = c ^ n * (hI.dpow x a * hJ.dpow (n - x) b)
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ x ∈ range (n + 1), hI.dpow x (c * a) * hJ.dpow (n - x) (c * b) = c ^ n * (hI.dpow x a * hJ.dpow (n - x) b)
Tactic:
intro k hk
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ∈ range (n + 1)
⊢ hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ∈ range (n + 1)
⊢ hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)
Tactic:
simp only [Finset.mem_range, Nat.lt_succ_iff] at hk
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)
Tactic:
rw [hI.dpow_smul]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
rw [hJ.dpow_smul]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * (c ^ (n - k) * hJ.dpow (n - k) b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * (c ^ (n - k) * hJ.dpow (n - k) b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
simp only [← mul_assoc]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * c ^ (n - k) * hJ.dpow (n - k) b = c ^ n * hI.dpow k a * hJ.dpow (n - k) b

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * c ^ (n - k) = c ^ n * hI.dpow k a

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
rw [mul_comm, ← mul_assoc]
Proof state after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ (n - k) * c ^ k * hI.dpow k a = c ^ n * hI.dpow k a

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ (n - k) * c ^ k = c ^ n

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
rw [← pow_add, Nat.sub_add_cancel hk]
Proof state after:
case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
exact hb
Proof state after:
case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Theorem: DividedPowers.IdealAdd.dpow_smul
Proof state before:
case intro.intro.intro.intro.x
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
exact ha
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ k ∈ range (n + 1), dpow hI hJ k x * dpow hI hJ (n - k) y
Tactic:
intro n x y
Proof state after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
x y : A
⊢ x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ k ∈ range (n + 1), dpow hI hJ k x * dpow hI hJ (n - k) y
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
x y : A
⊢ x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ k ∈ range (n + 1), dpow hI hJ k x * dpow hI hJ (n - k) y
Tactic:
rw [Ideal.add_eq_sup, Submodule.mem_sup]
Proof state after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
x y : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) →
    y ∈ I ⊔ J → dpow hI hJ n (x + y) = ∑ k ∈ range (n + 1), dpow hI hJ k x * dpow hI hJ (n - k) y
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
x y : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) →
    y ∈ I ⊔ J → dpow hI hJ n (x + y) = ∑ k ∈ range (n + 1), dpow hI hJ k x * dpow hI hJ (n - k) y
Tactic:
rintro ⟨a, ha, b, hb, rfl⟩
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
y a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ y ∈ I ⊔ J → dpow hI hJ n (a + b + y) = ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) y