-- Mathlib/RingTheory/Ideal/Basic.lean
theorem span_range_pow_eq_top (s : Set α) (hs : span s = ⊤) (n : s → ℕ) :
    span (Set.range fun x ↦ x.1 ^ n x) = ⊤

Proof state:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
⊢ span (range fun x => ↑x ^ n x) = ⊤

Tactic:
refine top_unique ((span_pow_eq_top _ ((eq_top_iff_one _).mpr mem) <|
  t.attach.sup fun x ↦ n ⟨x, hts x.2⟩).ge.trans <| span_le.mpr ?_)

Result:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
⊢ (fun x => x ^ t.attach.sup fun x => n ⟨↑x, ⋯⟩) '' ↑t ⊆ ↑(span (range fun x => ↑x ^ n x))

Proof state:
case intro.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
x : α
hxt : x ∈ ↑t
⊢ x ^ ((t.attach.sup fun x => n ⟨↑x, ⋯⟩) - n ⟨x, ⋯⟩) * x ^ n ⟨x, ⋯⟩ ∈ ↑(span (range fun x => ↑x ^ n x))

Tactic:
exact mul_mem_left _ _ (subset_span ⟨_, rfl⟩)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
⊢ (fun x => x ^ t.attach.sup fun x => n ⟨↑x, ⋯⟩) '' ↑t ⊆ ↑(span (range fun x => ↑x ^ n x))

Tactic:
rintro _ ⟨x, hxt, rfl⟩

Result:
case intro.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
x : α
hxt : x ∈ ↑t
⊢ (fun x => x ^ t.attach.sup fun x => n ⟨↑x, ⋯⟩) x ∈ ↑(span (range fun x => ↑x ^ n x))

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

Tactic:
have ⟨t, hts, mem⟩ := Submodule.mem_span_finite_of_mem_span ((eq_top_iff_one _).mp hs)

Result:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
⊢ span (range fun x => ↑x ^ n x) = ⊤

Proof state:
case intro.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
x : α
hxt : x ∈ ↑t
⊢ (fun x_1 => x_1 ^ ((t.attach.sup fun x => n ⟨↑x, ⋯⟩) - n ⟨↑⟨x, hxt⟩, ⋯⟩ + n ⟨↑⟨x, hxt⟩, ⋯⟩)) x ∈
    ↑(span (range fun x => ↑x ^ n x))

Tactic:
simp_rw [pow_add]

Result:
case intro.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
x : α
hxt : x ∈ ↑t
⊢ x ^ ((t.attach.sup fun x => n ⟨↑x, ⋯⟩) - n ⟨x, ⋯⟩) * x ^ n ⟨x, ⋯⟩ ∈ ↑(span (range fun x => ↑x ^ n x))

Proof state:
case intro.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
x : α
hxt : x ∈ ↑t
⊢ (fun x => x ^ t.attach.sup fun x => n ⟨↑x, ⋯⟩) x ∈ ↑(span (range fun x => ↑x ^ n x))

Tactic:
rw [← Nat.sub_add_cancel (Finset.le_sup <| t.mem_attach ⟨x, hxt⟩)]

Result:
case intro.intro
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
x : α
hxt : x ∈ ↑t
⊢ (fun x_1 => x_1 ^ ((t.attach.sup fun x => n ⟨↑x, ⋯⟩) - n ⟨↑⟨x, hxt⟩, ⋯⟩ + n ⟨↑⟨x, hxt⟩, ⋯⟩)) x ∈
    ↑(span (range fun x => ↑x ^ n x))