Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left (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 ∈ I
⊢ dpow hI hJ n x = hI.dpow n x
Tactic:
rw [← add_zero 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 ∈ I
⊢ dpow hI hJ n (x + 0) = hI.dpow n (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 ∈ I
⊢ dpow hI hJ n (x + 0) = hI.dpow n (x + 0)
Tactic:
rw [dpow_eq hI hJ hIJ n hx J.zero_mem]
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 ∈ I
⊢ ∑ k ∈ range (n + 1), hI.dpow k x * hJ.dpow (n - k) 0 = hI.dpow n (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 ∈ I
⊢ ∑ k ∈ range (n + 1), hI.dpow k x * hJ.dpow (n - k) 0 = hI.dpow n (x + 0)
Tactic:
rw [Finset.sum_eq_single n]
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 ∈ I
⊢ hI.dpow n x * hJ.dpow (n - n) 0 = hI.dpow n (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 ∈ I
⊢ ∀ b ∈ range (n + 1), b ≠ n → hI.dpow b x * hJ.dpow (n - b) 0 = 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 ∈ I
⊢ n ∉ range (n + 1) → hI.dpow n x * hJ.dpow (n - n) 0 = 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 ∈ I
⊢ hI.dpow n x * hJ.dpow (n - n) 0 = hI.dpow n (x + 0)
Tactic:
simp only [le_refl, tsub_eq_zero_of_le, add_zero]
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 ∈ I
⊢ hI.dpow n x * hJ.dpow 0 0 = hI.dpow n 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 ∈ I
⊢ hI.dpow n x * hJ.dpow 0 0 = hI.dpow n x
Tactic:
rw [hJ.dpow_zero J.zero_mem, mul_one]
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 ∈ I
⊢ ∀ b ∈ range (n + 1), b ≠ n → hI.dpow b x * hJ.dpow (n - b) 0 = 0
Tactic:
intro b hb 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 ∈ I
b : ℕ
hb : b ∈ range (n + 1)
hb' : b ≠ n
⊢ hI.dpow b x * hJ.dpow (n - b) 0 = 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 ∈ I
b : ℕ
hb : b ∈ range (n + 1)
hb' : b ≠ n
⊢ hI.dpow b x * hJ.dpow (n - b) 0 = 0
Tactic:
rw [hJ.dpow_eval_zero, MulZeroClass.mul_zero]
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 ∈ I
b : ℕ
hb : b ∈ range (n + 1)
hb' : b ≠ n
⊢ n - 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 ∈ I
b : ℕ
hb : b ∈ range (n + 1)
hb' : b ≠ n
⊢ n - b ≠ 0
Tactic:
intro h
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 ∈ I
b : ℕ
hb : b ∈ range (n + 1)
hb' : b ≠ n
h : n - b = 0
⊢ 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 ∈ I
b : ℕ
hb : b ∈ range (n + 1)
hb' : b ≠ n
h : n - b = 0
⊢ False
Tactic:
apply 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 ∈ I
b : ℕ
hb : b ∈ range (n + 1)
hb' : b ≠ n
h : n - b = 0
⊢ b = n

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 ∈ I
b : ℕ
hb : b ∈ range (n + 1)
hb' : b ≠ n
h : n - b = 0
⊢ b = n
Tactic:
rw [Finset.mem_range, Nat.lt_succ_iff] at 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 ∈ I
b : ℕ
hb : b ≤ n
hb' : b ≠ n
h : n - b = 0
⊢ b = n

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 ∈ I
b : ℕ
hb : b ≤ n
hb' : b ≠ n
h : n - b = 0
⊢ b = n
Tactic:
rw [← Nat.sub_add_cancel hb, h, zero_add]
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 ∈ I
⊢ n ∉ range (n + 1) → hI.dpow n x * hJ.dpow (n - n) 0 = 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 ∈ I
hn : n ∉ range (n + 1)
⊢ hI.dpow n x * hJ.dpow (n - n) 0 = 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 ∈ I
hn : n ∉ range (n + 1)
⊢ hI.dpow n x * hJ.dpow (n - n) 0 = 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 ∈ I
hn : n ∉ 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 ∈ I
hn : n ∉ 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 ∈ I
hn : n ∉ range (n + 1)
⊢ n ∈ 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 ∈ I
hn : n ∉ range (n + 1)
⊢ n ∈ 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 ∈ I
hn : n ∉ range (n + 1)
⊢ n < 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 ∈ I
hn : n ∉ range (n + 1)
⊢ n < n + 1
Tactic:
exact lt_add_one n
State after:
no goals