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

Proof state:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ span ((fun x => x ^ n) '' s) = ⊤

Tactic:
rw [eq_top_iff_one]

Result:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x => x ^ n) '' s)

Proof state:
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)

Tactic:
exact subset_span ⟨_, hx, pow_zero _⟩

Result:
no goals

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)
⊢ 1 ∈ span ((fun x => x ^ (n + 1)) '' s)

Tactic:
refine span_le.mpr ?_ this

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)
⊢ (fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support ⊆ ↑(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)
⊢ (f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))

Tactic:
refine this ?_

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
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ (f x * ↑x) ^ (n + 1) ∈ span {↑x ^ (n + 1)}

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
⊢ ↑x ^ (n + 1) ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))

Tactic:
exact subset_span ⟨x, x.prop, rfl⟩

Result:
no goals

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

Tactic:
rw [eq_top_iff_one, span, Finsupp.mem_span_iff_linearCombination] at hs

Result:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : ∃ l, (Finsupp.linearCombination α Subtype.val) l = 1
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 : (∑ 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)

Tactic:
rw [hf, one_pow] at this

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)
⊢ 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
⊢ (f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))

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

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
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ (f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))

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

Tactic:
rcases n with - | n

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

case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 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)
⊢ (f x * ↑x) ^ (n + 1) ∈ span {↑x ^ (n + 1)}

Tactic:
rw [mul_pow, mem_span_singleton]

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
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ ↑x ^ (n + 1) ∣ f x ^ (n + 1) * ↑x ^ (n + 1)

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

Tactic:
have hf : (f.support.sum fun a => f a * a) = 1 := hf

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
⊢ 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 : a✝ ∈ (fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support
⊢ a✝ ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))

Tactic:
simp_rw [Set.mem_image] at 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 : ∃ x ∈ ↑f.support, (f x * ↑x) ^ (n + 1) = a✝
⊢ a✝ ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))

Proof state:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : ∃ l, (Finsupp.linearCombination α Subtype.val) l = 1
n : ℕ
⊢ 1 ∈ span ((fun x => x ^ (n + 1)) '' s)

Tactic:
rcases hs with ⟨f, hf⟩

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

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

Tactic:
trivial

Result:
no goals