internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.IdealAdd.dpow_comp
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
p : ℕ
hp : p ∈ range (m * n + 1)
⊢ ↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
            ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
              Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
        hI.dpow p a *
      hJ.dpow (m * n - p) b =
    ↑(mchoose m n) * (hI.dpow p a * hJ.dpow (m * n - p) b)
Tactic:
simp only [mul_assoc]
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
p : ℕ
hp : p ∈ range (m * n + 1)
⊢ ↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
          (∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
            ((Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
              Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i))) *
      (hI.dpow p a * hJ.dpow (m * n - p) b) =
    ↑(mchoose m n) * (hI.dpow p a * hJ.dpow (m * n - p) b)
Theorem: DividedPowers.IdealAdd.dpow_comp
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
p : ℕ
hp : p ∈ range (m * n + 1)
⊢ ↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
        (∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
          ((Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
            Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i))) =
    ↑(mchoose m n)
Tactic:
rw [dpow_comp_coeffs hn (Nat.lt_succ_iff.mp (Finset.mem_range.mp hp))]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_null
Proof 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]
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_null
Proof 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']
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_null
Proof 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
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_null
Proof 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⟩
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_null
Proof 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
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_null
Proof 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]
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_null
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_one
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
hx : x ∈ I + J
⊢ dpow hI hJ 1 x = x
Tactic:
rw [Ideal.add_eq_sup, Submodule.mem_sup] at 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
x : A
hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x
⊢ dpow hI hJ 1 x = x
Theorem: DividedPowers.IdealAdd.dpow_one
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
hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x
⊢ dpow hI hJ 1 x = x
Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := hx
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 1 (a + b) = a + b
Theorem: DividedPowers.IdealAdd.dpow_one
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 1 (a + b) = a + b
Tactic:
rw [dpow_eq hI hJ hIJ _ 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 (1 + 1), hI.dpow k a * hJ.dpow (1 - k) b = a + b
Theorem: DividedPowers.IdealAdd.dpow_one
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 (1 + 1), hI.dpow k a * hJ.dpow (1 - k) b = a + b
Tactic:
suffices h : Finset.range (1 + 1) = {0, 1} by
  rw [h]
  simp only [Finset.sum_insert, Finset.mem_singleton, Nat.zero_ne_one, not_false_iff, tsub_zero,
    Finset.sum_singleton, tsub_self]
  rw [hI.dpow_zero ha, hI.dpow_one ha, hJ.dpow_zero hb, hJ.dpow_one hb]
  ring
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
⊢ range (1 + 1) = {0, 1}
Theorem: DividedPowers.IdealAdd.dpow_one
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : range (1 + 1) = {0, 1}
⊢ ∑ k ∈ range (1 + 1), hI.dpow k a * hJ.dpow (1 - k) b = a + b
Tactic:
rw [h]
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : range (1 + 1) = {0, 1}
⊢ ∑ k ∈ {0, 1}, hI.dpow k a * hJ.dpow (1 - k) b = a + b
Theorem: DividedPowers.IdealAdd.dpow_one
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : range (1 + 1) = {0, 1}
⊢ ∑ k ∈ {0, 1}, hI.dpow k a * hJ.dpow (1 - k) b = a + b
Tactic:
simp only [Finset.sum_insert, Finset.mem_singleton, Nat.zero_ne_one, not_false_iff, tsub_zero,
  Finset.sum_singleton, tsub_self]
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : range (1 + 1) = {0, 1}
⊢ hI.dpow 0 a * hJ.dpow 1 b + hI.dpow 1 a * hJ.dpow 0 b = a + b
Theorem: DividedPowers.IdealAdd.dpow_one
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : range (1 + 1) = {0, 1}
⊢ hI.dpow 0 a * hJ.dpow 1 b + hI.dpow 1 a * hJ.dpow 0 b = a + b
Tactic:
rw [hI.dpow_zero ha, hI.dpow_one ha, hJ.dpow_zero hb, hJ.dpow_one hb]
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : range (1 + 1) = {0, 1}
⊢ 1 * b + a * 1 = a + b
Theorem: DividedPowers.IdealAdd.dpow_one
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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
h : range (1 + 1) = {0, 1}
⊢ 1 * b + a * 1 = a + b
Tactic:
ring
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_one
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
⊢ range (1 + 1) = {0, 1}
Tactic:
rw [Finset.range_succ, Finset.range_one]
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
⊢ {1, 0} = {0, 1}
Theorem: DividedPowers.IdealAdd.dpow_one
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
⊢ {1, 0} = {0, 1}
Tactic:
ext k
Proof state after:
case intro.intro.intro.intro.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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
⊢ k ∈ {1, 0} ↔ k ∈ {0, 1}
Theorem: DividedPowers.IdealAdd.dpow_one
Proof state before:
case intro.intro.intro.intro.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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
⊢ k ∈ {1, 0} ↔ k ∈ {0, 1}
Tactic:
simp
Proof state after:
case intro.intro.intro.intro.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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
⊢ k = 1 ∨ k = 0 ↔ k = 0 ∨ k = 1
Theorem: DividedPowers.IdealAdd.dpow_one
Proof state before:
case intro.intro.intro.intro.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
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
⊢ k = 1 ∨ k = 0 ↔ k = 0 ∨ k = 1
Tactic:
exact or_comm
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_unique
Proof state before:
A : Type ?u.129773
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
n : ℕ
a : A
ha : a ∈ I ⊓ J
⊢ hI.dpow n a = hJ.dpow n a
Tactic:
rw [Submodule.mem_inf] at ha
Proof state after:
A : Type ?u.129773
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
n : ℕ
a : A
ha : a ∈ I ∧ a ∈ J
⊢ hI.dpow n a = hJ.dpow n a
Theorem: DividedPowers.IdealAdd.dpow_unique
Proof state before:
A : Type ?u.129773
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
n : ℕ
a : A
ha : a ∈ I ∧ a ∈ J
⊢ hI.dpow n a = hJ.dpow n a
Tactic:
rw [hI' _ _ ha.1, hJ' _ _ ha.2]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_unique
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
⊢ let hIJ := ⋯;
  hsup = dividedPowers hI hJ hIJ
Tactic:
intro hIJ
Proof state after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
⊢ hsup = dividedPowers hI hJ hIJ
Theorem: DividedPowers.IdealAdd.dpow_unique
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
⊢ hsup = dividedPowers hI hJ hIJ
Tactic:
apply eq_of_eq_on_ideal
Proof state after:
case h_eq
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
⊢ ∀ (n : ℕ) {x : A}, x ∈ I + J → hsup.dpow n x = (dividedPowers hI hJ hIJ).dpow n x
Theorem: DividedPowers.IdealAdd.dpow_unique
Proof state before:
case h_eq
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
⊢ ∀ (n : ℕ) {x : A}, x ∈ I + J → hsup.dpow n x = (dividedPowers hI hJ hIJ).dpow n x
Tactic:
intro n x hx
Proof state after:
case h_eq
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
x : A
hx : x ∈ I + J
⊢ hsup.dpow n x = (dividedPowers hI hJ hIJ).dpow n x
Theorem: DividedPowers.IdealAdd.dpow_unique
Proof state before:
case h_eq
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
x : A
hx : x ∈ I + J
⊢ hsup.dpow n x = (dividedPowers hI hJ hIJ).dpow n x
Tactic:
rw [Ideal.add_eq_sup, Submodule.mem_sup] at hx
Proof state after:
case h_eq
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
x : A
hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x
⊢ hsup.dpow n x = (dividedPowers hI hJ hIJ).dpow n x
Theorem: DividedPowers.IdealAdd.dpow_unique
Proof state before:
case h_eq
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
x : A
hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x
⊢ hsup.dpow n x = (dividedPowers hI hJ hIJ).dpow n x
Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := hx
Proof state after:
case h_eq.intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ hsup.dpow n (a + b) = (dividedPowers hI hJ hIJ).dpow n (a + b)
Theorem: DividedPowers.IdealAdd.dpow_unique
Proof state before:
case h_eq.intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ hsup.dpow n (a + b) = (dividedPowers hI hJ hIJ).dpow n (a + b)
Tactic:
rw [hsup.dpow_add' n (Submodule.mem_sup_left ha) (Submodule.mem_sup_right hb)]
Proof state after:
case h_eq.intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hsup.dpow k a * hsup.dpow (n - k) b = (dividedPowers hI hJ hIJ).dpow n (a + b)