Theorem: DividedPowers.IdealAdd.dpow_zero (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
⊢ ∀ {x : A}, x ∈ I + J → dpow hI hJ 0 x = 1
Tactic:
intro 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
x : A
⊢ x ∈ I + J → dpow hI hJ 0 x = 1

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

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

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

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

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