-- 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)
i : ι
⊢ ∃ j, Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆ ↑(Scheme.Hom.opensRange (𝒰.map j))

Tactic:
refine ⟨𝒰.f ((f i).base (IsLocalRing.closedPoint (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)
i : ι
⊢ Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆
    ↑(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)
⊢ Function.Surjective (pointsPi R X)

Tactic:
intro f

Result:
ι : 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

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)))
this : ∀ (j₀ : 𝒰.J), ∃ a, pointsPi (fun x => R ↑x) (𝒰.obj j₀) a = fun i => IsOpenImmersion.lift (𝒰.map j₀) (f ↑i) ⋯
⊢ ∃ a, pointsPi R X a = f

Tactic:
choose g hg 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)))
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

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

Tactic:
exact ((IsLocalRing.specializes_closedPoint x).map (f i).base.hom.2).mem_open
  (𝒰.map _).opensRange.2 (𝒰.covers _)

Result:
no goals

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

Tactic:
exact hj i

Result:
no goals

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))
x✝ : (j₀ : 𝒰.J) → ↑(R' j₀)
j₀ : 𝒰.J
i : { i // j i = j₀ }
⊢ (fun f x i => f ↑i) ((fun f i => f (j i) ⟨i, ⋯⟩) x✝) j₀ i = x✝ j₀ i

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)))
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))
x✝ : (j₀ : 𝒰.J) → ↑(R' j₀)
i : ι
⊢ (fun f x i => f ↑i) ((fun f i => f (j i) ⟨i, ⋯⟩) x✝) (j i) ⟨i, ⋯⟩ = x✝ (j i) ⟨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
⊢ ∃ a, pointsPi R X a = f

Tactic:
have (i) : IsAffine (𝒰.obj i) := isAffine_Spec _

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)
⊢ ∃ 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)
⊢ ∃ a, pointsPi R X a = f

Tactic:
have (i) : ∃ j, Set.range (f i).base ⊆ (𝒰.map j).opensRange := by
  refine ⟨𝒰.f ((f i).base (IsLocalRing.closedPoint (R i))), ?_⟩
  rintro _ ⟨x, rfl⟩
  exact ((IsLocalRing.specializes_closedPoint x).map (f i).base.hom.2).mem_open
    (𝒰.map _).opensRange.2 (𝒰.covers _)

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)
this : ∀ (i : ι), ∃ j, Set.range ⇑(ConcreteCategory.hom (f i).base) ⊆ ↑(Scheme.Hom.opensRange (𝒰.map j))
⊢ ∃ a, pointsPi R X a = f

Proof state:
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)))
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))
x✝ : (j₀ : 𝒰.J) → ↑(R' j₀)
i : ι
⊢ (fun f x i => f ↑i) ((fun f i => f (j i) ⟨i, ⋯⟩) x✝) (j i) ⟨i, ⋯⟩ = x✝ (j i) ⟨i, ⋯⟩

Tactic:
rfl

Result:
no goals