internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
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 : 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]
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 : 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
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 : 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]
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 : A
hx : x ∈ I
⊢ hI.dpow n x * hJ.dpow 0 0 = hI.dpow n x
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
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 : 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]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
Proof 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'
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
Proof 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]
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
Proof 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
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
Proof 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'
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
Proof 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
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
Proof 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]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
Proof 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
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
Proof 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
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
Proof 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
Proof 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)
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
Proof 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]
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
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 : A
hx : x ∈ J
⊢ dpow hI hJ n x = hJ.dpow n x
Tactic:
rw [← zero_add 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 : ℕ
x : A
hx : x ∈ J
⊢ dpow hI hJ n (0 + x) = hJ.dpow n (0 + x)
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
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 : 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]
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 : A
hx : x ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k 0 * hJ.dpow (n - k) x = hJ.dpow n (0 + x)
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
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 : 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]
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 : 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
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 : 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]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
Proof 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'
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
Proof 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]
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
Proof 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'
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
Proof 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
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
Proof 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
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
Proof 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
Proof 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)
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
Proof 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]
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_right
Proof 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)
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_zero
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
⊢ ∀ {x : A}, x ∈ I + J → dpow hI hJ 0 x = 1
Tactic:
intro 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
x : A
⊢ x ∈ I + J → dpow hI hJ 0 x = 1
Theorem: DividedPowers.IdealAdd.dpow_zero
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
x : A
⊢ x ∈ I + J → dpow hI hJ 0 x = 1
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
x : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → dpow hI hJ 0 x = 1
Theorem: DividedPowers.IdealAdd.dpow_zero
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
x : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → dpow hI hJ 0 x = 1
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ 0 (a + b) = 1
Theorem: DividedPowers.IdealAdd.dpow_zero
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ 0 (a + b) = 1
Tactic:
rw [dpow_eq hI hJ hIJ (0 : ℕ) 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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (0 + 1), hI.dpow k a * hJ.dpow (0 - k) b = 1
Theorem: DividedPowers.IdealAdd.dpow_zero
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (0 + 1), hI.dpow k a * hJ.dpow (0 - k) b = 1
Tactic:
simp only [zero_add, range_one, ge_iff_le, zero_le, tsub_eq_zero_of_le, sum_singleton]
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ hI.dpow 0 a * hJ.dpow 0 b = 1
Theorem: DividedPowers.IdealAdd.dpow_zero
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ hI.dpow 0 a * hJ.dpow 0 b = 1
Tactic:
rw [hI.dpow_zero ha, hJ.dpow_zero hb, mul_one]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_mul
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
m n : ℕ
x : A
⊢ x ∈ I + J → dpow hI hJ m x * dpow hI hJ n x = ↑((m + n).choose m) * dpow hI hJ (m + 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
m n : ℕ
x : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → dpow hI hJ m x * dpow hI hJ n x = ↑((m + n).choose m) * dpow hI hJ (m + n) x
Theorem: DividedPowers.IdealAdd.dpow_mul
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
m n : ℕ
x : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → dpow hI hJ m x * dpow hI hJ n x = ↑((m + n).choose m) * dpow hI hJ (m + 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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ m (a + b) * dpow hI hJ n (a + b) = ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Theorem: DividedPowers.IdealAdd.dpow_mul
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ m (a + b) * dpow hI hJ n (a + b) = ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [dpow_eq hI hJ hIJ m 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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ (∑ k ∈ range (m + 1), hI.dpow k a * hJ.dpow (m - k) b) * dpow hI hJ n (a + b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Theorem: DividedPowers.IdealAdd.dpow_mul
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ (∑ k ∈ range (m + 1), hI.dpow k a * hJ.dpow (m - k) b) * dpow hI hJ n (a + b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [← Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j => hI.dpow i a * hJ.dpow j b]
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * dpow hI hJ n (a + b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Theorem: DividedPowers.IdealAdd.dpow_mul
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * dpow hI hJ n (a + b) =
    ↑((m + n).choose m) * dpow hI hJ (m + 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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Theorem: DividedPowers.IdealAdd.dpow_mul
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [← Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun k l => hI.dpow k a * hJ.dpow l b]
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * ∑ ij ∈ antidiagonal n, hI.dpow ij.1 a * hJ.dpow ij.2 b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Theorem: DividedPowers.IdealAdd.dpow_mul
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * ∑ ij ∈ antidiagonal n, hI.dpow ij.1 a * hJ.dpow ij.2 b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [Finset.sum_mul]
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ i ∈ antidiagonal m, hI.dpow i.1 a * hJ.dpow i.2 b * ∑ ij ∈ antidiagonal n, hI.dpow ij.1 a * hJ.dpow ij.2 b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)