Theorem: DividedPowers.IdealAdd.dpow_one (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
hx : x ∈ I + J
⊢ dpow hI hJ 1 x = x
Tactic:
rw [Ideal.add_eq_sup, Submodule.mem_sup] at hx
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

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

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

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

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

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

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

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

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

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

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

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