internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
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
L1 :
  ∀ (k : Sym ℕ m),
    ∀ i ∈ range (n + 1),
      dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
        ↑(DividedPowers.IdealAdd.cnik n i ↑k) * hI.dpow (Multiset.count i ↑k * i) a *
          hJ.dpow (Multiset.count i ↑k * (n - i)) b
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
k : Sym ℕ m
hk : k ∈ (range (n + 1)).sym m
⊢ φ k ∈ range (m * n + 1)
Tactic:
simp only [Sym.mem_coe, mem_range, Nat.lt_succ_iff]
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
L1 :
  ∀ (k : Sym ℕ m),
    ∀ i ∈ range (n + 1),
      dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
        ↑(DividedPowers.IdealAdd.cnik n i ↑k) * hI.dpow (Multiset.count i ↑k * i) a *
          hJ.dpow (Multiset.count i ↑k * (n - i)) b
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
k : Sym ℕ m
hk : k ∈ (range (n + 1)).sym m
⊢ φ k ≤ m * n
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
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
L1 :
  ∀ (k : Sym ℕ m),
    ∀ i ∈ range (n + 1),
      dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
        ↑(DividedPowers.IdealAdd.cnik n i ↑k) * hI.dpow (Multiset.count i ↑k * i) a *
          hJ.dpow (Multiset.count i ↑k * (n - i)) b
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
k : Sym ℕ m
hk : k ∈ (range (n + 1)).sym m
⊢ φ k ≤ m * n
Tactic:
exact range_sym_weighted_sum_le hk
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_zero
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
⊢ ∀ {x : A}, x ∈ ?m.65386 → dpow hI hJ 0 x = 1
Tactic:
intro x hx
Proof state after:
case dpow_zero
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
x : A
hx : x ∈ ?m.65386
⊢ dpow hI hJ 0 x = 1
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_zero
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
x : A
hx : x ∈ ?m.65386
⊢ dpow hI hJ 0 x = 1
Tactic:
rw [dpow_zero hI hJ hIJ]
Proof state after:
case dpow_zero
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
x : A
hx : x ∈ ?m.65386
⊢ x ∈ I + J
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_zero
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
x : A
hx : x ∈ ?m.65386
⊢ x ∈ I + J
Tactic:
exact hx
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_add
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
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y
Tactic:
simp only [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
Proof state after:
case dpow_add
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
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ x_3 ∈ range n.succ, dpow hI hJ x_3 x * dpow hI hJ (n - x_3) y
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_add
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
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ x_3 ∈ range n.succ, dpow hI hJ x_3 x * dpow hI hJ (n - x_3) y
Tactic:
intro n x y hx hy
Proof state after:
case dpow_add
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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ dpow hI hJ n (x + y) = ∑ x_1 ∈ range n.succ, dpow hI hJ x_1 x * dpow hI hJ (n - x_1) y
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_add
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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ dpow hI hJ n (x + y) = ∑ x_1 ∈ range n.succ, dpow hI hJ x_1 x * dpow hI hJ (n - x_1) y
Tactic:
rw [dpow_add' hI hJ hIJ]
Proof state after:
case dpow_add.x
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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ x ∈ I + J

case dpow_add.x
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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ y ∈ I + J
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_add.x
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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ x ∈ I + J

case dpow_add.x
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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ y ∈ I + J
Tactic:
exact hx
Proof state after:
case dpow_add.x
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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ y ∈ I + J
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_add.x
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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ y ∈ I + J
Tactic:
exact hy
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_eval_zero
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
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0
Tactic:
intro n hn
Proof state after:
case dpow_eval_zero
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
n : ℕ
hn : n ≠ 0
⊢ dpow hI hJ n 0 = 0
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_eval_zero
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
n : ℕ
hn : n ≠ 0
⊢ dpow hI hJ n 0 = 0
Tactic:
rw [dpow_eq_of_mem_left hI hJ hIJ n I.zero_mem]
Proof state after:
case dpow_eval_zero
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
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_eval_zero
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
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0
Tactic:
exact dpow_eval_zero hI hn
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case hx
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
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Tactic:
intro i _
Proof state after:
case hx
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
i : ℕ
a✝ : i ∈ range (n + 1)
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case hx
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
i : ℕ
a✝ : i ∈ range (n + 1)
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Tactic:
by_cases hi0 : i = 0
Proof state after:
case pos
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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J

case neg
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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case pos
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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Tactic:
rw [hi0]
Proof state after:
case pos
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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ I + J
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case pos
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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ I + J
Tactic:
apply Submodule.mem_sup_right
Proof state after:
case pos.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
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ J
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case pos.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
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ J
Tactic:
apply Ideal.mul_mem_left
Proof state after:
case pos.a.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
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hJ.dpow (n - 0) b ∈ J
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case pos.a.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
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hJ.dpow (n - 0) b ∈ J
Tactic:
exact hJ.dpow_mem hn hb
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case neg
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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Tactic:
apply Submodule.mem_sup_left
Proof state after:
case neg.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
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case neg.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
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I
Tactic:
apply Ideal.mul_mem_right
Proof state after:
case neg.a.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
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a ∈ I
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case neg.a.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
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a ∈ I
Tactic:
exact hI.dpow_mem hi0 ha
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ Ring.inverse (C a) = C (Ring.inverse a)
Tactic:
simp only [Ring.inverse]
Proof state after:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)
Tactic:
by_cases ha : IsUnit a
Proof state after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)

