-- 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) (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))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.J) → ↑(R' j₀)) :=
  { toFun := fun f x i => f ↑i, invFun := fun f i => f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
⊢ pointsPi R X
      (Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ => g j₀ ≫ 𝒰.map j₀) =
    f

Tactic:
ext i : 1

Result:
case h
ι : 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))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.J) → ↑(R' j₀)) :=
  { toFun := fun f x i => f ↑i, invFun := fun f i => f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
⊢ pointsPi R X
      (Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ => g j₀ ≫ 𝒰.map j₀) i =
    f 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) ⋯
R' : 𝒰.J → CommRingCat := fun j₀ => CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
⊢ ∃ a, pointsPi R X a = f

Tactic:
let e : (Π i, R i) ≃+* Π j₀, R' j₀ :=
{ toFun f _ i := f i
  invFun f i := f _ ⟨i, rfl⟩
  left_inv _ := rfl
  right_inv _ := funext₂ fun j₀ i ↦ by rcases i with ⟨i, rfl⟩; rfl
  map_mul' _ _ := rfl
  map_add' _ _ := rfl }

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))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.J) → ↑(R' j₀)) :=
  { toFun := fun f x i => f ↑i, invFun := fun f i => f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
⊢ ∃ 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)))
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))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.J) → ↑(R' j₀)) :=
  { toFun := fun f x i => f ↑i, invFun := fun f i => f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
⊢ ∃ a, pointsPi R X a = f

Tactic:
refine ⟨Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫
  Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.map j₀, ?_⟩

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))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.J) → ↑(R' j₀)) :=
  { toFun := fun f x i => f ↑i, invFun := fun f i => f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
⊢ pointsPi R X
      (Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ => g j₀ ≫ 𝒰.map j₀) =
    f

Proof state:
case h
ι : 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))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.J) → ↑(R' j₀)) :=
  { toFun := fun f x i => f ↑i, invFun := fun f i => f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x => ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 => ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x => ↑(R' x)) (j i))
⊢ pointsPi R X
      (Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ => g j₀ ≫ 𝒰.map j₀) i =
    f i

Tactic:
rw [pointsPi, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, this, CommRingCat.ofHom_comp,
  Spec.map_comp_assoc, ← ι_sigmaSpec R', Category.assoc, IsIso.hom_inv_id_assoc,
  Sigma.ι_desc, ← Category.assoc, hg, IsOpenImmersion.lift_fac]

Result:
no goals