internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.isSubDPIdeal_inf_iff
Proof state before:
case refine'_1.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ ∀ c ∈ Finset.range n, hI.dpow c b * hI.dpow (n - c) (a - b) ∈ J
Tactic:
intro i hi
Proof state after:
case refine'_1.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
i : ℕ
hi : i ∈ Finset.range n
⊢ hI.dpow i b * hI.dpow (n - i) (a - b) ∈ J
Theorem: DividedPowers.isSubDPIdeal_inf_iff
Proof state before:
case refine'_1.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
i : ℕ
hi : i ∈ Finset.range n
⊢ hI.dpow i b * hI.dpow (n - i) (a - b) ∈ J
Tactic:
apply SemilatticeInf.inf_le_left J I
Proof state after:
case refine'_1.a.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
i : ℕ
hi : i ∈ Finset.range n
⊢ hI.dpow i b * hI.dpow (n - i) (a - b) ∈ J ⊓ I
Theorem: DividedPowers.isSubDPIdeal_inf_iff
Proof state before:
case refine'_1.a.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
i : ℕ
hi : i ∈ Finset.range n
⊢ hI.dpow i b * hI.dpow (n - i) (a - b) ∈ J ⊓ I
Tactic:
exact
  (J ⊓ I).smul_mem _
    (hIJ.dpow_mem (n - i) (ne_of_gt (Nat.sub_pos_of_lt (Finset.mem_range.mp hi))) _
      ⟨hab, hab'⟩)
Proof state after:
no goals
Theorem: DividedPowers.isSubDPIdeal_inf_iff
Proof state before:
case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
⊢ hI.isSubDPIdeal (J ⊓ I)
Tactic:
refine' ⟨SemilatticeInf.inf_le_right J I, fun n hn a ha => ⟨_, hI.dpow_mem hn ha.right⟩⟩
Proof state after:
case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a ∈ ↑J
Theorem: DividedPowers.isSubDPIdeal_inf_iff
Proof state before:
case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a ∈ ↑J
Tactic:
rw [← sub_zero (hI.dpow n a), ← hI.dpow_eval_zero hn]
Proof state after:
case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a - hI.dpow n 0 ∈ ↑J
Theorem: DividedPowers.isSubDPIdeal_inf_iff
Proof state before:
case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a - hI.dpow n 0 ∈ ↑J
Tactic:
exact hIJ n a 0 ha.right I.zero_mem (J.sub_mem ha.left J.zero_mem)
Proof state after:
no goals
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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)
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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)
Proof state after:
no goals
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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)
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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)
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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]
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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 _
Proof state after:
no goals
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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)]
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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)
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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 _
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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]
Proof 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
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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)
Proof state after:
no goals
Theorem: DividedPowers.span_isSubDPIdeal_iff
Proof 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)
Proof state after:
no goals
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),
    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
Proof 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
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
⊢ hI.dpow n (a • x) ∈ Ideal.span S
Tactic:
simp only [Algebra.id.smul_eq_mul]
Proof 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
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
⊢ hI.dpow n (a * x) ∈ Ideal.span S
Tactic:
rw [hI.dpow_smul n (hSI hxI)]
Proof 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