case neg
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)
Tactic:
simp only [dif_pos ha]
Proof state after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C ↑ha.unit⁻¹
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C ↑ha.unit⁻¹
Tactic:
have hCa : IsUnit (C a) := by
  rw [← IsUnit.unit_spec ha]
  exact RingHom.isUnit_map C ha
Proof state after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C ↑ha.unit⁻¹
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C ↑ha.unit⁻¹
Tactic:
rw [dif_pos hCa]
Proof state after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ = C ↑ha.unit⁻¹
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ = C ↑ha.unit⁻¹
Tactic:
apply IsUnit.mul_right_cancel hCa
Proof state after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ * C a = C ↑ha.unit⁻¹ * C a
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ * C a = C ↑ha.unit⁻¹ * C a
Tactic:
rw [← map_mul]
Proof state after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ * C a = C (↑ha.unit⁻¹ * a)
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ * C a = C (↑ha.unit⁻¹ * a)
Tactic:
simp only [IsUnit.val_inv_mul, map_one]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ IsUnit (C a)
Tactic:
rw [← IsUnit.unit_spec ha]
Proof state after:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ IsUnit (C ↑ha.unit)
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ IsUnit (C ↑ha.unit)
Tactic:
exact RingHom.isUnit_map C ha
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case neg
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)
Tactic:
simp only [Ring.inverse, dif_neg ha, map_zero]
Proof state after:
case neg
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = 0
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case neg
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = 0
Tactic:
rw [dif_neg]
Proof state after:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ ¬IsUnit (C a)
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ ¬IsUnit (C a)
Tactic:
intro hCa
Proof state after:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : IsUnit (C a)
⊢ False
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : IsUnit (C a)
⊢ False
Tactic:
apply ha
Proof state after:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : IsUnit (C a)
⊢ IsUnit a
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : IsUnit (C a)
⊢ IsUnit a
Tactic:
rw [isUnit_iff_exists_inv] at hCa ⊢
Proof state after:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : ∃ b, C a * b = 1
⊢ ∃ b, a * b = 1
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : ∃ b, C a * b = 1
⊢ ∃ b, a * b = 1
Tactic:
obtain ⟨b, hb⟩ := hCa
Proof state after:
case neg.hnc.intro
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ ∃ b, a * b = 1
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case neg.hnc.intro
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ ∃ b, a * b = 1
Tactic:
use b.coeff 0
Proof state after:
case h
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ a * b.coeff 0 = 1