Theorem: DividedPowers.isSubDPIdeal_iSup (DividedPowers/SubDPIdeal.lean)

State before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
⊢ hI.isSubDPIdeal (iSup J)
Tactic:
rw [Ideal.iSup_eq_span]
State after:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
⊢ hI.isSubDPIdeal (Ideal.span (⋃ i, ↑(J i)))

State before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
⊢ hI.isSubDPIdeal (Ideal.span (⋃ i, ↑(J i)))
Tactic:
rw [span_isSubDPIdeal_iff]
State after:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ ⋃ i, ↑(J i), hI.dpow n s ∈ Ideal.span (⋃ i, ↑(J i))

case hS
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
⊢ ⋃ i, ↑(J i) ⊆ ↑I

State before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ ⋃ i, ↑(J i), hI.dpow n s ∈ Ideal.span (⋃ i, ↑(J i))
Tactic:
rintro n hn a
State after:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
⊢ a ∈ ⋃ i, ↑(J i) → hI.dpow n a ∈ Ideal.span (⋃ i, ↑(J i))

State before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
⊢ a ∈ ⋃ i, ↑(J i) → hI.dpow n a ∈ Ideal.span (⋃ i, ↑(J i))
Tactic:
rw [Set.mem_iUnion]
State after:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
⊢ (∃ i, a ∈ ↑(J i)) → hI.dpow n a ∈ Ideal.span (⋃ i, ↑(J i))

State before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
⊢ (∃ i, a ∈ ↑(J i)) → hI.dpow n a ∈ Ideal.span (⋃ i, ↑(J i))
Tactic:
rintro ⟨i, ha⟩
State after:
case intro
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
i : ι
ha : a ∈ ↑(J i)
⊢ hI.dpow n a ∈ Ideal.span (⋃ i, ↑(J i))

State before:
case intro
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
i : ι
ha : a ∈ ↑(J i)
⊢ hI.dpow n a ∈ Ideal.span (⋃ i, ↑(J i))
Tactic:
apply Ideal.span_mono (Set.subset_iUnion _ i)
State after:
case intro.a
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
i : ι
ha : a ∈ ↑(J i)
⊢ hI.dpow n a ∈ Ideal.span ↑(J i)

State before:
case intro.a
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
i : ι
ha : a ∈ ↑(J i)
⊢ hI.dpow n a ∈ Ideal.span ↑(J i)
Tactic:
rw [Ideal.span_eq]
State after:
case intro.a
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
i : ι
ha : a ∈ ↑(J i)
⊢ hI.dpow n a ∈ J i

State before:
case intro.a
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
i : ι
ha : a ∈ ↑(J i)
⊢ hI.dpow n a ∈ J i
Tactic:
exact (hJ i).2 n hn a ha
State after:
no goals

State before:
case hS
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
⊢ ⋃ i, ↑(J i) ⊆ ↑I
Tactic:
rw [Set.iUnion_subset_iff]
State after:
case hS
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
⊢ ∀ (i : ι), ↑(J i) ⊆ ↑I

State before:
case hS
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
⊢ ∀ (i : ι), ↑(J i) ⊆ ↑I
Tactic:
intro i
State after:
case hS
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
i : ι
⊢ ↑(J i) ⊆ ↑I

State before:
case hS
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
J : ι → Ideal A
hJ : ∀ (i : ι), hI.isSubDPIdeal (J i)
i : ι
⊢ ↑(J i) ⊆ ↑I
Tactic:
exact (hJ i).1
State after:
no goals