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

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ hI.isSubDPIdeal (Ideal.span S) ↔ ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ Ideal.span S
Tactic:
constructor
State after:
case mp
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ hI.isSubDPIdeal (Ideal.span S) → ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ Ideal.span S

case mpr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ (∀ (n : ℕ), n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ Ideal.span S) → hI.isSubDPIdeal (Ideal.span S)

State before:
case mp
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ hI.isSubDPIdeal (Ideal.span S) → ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ Ideal.span S
Tactic:
intro hhI h hn s hs
State after:
case mp
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : hI.isSubDPIdeal (Ideal.span S)
h : ℕ
hn : h ≠ 0
s : A
hs : s ∈ S
⊢ hI.dpow h s ∈ Ideal.span S

State before:
case mp
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : hI.isSubDPIdeal (Ideal.span S)
h : ℕ
hn : h ≠ 0
s : A
hs : s ∈ S
⊢ hI.dpow h s ∈ Ideal.span S
Tactic:
apply hhI.dpow_mem h hn s (Ideal.subset_span hs)
State after:
no goals

State before:
case mpr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ (∀ (n : ℕ), n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ Ideal.span S) → hI.isSubDPIdeal (Ideal.span S)
Tactic:
intro hhI
State after:
case mpr
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
⊢ hI.isSubDPIdeal (Ideal.span S)

State before:
case mpr
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
⊢ hI.isSubDPIdeal (Ideal.span S)
Tactic:
have hSI := Ideal.span_le.mpr hS
State after:
case mpr
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
⊢ hI.isSubDPIdeal (Ideal.span S)

State before:
case mpr
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
⊢ hI.isSubDPIdeal (Ideal.span S)
Tactic:
apply isSubDPIdeal.mk hSI
State after:
case mpr
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
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ Ideal.span S, hI.dpow n j ∈ Ideal.span S

State before:
case mpr
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
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ Ideal.span S, hI.dpow n j ∈ Ideal.span S
Tactic:
intro n hn z hz
State after:
case mpr
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
n : ℕ
hn : n ≠ 0
z : A
hz : z ∈ Ideal.span S
⊢ hI.dpow n z ∈ Ideal.span S

State before:
case mpr
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
n : ℕ
hn : n ≠ 0
z : A
hz : z ∈ Ideal.span S
⊢ hI.dpow n z ∈ Ideal.span S
Tactic:
revert n
State after:
case mpr
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
⊢ ∀ (n : ℕ), n ≠ 0 → hI.dpow n z ∈ Ideal.span S

State before:
case mpr
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
⊢ ∀ (n : ℕ), n ≠ 0 → hI.dpow n z ∈ Ideal.span S
Tactic:
refine' Submodule.span_induction' _ _  _ _ hz
State after:
case mpr.refine'_1
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
⊢ ∀ x ∈ S, ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S

case mpr.refine'_2
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
⊢ ∀ (n : ℕ), n ≠ 0 → hI.dpow n 0 ∈ Ideal.span S

case mpr.refine'_3
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
⊢ ∀ x ∈ Submodule.span A S,
    ∀ y ∈ Submodule.span A S,
      (∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S) →
        (∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S) → ∀ (n : ℕ), n ≠ 0 → hI.dpow n (x + y) ∈ Ideal.span S

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),
    x ∈ Submodule.span A S →
      (∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S) → ∀ (n : ℕ), n ≠ 0 → hI.dpow n (a • x) ∈ Ideal.span S

State before:
case mpr.refine'_1
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
⊢ ∀ x ∈ S, ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
Tactic:
intro s hs n hn
State after:
case mpr.refine'_1
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
s : A
hs : s ∈ S
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n s ∈ Ideal.span S

State before:
case mpr.refine'_1
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
s : A
hs : s ∈ S
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n s ∈ Ideal.span S
Tactic:
exact hhI n hn s hs
State after:
no goals

State before:
case mpr.refine'_2
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
⊢ ∀ (n : ℕ), n ≠ 0 → hI.dpow n 0 ∈ Ideal.span S
Tactic:
intro n hn
State after:
case mpr.refine'_2
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
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 ∈ Ideal.span S

State before:
case mpr.refine'_2
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
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 ∈ Ideal.span S
Tactic:
rw [hI.dpow_eval_zero hn]
State after:
case mpr.refine'_2
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
n : ℕ
hn : n ≠ 0
⊢ 0 ∈ Ideal.span S

State before:
case mpr.refine'_2
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
n : ℕ
hn : n ≠ 0
⊢ 0 ∈ Ideal.span S
Tactic:
apply Ideal.zero_mem _
State after:
no goals

