-- Mathlib/RingTheory/Ideal/Basic.lean
theorem span_pow_eq_top (s : Set α) (hs : span s = ⊤) (n : ℕ) :
    span ((fun (x : α) => x ^ n) '' s) = ⊤

Proof state:
case succ.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : (Finsupp.linearCombination α Subtype.val) f = 1
hf : ∑ a ∈ 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 ^ (n + 1)) '' s))

Tactic:
rintro _ hx

Result:
case succ.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : (Finsupp.linearCombination α Subtype.val) f = 1
hf : ∑ a ∈ 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 ^ (n + 1)) '' s))

Proof state:
case zero
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
⊢ 1 ∈ span ((fun x => x ^ 0) '' s)

Tactic:
obtain rfl | ⟨x, hx⟩ := eq_empty_or_nonempty s

Result:
case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ span ((fun x => x ^ 0) '' ∅)

case zero.inr.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
x : α
hx : x ∈ s
⊢ 1 ∈ span ((fun x => x ^ 0) '' s)

Proof state:
case succ.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : (Finsupp.linearCombination α Subtype.val) f = 1
hf : ∑ a ∈ f.support, f a * ↑a = 1
⊢ 1 ∈ span ((fun x => x ^ (n + 1)) '' s)

Tactic:
have := sum_pow_mem_span_pow f.support (fun a => f a * a) n

Result:
case succ.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : (Finsupp.linearCombination α Subtype.val) f = 1
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : (∑ i ∈ f.support, f i * ↑i) ^ (f.support.card * n + 1) ∈ span ((fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x => x ^ (n + 1)) '' s)

Proof state:
case succ.intro.intro.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : (Finsupp.linearCombination α Subtype.val) f = 1
hf : ∑ a ∈ 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)

Tactic:
exact ⟨f x ^ (n + 1), mul_comm _ _⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : (Finsupp.linearCombination α Subtype.val) f = 1
hf : ∑ a ∈ 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)

Tactic:
rw [span_le, Set.singleton_subset_iff]

Result:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : (Finsupp.linearCombination α Subtype.val) f = 1
hf : ∑ a ∈ 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))

Proof state:
case succ.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : (Finsupp.linearCombination α Subtype.val) f = 1
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support)
a✝ : α
hx : ∃ x ∈ ↑f.support, (f x * ↑x) ^ (n + 1) = a✝
⊢ a✝ ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))

Tactic:
rcases hx with ⟨x, _, rfl⟩

Result:
case succ.intro.intro.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : (Finsupp.linearCombination α Subtype.val) f = 1
hf : ∑ a ∈ 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 ^ (n + 1)) '' s))

Proof state:
case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ span ((fun x => x ^ 0) '' ∅)

Tactic:
rw [Set.image_empty, hs]

Result:
case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ ⊤