Theorem: DividedPowers.IdealAdd.dpow_smul (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 : ℕ) {c x : A}, x ∈ I + J → dpow hI hJ n (c * x) = c ^ n * dpow hI hJ n x
Tactic:
intro n c 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 : ℕ
c x : A
⊢ x ∈ I + J → dpow hI hJ n (c * x) = c ^ n * dpow hI hJ 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 : ℕ
c x : A
⊢ x ∈ I + J → dpow hI hJ n (c * x) = c ^ n * dpow hI hJ n x
Tactic:
rw [Ideal.add_eq_sup, Submodule.mem_sup]
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 : ℕ
c x : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → dpow hI hJ n (c * x) = c ^ n * dpow hI hJ 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 : ℕ
c x : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → dpow hI hJ n (c * x) = c ^ n * dpow hI hJ n x
Tactic:
rintro ⟨a, ha, b, hb, rfl⟩
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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * (a + b)) = c ^ n * dpow hI hJ n (a + b)

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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * (a + b)) = c ^ n * dpow hI hJ n (a + b)
Tactic:
rw [dpow_eq hI hJ hIJ n ha hb]
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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * (a + b)) = c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b

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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * (a + b)) = c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
rw [mul_add]
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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * a + c * b) = c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b

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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (c * a + c * b) = c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
rw [dpow_eq hI hJ hIJ n (Ideal.mul_mem_left I c ha) (Ideal.mul_mem_left J c hb)]
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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) =
    c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b

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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) =
    c ^ n * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
rw [Finset.mul_sum]
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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) =
    ∑ i ∈ range (n + 1), c ^ n * (hI.dpow i a * hJ.dpow (n - i) b)

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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) =
    ∑ i ∈ range (n + 1), c ^ n * (hI.dpow i a * hJ.dpow (n - i) b)
Tactic:
apply Finset.sum_congr rfl
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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ x ∈ range (n + 1), hI.dpow x (c * a) * hJ.dpow (n - x) (c * b) = c ^ n * (hI.dpow x a * hJ.dpow (n - x) b)

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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ x ∈ range (n + 1), hI.dpow x (c * a) * hJ.dpow (n - x) (c * b) = c ^ n * (hI.dpow x a * hJ.dpow (n - x) b)
Tactic:
intro k hk
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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ∈ range (n + 1)
⊢ hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)

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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ∈ range (n + 1)
⊢ hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)
Tactic:
simp only [Finset.mem_range, Nat.lt_succ_iff] at hk
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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)

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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ hI.dpow k (c * a) * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)
Tactic:
rw [hI.dpow_smul]
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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I

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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * hJ.dpow (n - k) (c * b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
rw [hJ.dpow_smul]
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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * (c ^ (n - k) * hJ.dpow (n - k) b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I

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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * (c ^ (n - k) * hJ.dpow (n - k) b) = c ^ n * (hI.dpow k a * hJ.dpow (n - k) b)

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
simp only [← mul_assoc]
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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * c ^ (n - k) * hJ.dpow (n - k) b = c ^ n * hI.dpow k a * hJ.dpow (n - k) b

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I

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 : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ k * hI.dpow k a * c ^ (n - k) = c ^ n * hI.dpow k a

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
rw [mul_comm, ← mul_assoc]
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 : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ (n - k) * c ^ k * hI.dpow k a = c ^ n * hI.dpow k a

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I

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 : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ c ^ (n - k) * c ^ k = c ^ n

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
rw [← pow_add, Nat.sub_add_cancel hk]
State after:
case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I

State before:
case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ b ∈ J

case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
exact hb
State after:
case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I

State before:
case intro.intro.intro.intro.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
n : ℕ
c a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
hk : k ≤ n
⊢ a ∈ I
Tactic:
exact ha
State after:
no goals