Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right (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
hx : x ∈ J
⊢ dpow hI hJ n x = hJ.dpow n x
Tactic:
rw [← zero_add x]
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
hx : x ∈ J
⊢ dpow hI hJ n (0 + x) = hJ.dpow n (0 + x)

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
hx : x ∈ J
⊢ dpow hI hJ n (0 + x) = hJ.dpow n (0 + x)
Tactic:
rw [dpow_eq hI hJ hIJ n I.zero_mem 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
hx : x ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k 0 * hJ.dpow (n - k) x = hJ.dpow n (0 + x)

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
hx : x ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k 0 * hJ.dpow (n - k) x = hJ.dpow n (0 + x)
Tactic:
rw [Finset.sum_eq_single 0]
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
hx : x ∈ J
⊢ hI.dpow 0 0 * hJ.dpow (n - 0) x = hJ.dpow n (0 + x)

case 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 : ℕ
x : A
hx : x ∈ J
⊢ ∀ b ∈ range (n + 1), b ≠ 0 → hI.dpow b 0 * hJ.dpow (n - b) x = 0

case 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 : ℕ
x : A
hx : x ∈ J
⊢ 0 ∉ range (n + 1) → hI.dpow 0 0 * hJ.dpow (n - 0) x = 0

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
hx : x ∈ J
⊢ hI.dpow 0 0 * hJ.dpow (n - 0) x = hJ.dpow n (0 + x)
Tactic:
simp only [Nat.sub_zero, zero_add, hI.dpow_zero I.zero_mem, one_mul]
State after:
no goals

State before:
case 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 : ℕ
x : A
hx : x ∈ J
⊢ ∀ b ∈ range (n + 1), b ≠ 0 → hI.dpow b 0 * hJ.dpow (n - b) x = 0
Tactic:
intro b _ hb'
State after:
case 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 : ℕ
x : A
hx : x ∈ J
b : ℕ
a✝ : b ∈ range (n + 1)
hb' : b ≠ 0
⊢ hI.dpow b 0 * hJ.dpow (n - b) x = 0

State before:
case 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 : ℕ
x : A
hx : x ∈ J
b : ℕ
a✝ : b ∈ range (n + 1)
hb' : b ≠ 0
⊢ hI.dpow b 0 * hJ.dpow (n - b) x = 0
Tactic:
rw [hI.dpow_eval_zero, MulZeroClass.zero_mul]
State after:
case 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 : ℕ
x : A
hx : x ∈ J
b : ℕ
a✝ : b ∈ range (n + 1)
hb' : b ≠ 0
⊢ b ≠ 0

State before:
case 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 : ℕ
x : A
hx : x ∈ J
b : ℕ
a✝ : b ∈ range (n + 1)
hb' : b ≠ 0
⊢ b ≠ 0
Tactic:
exact hb'
State after:
no goals

State before:
case 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 : ℕ
x : A
hx : x ∈ J
⊢ 0 ∉ range (n + 1) → hI.dpow 0 0 * hJ.dpow (n - 0) x = 0
Tactic:
intro hn
State after:
case 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 : ℕ
x : A
hx : x ∈ J
hn : 0 ∉ range (n + 1)
⊢ hI.dpow 0 0 * hJ.dpow (n - 0) x = 0

State before:
case 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 : ℕ
x : A
hx : x ∈ J
hn : 0 ∉ range (n + 1)
⊢ hI.dpow 0 0 * hJ.dpow (n - 0) x = 0
Tactic:
exfalso
State after:
case 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 : ℕ
x : A
hx : x ∈ J
hn : 0 ∉ range (n + 1)
⊢ False

State before:
case 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 : ℕ
x : A
hx : x ∈ J
hn : 0 ∉ range (n + 1)
⊢ False
Tactic:
apply hn
State after:
case 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 : ℕ
x : A
hx : x ∈ J
hn : 0 ∉ range (n + 1)
⊢ 0 ∈ range (n + 1)

State before:
case 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 : ℕ
x : A
hx : x ∈ J
hn : 0 ∉ range (n + 1)
⊢ 0 ∈ range (n + 1)
Tactic:
rw [Finset.mem_range]
State after:
case 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 : ℕ
x : A
hx : x ∈ J
hn : 0 ∉ range (n + 1)
⊢ 0 < n + 1

State before:
case 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 : ℕ
x : A
hx : x ∈ J
hn : 0 ∉ range (n + 1)
⊢ 0 < n + 1
Tactic:
exact NeZero.pos (n + 1)
State after:
no goals