-- Mathlib/AlgebraicGeometry/PointsPi.lean
lemma Ideal.span_eq_top_of_span_image_evalRingHom
    {ι} {R : ι → Type*} [∀ i, CommRing (R i)] (s : Set (Π i, R i))
    (hs : s.Finite) (hs' : ∀ i, Ideal.span (Pi.evalRingHom (R ·) i '' s) = ⊤) :
    Ideal.span s = ⊤

Proof state:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a => a * (⇑(Pi.evalRingHom (fun x => R x) i) ∘ Subtype.val) i_1) = 1
this : Fintype ↑s
⊢ ∃ c, (c.sum fun i a => a * ↑i) = 1

Tactic:
refine ⟨Finsupp.equivFunOnFinite.symm fun i x ↦ f x i, ?_⟩

Result:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a => a * (⇑(Pi.evalRingHom (fun x => R x) i) ∘ Subtype.val) i_1) = 1
this : Fintype ↑s
⊢ ((Finsupp.equivFunOnFinite.symm fun i x => (f x) i).sum fun i a => a * ↑i) = 1

Proof state:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' : ∀ (i : ι), ∃ c, (c.sum fun i_1 a => a * (⇑(Pi.evalRingHom (fun x => R x) i) ∘ Subtype.val) i_1) = 1
⊢ ∃ c, (c.sum fun i a => a * ↑i) = 1

Tactic:
choose f hf using hs'

Result:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a => a * (⇑(Pi.evalRingHom (fun x => R x) i) ∘ Subtype.val) i_1) = 1
⊢ ∃ c, (c.sum fun i a => a * ↑i) = 1

Proof state:
case h
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a => a * (⇑(Pi.evalRingHom (fun x => R x) i) ∘ Subtype.val) i_1) = 1
this : Fintype ↑s
i : ι
⊢ (Finsupp.equivFunOnFinite.symm fun i x => (f x) i).sum (fun i a => a * ↑i) i = 1 i

Tactic:
simpa [Finsupp.sum_fintype] using hf i

Result:
no goals

Proof state:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' : ∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x => R x) i) '' s) = ⊤
⊢ Ideal.span s = ⊤

Tactic:
simp only [Ideal.eq_top_iff_one, ← Subtype.range_val (s := s), ← Set.range_comp,
  Finsupp.mem_ideal_span_range_iff_exists_finsupp] at hs' ⊢

Result:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' : ∀ (i : ι), ∃ c, (c.sum fun i_1 a => a * (⇑(Pi.evalRingHom (fun x => R x) i) ∘ Subtype.val) i_1) = 1
⊢ ∃ c, (c.sum fun i a => a * ↑i) = 1

Proof state:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a => a * (⇑(Pi.evalRingHom (fun x => R x) i) ∘ Subtype.val) i_1) = 1
this : Fintype ↑s
⊢ ((Finsupp.equivFunOnFinite.symm fun i x => (f x) i).sum fun i a => a * ↑i) = 1

Tactic:
ext i

Result:
case h
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a => a * (⇑(Pi.evalRingHom (fun x => R x) i) ∘ Subtype.val) i_1) = 1
this : Fintype ↑s
i : ι
⊢ (Finsupp.equivFunOnFinite.symm fun i x => (f x) i).sum (fun i a => a * ↑i) i = 1 i

Proof state:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a => a * (⇑(Pi.evalRingHom (fun x => R x) i) ∘ Subtype.val) i_1) = 1
⊢ ∃ c, (c.sum fun i a => a * ↑i) = 1

Tactic:
have : Fintype s := hs.fintype

Result:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a => a * (⇑(Pi.evalRingHom (fun x => R x) i) ∘ Subtype.val) i_1) = 1
this : Fintype ↑s
⊢ ∃ c, (c.sum fun i a => a * ↑i) = 1