State before:
case mpr.refine'_3
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
⊢ ∀ x ∈ Submodule.span A S,
    ∀ y ∈ Submodule.span A S,
      (∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S) →
        (∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S) → ∀ (n : ℕ), n ≠ 0 → hI.dpow n (x + y) ∈ Ideal.span S
Tactic:
rintro x hxI y hyI hx hy n hn
State after:
case mpr.refine'_3
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n (x + y) ∈ Ideal.span S

State before:
case mpr.refine'_3
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n (x + y) ∈ Ideal.span S
Tactic:
rw [hI.dpow_add' n (hSI hxI) (hSI hyI)]
State after:
case mpr.refine'_3
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
⊢ ∑ k ∈ Finset.range (n + 1), hI.dpow k x * hI.dpow (n - k) y ∈ Ideal.span S

State before:
case mpr.refine'_3
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
⊢ ∑ k ∈ Finset.range (n + 1), hI.dpow k x * hI.dpow (n - k) y ∈ Ideal.span S
Tactic:
apply Submodule.sum_mem (Ideal.span S)
State after:
case mpr.refine'_3
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
⊢ ∀ c ∈ Finset.range (n + 1), hI.dpow c x * hI.dpow (n - c) y ∈ Ideal.span S

State before:
case mpr.refine'_3
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
⊢ ∀ c ∈ Finset.range (n + 1), hI.dpow c x * hI.dpow (n - c) y ∈ Ideal.span S
Tactic:
intro m _
State after:
case mpr.refine'_3
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
m : ℕ
a✝ : m ∈ Finset.range (n + 1)
⊢ hI.dpow m x * hI.dpow (n - m) y ∈ Ideal.span S

State before:
case mpr.refine'_3
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
m : ℕ
a✝ : m ∈ Finset.range (n + 1)
⊢ hI.dpow m x * hI.dpow (n - m) y ∈ Ideal.span S
Tactic:
by_cases hm0 : m = 0
State after:
case pos
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
m : ℕ
a✝ : m ∈ Finset.range (n + 1)
hm0 : m = 0
⊢ hI.dpow m x * hI.dpow (n - m) y ∈ Ideal.span S

case neg
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
m : ℕ
a✝ : m ∈ Finset.range (n + 1)
hm0 : ¬m = 0
⊢ hI.dpow m x * hI.dpow (n - m) y ∈ Ideal.span S

State before:
case pos
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
m : ℕ
a✝ : m ∈ Finset.range (n + 1)
hm0 : m = 0
⊢ hI.dpow m x * hI.dpow (n - m) y ∈ Ideal.span S
Tactic:
rw [hm0]
State after:
case pos
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
m : ℕ
a✝ : m ∈ Finset.range (n + 1)
hm0 : m = 0
⊢ hI.dpow 0 x * hI.dpow (n - 0) y ∈ Ideal.span S

State before:
case pos
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
m : ℕ
a✝ : m ∈ Finset.range (n + 1)
hm0 : m = 0
⊢ hI.dpow 0 x * hI.dpow (n - 0) y ∈ Ideal.span S
Tactic:
exact Ideal.mul_mem_left (Ideal.span S) _ (hy n hn)
State after:
no goals

State before:
case neg
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
x : A
hxI : x ∈ Submodule.span A S
y : A
hyI : y ∈ Submodule.span A S
hx : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S
hy : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ Ideal.span S
n : ℕ
hn : n ≠ 0
m : ℕ
a✝ : m ∈ Finset.range (n + 1)
hm0 : ¬m = 0
⊢ hI.dpow m x * hI.dpow (n - m) y ∈ Ideal.span S
Tactic:
exact Ideal.mul_mem_right _ (Ideal.span S) (hx m hm0)
State after:
no goals

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),
    x ∈ Submodule.span A S →
      (∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ Ideal.span S) → ∀ (n : ℕ), n ≠ 0 → hI.dpow n (a • x) ∈ Ideal.span S
Tactic:
intro a x hxI hx n hn
State after:
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
⊢ hI.dpow n (a • x) ∈ Ideal.span S

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
⊢ hI.dpow n (a • x) ∈ Ideal.span S
Tactic:
simp only [Algebra.id.smul_eq_mul]
State after:
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
⊢ hI.dpow n (a * x) ∈ Ideal.span S

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
⊢ hI.dpow n (a * x) ∈ Ideal.span S
Tactic:
rw [hI.dpow_smul n (hSI hxI)]
State after:
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

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