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

State before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
⊢ dpow hI hJ n x = 0
Tactic:
simp only [dpow]
State after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
⊢ Function.extend (fun x => ↑x.1 + ↑x.2) (fun x => ∑ k ∈ range (n + 1), hI.dpow k ↑x.1 * hJ.dpow (n - k) ↑x.2)
      (Function.const A 0) x =
    0

State before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
⊢ Function.extend (fun x => ↑x.1 + ↑x.2) (fun x => ∑ k ∈ range (n + 1), hI.dpow k ↑x.1 * hJ.dpow (n - k) ↑x.2)
      (Function.const A 0) x =
    0
Tactic:
rw [Function.extend_apply']
State after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
⊢ Function.const A 0 x = 0

case hb
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
⊢ ¬∃ a, ↑a.1 + ↑a.2 = x

State before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
⊢ Function.const A 0 x = 0

case hb
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
⊢ ¬∃ a, ↑a.1 + ↑a.2 = x
Tactic:
rfl
State after:
case hb
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
⊢ ¬∃ a, ↑a.1 + ↑a.2 = x

State before:
case hb
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
⊢ ¬∃ a, ↑a.1 + ↑a.2 = x
Tactic:
rintro ⟨⟨⟨a, ha⟩, ⟨b, hb⟩⟩, h⟩
State after:
case hb.intro.mk.mk.mk
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : ↑(⟨a, ha⟩, ⟨b, hb⟩).1 + ↑(⟨a, ha⟩, ⟨b, hb⟩).2 = x
⊢ False

State before:
case hb.intro.mk.mk.mk
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : ↑(⟨a, ha⟩, ⟨b, hb⟩).1 + ↑(⟨a, ha⟩, ⟨b, hb⟩).2 = x
⊢ False
Tactic:
apply hx
State after:
case hb.intro.mk.mk.mk
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : ↑(⟨a, ha⟩, ⟨b, hb⟩).1 + ↑(⟨a, ha⟩, ⟨b, hb⟩).2 = x
⊢ x ∈ I + J

State before:
case hb.intro.mk.mk.mk
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : ↑(⟨a, ha⟩, ⟨b, hb⟩).1 + ↑(⟨a, ha⟩, ⟨b, hb⟩).2 = x
⊢ x ∈ I + J
Tactic:
rw [← h]
State after:
case hb.intro.mk.mk.mk
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : ↑(⟨a, ha⟩, ⟨b, hb⟩).1 + ↑(⟨a, ha⟩, ⟨b, hb⟩).2 = x
⊢ ↑(⟨a, ha⟩, ⟨b, hb⟩).1 + ↑(⟨a, ha⟩, ⟨b, hb⟩).2 ∈ I + J

State before:
case hb.intro.mk.mk.mk
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
x : A
hx : x ∉ I + J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : ↑(⟨a, ha⟩, ⟨b, hb⟩).1 + ↑(⟨a, ha⟩, ⟨b, hb⟩).2 = x
⊢ ↑(⟨a, ha⟩, ⟨b, hb⟩).1 + ↑(⟨a, ha⟩, ⟨b, hb⟩).2 ∈ I + J
Tactic:
exact Submodule.add_mem_sup ha hb
State after:
no goals