-- Mathlib/AlgebraicGeometry/PointsPi.lean
lemma pointsPi_surjective [CompactSpace X] [∀ i, IsLocalRing (R i)] :
    Function.Surjective (pointsPi R X)

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
j : ι → 𝒰.J
hj : ∀ (i : ι), Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆ ↑(Scheme.Hom.opensRange (𝒰.map (j i)))
g : (j₀ : 𝒰.J) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.obj j₀
hg : ∀ (j₀ : 𝒰.J), pointsPi (fun x => R ↑x) (𝒰.obj j₀) (g j₀) = fun i => IsOpenImmersion.lift (𝒰.map j₀) (f ↑i) ⋯
⊢ ∃ a, pointsPi R X a = f

Tactic:
simp_rw [funext_iff, pointsPi] at hg

Result:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
j : ι → 𝒰.J
hj : ∀ (i : ι), Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆ ↑(Scheme.Hom.opensRange (𝒰.map (j i)))
g : (j₀ : 𝒰.J) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.obj j₀
hg :
  ∀ (j₀ : 𝒰.J) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x => ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.map j₀) (f ↑x) ⋯
⊢ ∃ a, pointsPi R X a = f

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
i : ι
⊢ Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆
    ↑(Scheme.Hom.opensRange (𝒰.map (𝒰.f ((ConcreteCategory.hom (f i).base) (IsLocalRing.closedPoint ↑(R i))))))

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
i : ι
x : ↑↑(Spec (R i)).toPresheafedSpace
⊢ (ConcreteCategory.hom (f i).base) x ∈
    ↑(Scheme.Hom.opensRange (𝒰.map (𝒰.f ((ConcreteCategory.hom (f i).base) (IsLocalRing.closedPoint ↑(R i))))))

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
j : ι → 𝒰.J
hj : ∀ (i : ι), Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆ ↑(Scheme.Hom.opensRange (𝒰.map (j i)))
g : (j₀ : 𝒰.J) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.obj j₀
hg :
  ∀ (j₀ : 𝒰.J) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x => ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.map j₀) (f ↑x) ⋯
⊢ ∃ a, pointsPi R X a = f

Tactic:
let R' (j₀) := CommRingCat.of (Π i : { i // j i = j₀ }, R i)

Result:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
j : ι → 𝒰.J
hj : ∀ (i : ι), Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆ ↑(Scheme.Hom.opensRange (𝒰.map (j i)))
g : (j₀ : 𝒰.J) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.obj j₀
hg :
  ∀ (j₀ : 𝒰.J) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x => ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.map j₀) (f ↑x) ⋯
R' : 𝒰.J → CommRingCat := fun j₀ => CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
⊢ ∃ a, pointsPi R X a = f

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
j : ι → 𝒰.J
hj : ∀ (i : ι), Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆ ↑(Scheme.Hom.opensRange (𝒰.map (j i)))
j₀ : 𝒰.J
i : { i // j i = j₀ }
⊢ Set.range ⇑(ConcreteCategory.hom (f ↑i).base) ⊆ Set.range ⇑(ConcreteCategory.hom (𝒰.map j₀).base)

Tactic:
rcases i with ⟨i, rfl⟩

Result:
case mk
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
j : ι → 𝒰.J
hj : ∀ (i : ι), Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆ ↑(Scheme.Hom.opensRange (𝒰.map (j i)))
i : ι
⊢ Set.range ⇑(ConcreteCategory.hom (f ↑⟨i, ⋯⟩).base) ⊆ Set.range ⇑(ConcreteCategory.hom (𝒰.map (j i)).base)

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
⊢ ∃ a, pointsPi R X a = f

Tactic:
let 𝒰 : X.OpenCover := X.affineCover.finiteSubcover

Result:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ ∃ a, pointsPi R X a = f

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
this : ∀ (i : ι), ∃ j, Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆ ↑(Scheme.Hom.opensRange (𝒰.map j))
⊢ ∃ a, pointsPi R X a = f

Tactic:
choose j hj using this

Result:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
j : ι → 𝒰.J
hj : ∀ (i : ι), Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆ ↑(Scheme.Hom.opensRange (𝒰.map (j i)))
⊢ ∃ a, pointsPi R X a = f