internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof state before:
case mpr.refine'_4
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ Ideal.span S
hSI : Ideal.span S ≤ I
z : A
hz : z ∈ Ideal.span S
a x : A
hxI : x ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
⊢ a ^ n * hI.dpow n x ∈ Ideal.span S
Tactic:
exact Ideal.mul_mem_left (Ideal.span S) (a ^ n) (hx n hn)
Proof state after:
no goals
Theorem: DividedPowers.generated_dpow_isSubIdeal
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
Tactic:
rw [Ideal.span_le]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ⊆ ↑I
Theorem: DividedPowers.generated_dpow_isSubIdeal
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ⊆ ↑I
Tactic:
rintro y ⟨n, hn, x, hx, hxy⟩
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
y : A
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
hxy : y = hI.dpow n x
⊢ y ∈ ↑I
Theorem: DividedPowers.generated_dpow_isSubIdeal
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
y : A
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
hxy : y = hI.dpow n x
⊢ y ∈ ↑I
Tactic:
rw [hxy]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
y : A
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
hxy : y = hI.dpow n x
⊢ hI.dpow n x ∈ ↑I
Theorem: DividedPowers.generated_dpow_isSubIdeal
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
y : A
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
hxy : y = hI.dpow n x
⊢ hI.dpow n x ∈ ↑I
Tactic:
exact hI.dpow_mem hn (hS hx)
Proof state after:
no goals
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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]
Proof 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
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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⟩
Proof state after:
no goals
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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
Proof 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)
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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
Proof 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)
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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
Proof 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)
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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 _ _)
Proof 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
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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]
Proof 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
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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 _ _)
Proof 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
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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]
Proof 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
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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]
Proof 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
Theorem: DividedPowers.isSubDPIdeal_sup
Proof 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⟩
Proof state after:
no goals
Theorem: DividedPowers.isSubDPIdeal_iSup
Proof 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]
Proof 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)))
Theorem: DividedPowers.isSubDPIdeal_iSup
Proof 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]
Proof 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
Theorem: DividedPowers.isSubDPIdeal_iSup
Proof 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
Proof 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))
Theorem: DividedPowers.isSubDPIdeal_iSup
Proof 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]
Proof 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))
Theorem: DividedPowers.isSubDPIdeal_iSup
Proof 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⟩
Proof 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))
Theorem: DividedPowers.isSubDPIdeal_iSup
Proof 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)
Proof 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)
Theorem: DividedPowers.isSubDPIdeal_iSup
Proof 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]
Proof 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
Theorem: DividedPowers.isSubDPIdeal_iSup
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.isSubDPIdeal_iSup
Proof 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]
Proof 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
Theorem: DividedPowers.isSubDPIdeal_iSup
Proof 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
Proof 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
Theorem: DividedPowers.isSubDPIdeal_iSup
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.isSubDPIdeal_map
Proof state before:
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ hJ.isSubDPIdeal (Ideal.map f K)
Tactic:
simp only [Ideal.map]
Proof state after:
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ hJ.isSubDPIdeal (Ideal.span (⇑f '' ↑K))
Theorem: DividedPowers.isSubDPIdeal_map
Proof state before:
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ hJ.isSubDPIdeal (Ideal.span (⇑f '' ↑K))
Tactic:
rw [span_isSubDPIdeal_iff]
Proof state after:
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ ⇑f '' ↑K, hJ.dpow n s ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Theorem: DividedPowers.isSubDPIdeal_map
Proof state before:
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ ⇑f '' ↑K, hJ.dpow n s ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Tactic:
rintro n hn y ⟨x, hx, rfl⟩
Proof state after:
case intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ hJ.dpow n (f x) ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Theorem: DividedPowers.isSubDPIdeal_map
Proof state before:
case intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ hJ.dpow n (f x) ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Tactic:
rw [hf.2 n x (hK.1 hx)]
Proof state after:
case intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ f (hI.dpow n x) ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Theorem: DividedPowers.isSubDPIdeal_map
Proof state before:
case intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ f (hI.dpow n x) ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Tactic:
apply Ideal.mem_map_of_mem
Proof state after:
case intro.intro.h
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ hI.dpow n x ∈ K

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Theorem: DividedPowers.isSubDPIdeal_map
Proof state before:
case intro.intro.h
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ hI.dpow n x ∈ K

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Tactic:
exact hK.2 n hn x hx
Proof state after:
case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Theorem: DividedPowers.isSubDPIdeal_map
Proof state before:
case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Tactic:
rintro y ⟨x, hx, rfl⟩
Proof state after:
case hS.intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
x : A
hx : x ∈ ↑K
⊢ f x ∈ ↑J
Theorem: DividedPowers.isSubDPIdeal_map
Proof state before:
case hS.intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
x : A
hx : x ∈ ↑K
⊢ f x ∈ ↑J
Tactic:
exact hf.1 (Ideal.mem_map_of_mem f (hK.1 hx))
Proof state after:
no goals
Theorem: DividedPowers.SubDPIdeal.le_generatedDpow
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
x : A
hx : x ∈ S
⊢ x = hI.dpow 1 x
Tactic:
rw [hI.dpow_one (hS hx)]
Proof state after:
no goals
Theorem: DividedPowers.SubDPIdeal.generated_dpow_le
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
J : hI.SubDPIdeal
hSJ : S ⊆ ↑J.carrier
⊢ Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ J.carrier
Tactic:
rw [Ideal.span_le]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
J : hI.SubDPIdeal
hSJ : S ⊆ ↑J.carrier
⊢ {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ⊆ ↑J.carrier
Theorem: DividedPowers.SubDPIdeal.generated_dpow_le
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
J : hI.SubDPIdeal
hSJ : S ⊆ ↑J.carrier
⊢ {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ⊆ ↑J.carrier
Tactic:
rintro y ⟨n, hn, x, hx, hxy⟩
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
J : hI.SubDPIdeal
hSJ : S ⊆ ↑J.carrier
y : A
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
hxy : y = hI.dpow n x
⊢ y ∈ ↑J.carrier
Theorem: DividedPowers.SubDPIdeal.generated_dpow_le
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
J : hI.SubDPIdeal
hSJ : S ⊆ ↑J.carrier
y : A
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
hxy : y = hI.dpow n x
⊢ y ∈ ↑J.carrier
Tactic:
rw [hxy]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
J : hI.SubDPIdeal
hSJ : S ⊆ ↑J.carrier
y : A
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
hxy : y = hI.dpow n x
⊢ hI.dpow n x ∈ ↑J.carrier
Theorem: DividedPowers.SubDPIdeal.generated_dpow_le
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
J : hI.SubDPIdeal
hSJ : S ⊆ ↑J.carrier
y : A
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
hxy : y = hI.dpow n x
⊢ hI.dpow n x ∈ ↑J.carrier
Tactic:
exact J.dpow_mem n hn x (hSJ hx)
Proof state after:
no goals
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ (generated hI S).carrier = Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Tactic:
simp only [generated, sInf_carrier_def]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier =
    Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}