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

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
⊢ hI.isSubDPIdeal (J ⊔ K)
Tactic:
rw [← J.span_eq, ← K.span_eq, ← Ideal.span_union, span_isSubDPIdeal_iff]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ ↑J ∪ ↑K, hI.dpow n s ∈ Ideal.span (↑J ∪ ↑K)

case hS
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
⊢ ↑J ∪ ↑K ⊆ ↑I

State before:
case hS
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
⊢ ↑J ∪ ↑K ⊆ ↑I
Tactic:
. rw [Set.union_subset_iff]; exact ⟨hJ.1, hK.1⟩
State after:
no goals

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ ↑J ∪ ↑K, hI.dpow n s ∈ Ideal.span (↑J ∪ ↑K)
Tactic:
intro n hn a ha
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J ∪ ↑K
⊢ hI.dpow n a ∈ Ideal.span (↑J ∪ ↑K)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J ∪ ↑K
⊢ hI.dpow n a ∈ Ideal.span (↑J ∪ ↑K)
Tactic:
cases' ha with ha ha
State after:
case inl
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J
⊢ hI.dpow n a ∈ Ideal.span (↑J ∪ ↑K)

case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑K
⊢ hI.dpow n a ∈ Ideal.span (↑J ∪ ↑K)

State before:
case inl
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J
⊢ hI.dpow n a ∈ Ideal.span (↑J ∪ ↑K)

case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑K
⊢ hI.dpow n a ∈ Ideal.span (↑J ∪ ↑K)
Tactic:
. apply Ideal.span_mono (Set.subset_union_left _ _)
  rw [J.span_eq]; exact hJ.2 n hn a ha
State after:
case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑K
⊢ hI.dpow n a ∈ Ideal.span (↑J ∪ ↑K)

State before:
case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑K
⊢ hI.dpow n a ∈ Ideal.span (↑J ∪ ↑K)
Tactic:
. apply Ideal.span_mono (Set.subset_union_right _ _)
  rw [K.span_eq]; exact hK.2 n hn a ha
State after:
no goals

State before:
case inl
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J
⊢ hI.dpow n a ∈ Ideal.span (↑J ∪ ↑K)
Tactic:
apply Ideal.span_mono (Set.subset_union_left _ _)
State after:
case inl.a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J
⊢ hI.dpow n a ∈ Ideal.span ↑J

State before:
case inl.a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J
⊢ hI.dpow n a ∈ Ideal.span ↑J
Tactic:
rw [J.span_eq]
State after:
case inl.a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J
⊢ hI.dpow n a ∈ J

State before:
case inl.a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J
⊢ hI.dpow n a ∈ J
Tactic:
exact hJ.2 n hn a ha
State after:
no goals

State before:
case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑K
⊢ hI.dpow n a ∈ Ideal.span (↑J ∪ ↑K)
Tactic:
apply Ideal.span_mono (Set.subset_union_right _ _)
State after:
case inr.a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑K
⊢ hI.dpow n a ∈ Ideal.span ↑K

State before:
case inr.a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑K
⊢ hI.dpow n a ∈ Ideal.span ↑K
Tactic:
rw [K.span_eq]
State after:
case inr.a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑K
⊢ hI.dpow n a ∈ K

State before:
case inr.a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑K
⊢ hI.dpow n a ∈ K
Tactic:
exact hK.2 n hn a ha
State after:
no goals

State before:
case hS
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
⊢ ↑J ∪ ↑K ⊆ ↑I
Tactic:
rw [Set.union_subset_iff]
State after:
case hS
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
⊢ ↑J ⊆ ↑I ∧ ↑K ⊆ ↑I

State before:
case hS
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.isSubDPIdeal J
hK : hI.isSubDPIdeal K
⊢ ↑J ⊆ ↑I ∧ ↑K ⊆ ↑I
Tactic:
exact ⟨hJ.1, hK.1⟩
State after:
no goals