-- 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:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i => Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↑↑V.toPresheafedSpace
I : Ideal ↑(CommRingCat.of ((i : ι) → ↑(R i)))
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ I))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
⊢ (f ≫ e.hom) ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R

Tactic:
rwa [Category.assoc]

Result:
no goals

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 = ⊤
⊢ IsClosedImmersion g

Tactic:
have : IsIso g.coborderRange.ι := by rw [this, ← Scheme.topIso_hom]; infer_instance

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 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 (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).topIso.hom

Tactic:
infer_instance

Result:
no goals

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

Tactic:
obtain rfl := eq_bot_of_comp_quotientMk_eq_sigmaSpec R I (f ≫ e.hom) (by rwa [Category.assoc])

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 (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))

Proof state:
case hV'
ι : 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
⊢ IsCompact (Set.range ⇑(ConcreteCategory.hom g.base))

Tactic:
exact isCompact_range g.base.hom.2

Result:
no goals

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
⊢ Scheme.Hom.coborderRange g = ⊤

Tactic:
apply eq_top_of_sigmaSpec_subset_of_isCompact (hVU := subset_coborder)

Result:
case hV
ι : 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
⊢ ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ Set.range ⇑(ConcreteCategory.hom g.base)

case hV'
ι : 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
⊢ IsCompact (Set.range ⇑(ConcreteCategory.hom g.base))

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 (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)

Tactic:
infer_instance

Result:
no goals

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 g

Tactic:
have : IsClosedImmersion g := by
  have : IsIso g.coborderRange.ι := by rw [this, ← Scheme.topIso_hom]; infer_instance
  rw [← g.liftCoborder_ι]
  infer_instance

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 : IsClosedImmersion g
⊢ IsIso 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 = ⊤
this : IsClosedImmersion g
⊢ IsIso g

Tactic:
obtain ⟨I, e, rfl⟩ := IsClosedImmersion.Spec_iff.mp this

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

Proof state:
case hV
ι : 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
⊢ ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
simpa only [← hU'] using Set.range_comp_subset_range f.base g.base

Result:
no goals