α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x => x ^ n) '' s)
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ span ((fun x => x ^ n) '' s) = ⊤
rw [eq_top_iff_one]
case zero
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
⊢ 1 ∈ span ((fun x => x ^ Nat.zero) '' s)

case succ
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x => x ^ n) '' s)
cases' n with n
case succ
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : ∃ l, ↑(Finsupp.total (↑s) α α Subtype.val) l = 1
n : ℕ
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
case succ
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
rw [eq_top_iff_one, span, Finsupp.mem_span_iff_total] at hs
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
case succ
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : ∃ l, ↑(Finsupp.total (↑s) α α Subtype.val) l = 1
n : ℕ
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
rcases hs with ⟨f, hf⟩
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
have hf : (f.support.sum fun a => f a * a) = 1 := hf
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this :
  (∑ i in f.support, ↑f i * ↑i) ^ (Finset.card f.support * n + 1) ∈
    span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
have := sum_pow_mem_span_pow f.support (fun a => f a * a) n
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this :
  (∑ i in f.support, ↑f i * ↑i) ^ (Finset.card f.support * n + 1) ∈
    span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
rw [hf, one_pow] at this
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ (fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support ⊆ ↑(span ((fun x => x ^ Nat.succ n) '' s))
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
refine' span_le.mpr _ this
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
a✝ : α
hx : a✝ ∈ (fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support
⊢ a✝ ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ (fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support ⊆ ↑(span ((fun x => x ^ Nat.succ n) '' s))
rintro _ hx
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
a✝ : α
hx : ∃ x, x ∈ ↑f.support ∧ (↑f x * ↑x) ^ (n + 1) = a✝
⊢ a✝ ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
a✝ : α
hx : a✝ ∈ (fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support
⊢ a✝ ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
simp_rw [Set.mem_image] at hx
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ (↑f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
a✝ : α
hx : ∃ x, x ∈ ↑f.support ∧ (↑f x * ↑x) ^ (n + 1) = a✝
⊢ a✝ ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
rcases hx with ⟨x, _, rfl⟩
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this✝ : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ (↑f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ (↑f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
have : span ({(x:α) ^ (n + 1)} : Set α) ≤ span ((fun x : α => x ^ (n + 1)) '' s) := by
  rw [span_le, Set.singleton_subset_iff]
  exact subset_span ⟨x, x.prop, rfl⟩
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this✝ : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ (↑f x * ↑x) ^ (n + 1) ∈ span {↑x ^ (n + 1)}
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this✝ : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ (↑f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
refine' this _
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this✝ : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ ↑x ^ (n + 1) ∣ ↑f x ^ (n + 1) * ↑x ^ (n + 1)
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this✝ : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ (↑f x * ↑x) ^ (n + 1) ∈ span {↑x ^ (n + 1)}
rw [mul_pow, mem_span_singleton]
no goals
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this✝ : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ ↑x ^ (n + 1) ∣ ↑f x ^ (n + 1) * ↑x ^ (n + 1)
exact ⟨f x ^ (n + 1), mul_comm _ _⟩
case zero.inl
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
hs : span ∅ = ⊤
⊢ 1 ∈ span ((fun x => x ^ Nat.zero) '' ∅)

case zero.inr.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
x : α
hx : x ∈ s
⊢ 1 ∈ span ((fun x => x ^ Nat.zero) '' s)
case zero
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
⊢ 1 ∈ span ((fun x => x ^ Nat.zero) '' s)
obtain rfl | ⟨x, hx⟩ := eq_empty_or_nonempty s
case zero.inl
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
hs : span ∅ = ⊤
⊢ 1 ∈ ⊤
case zero.inl
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
hs : span ∅ = ⊤
⊢ 1 ∈ span ((fun x => x ^ Nat.zero) '' ∅)
rw [Set.image_empty, hs]
no goals
case zero.inl
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
hs : span ∅ = ⊤
⊢ 1 ∈ ⊤
trivial
no goals
case zero.inr.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
x : α
hx : x ∈ s
⊢ 1 ∈ span ((fun x => x ^ Nat.zero) '' s)
exact subset_span ⟨_, hx, pow_zero _⟩
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ ↑x ^ (n + 1) ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
rw [span_le, Set.singleton_subset_iff]
no goals
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ ↑x ^ (n + 1) ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))
exact subset_span ⟨x, x.prop, rfl⟩