Theorem: DividedPowers.IdealAdd.dpow_mem (DividedPowers/IdealAdd.lean)

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 : A
hn : n ≠ 0
hx : x ∈ I + J
⊢ dpow hI hJ n x ∈ I + J
Tactic:
rw [Ideal.add_eq_sup, Submodule.mem_sup] at hx
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 : A
hn : n ≠ 0
hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x
⊢ dpow hI hJ n x ∈ I + J

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 : A
hn : n ≠ 0
hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x
⊢ dpow hI hJ n x ∈ I + J
Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := hx
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
⊢ dpow hI hJ n (a + b) ∈ I + J

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
⊢ dpow hI hJ n (a + b) ∈ I + J
Tactic:
rw [dpow_eq hI hJ hIJ _ ha hb]
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 ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b ∈ I + J

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 ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b ∈ I + J
Tactic:
apply Submodule.sum_mem (I ⊔ J)
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
⊢ ∀ c ∈ range (n + 1), hI.dpow c a * hJ.dpow (n - c) b ∈ I ⊔ J

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 _
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

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
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

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]
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals