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

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

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

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

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