Theorem: DividedPowers.IdealAdd.dpow_unique (DividedPowers/IdealAdd.lean)

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
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

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]
State after:
no goals

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
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

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
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

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
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

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
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

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
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)

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)]
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)

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
⊢ ∑ k ∈ range (n + 1), hsup.dpow k a * hsup.dpow (n - k) b = (dividedPowers hI hJ hIJ).dpow n (a + b)
Tactic:
simp only [IdealAdd.dividedPowers, dpow_eq hI hJ hIJ n ha hb]
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 = ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b

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
⊢ ∑ k ∈ range (n + 1), hsup.dpow k a * hsup.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
apply Finset.sum_congr rfl
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
⊢ ∀ x ∈ range (n + 1), hsup.dpow x a * hsup.dpow (n - x) b = hI.dpow x a * hJ.dpow (n - x) b

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
⊢ ∀ x ∈ range (n + 1), hsup.dpow x a * hsup.dpow (n - x) b = hI.dpow x a * hJ.dpow (n - x) b
Tactic:
intro k _
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 : ℕ
a✝ : k ∈ range (n + 1)
⊢ hsup.dpow k a * hsup.dpow (n - k) b = hI.dpow k a * hJ.dpow (n - k) b