-- Mathlib/AlgebraicGeometry/PointsPi.lean
/-- If `V` is a locally closed subscheme of `Spec (Π Rᵢ)` containing `∐ Spec Rᵢ`, then
`V = Spec (Π Rᵢ)`. -/
lemma isIso_of_comp_eq_sigmaSpec {V : Scheme}
    (f : (∐ fun i ↦ Spec (R i)) ⟶ V) (g : V ⟶ Spec (.of (Π i, R i)))
    [IsImmersion g] [CompactSpace V]
    (hU' : f ≫ g = sigmaSpec R) : IsIso g

Proof state:
case intro.intro
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i => Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↑↑V.toPresheafedSpace
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ ⊥))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
⊢ IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))

Tactic:
convert_to IsIso (e.hom ≫ Spec.map (RingEquiv.quotientBot _).toCommRingCatIso.inv)

Result:
case intro.intro
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i => Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↑↑V.toPresheafedSpace
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ ⊥))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
⊢ IsIso (e.hom ≫ Spec.map (RingEquiv.quotientBot ↑(CommRingCat.of ((i : ι) → ↑(R i)))).toCommRingCatIso.inv)

Proof state:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i => Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↑↑V.toPresheafedSpace
hU' : f ≫ g = sigmaSpec R
this✝ : Scheme.Hom.coborderRange g = ⊤
this : IsIso (Scheme.Hom.coborderRange g).ι
⊢ IsClosedImmersion g

Tactic:
rw [← g.liftCoborder_ι]

Result:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i => Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↑↑V.toPresheafedSpace
hU' : f ≫ g = sigmaSpec R
this✝ : Scheme.Hom.coborderRange g = ⊤
this : IsIso (Scheme.Hom.coborderRange g).ι
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)

Proof state:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i => Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↑↑V.toPresheafedSpace
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
⊢ IsIso (Scheme.Hom.coborderRange g).ι

Tactic:
rw [this, ← Scheme.topIso_hom]

Result:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i => Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↑↑V.toPresheafedSpace
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
⊢ IsIso (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).topIso.hom

Proof state:
case intro.intro
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i => Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↑↑V.toPresheafedSpace
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ ⊥))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
⊢ IsIso (e.hom ≫ Spec.map (RingEquiv.quotientBot ↑(CommRingCat.of ((i : ι) → ↑(R i)))).toCommRingCatIso.inv)

Tactic:
infer_instance

Result:
no goals