-- Mathlib/AlgebraicGeometry/Limits.lean
lemma isOpenImmersion_sigmaDesc
    {X : Scheme} (α : ∀ i, f i ⟶ X) [∀ i, IsOpenImmersion (α i)]
    (hα : Pairwise (Disjoint on (Set.range <| α · |>.base))) :
    IsOpenImmersion (Sigma.desc α)

Proof state:
case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
⊢ IsOpenMap (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f))

Tactic:
rw [isOpenMap_sigma]

Result:
case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
⊢ ∀ (i : ι), IsOpenMap fun a => (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f)) ⟨i, a⟩

Proof state:
case right.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
x : ↑↑(∐ f).toPresheafedSpace
y : ↑↑((sigmaOpenCover f).obj ((sigmaOpenCover f).f x)).toPresheafedSpace
hy : (ConcreteCategory.hom ((sigmaOpenCover f).map ((sigmaOpenCover f).f x)).base) y = x
⊢ Scheme.Hom.stalkMap (Sigma.desc α) ((ConcreteCategory.hom ((sigmaOpenCover f).map ((sigmaOpenCover f).f x)).base) y) ≫
      Scheme.Hom.stalkMap ((sigmaOpenCover f).map ((sigmaOpenCover f).f x)) y =
    (X.presheaf.stalkCongr ⋯).hom ≫ Scheme.Hom.stalkMap (α ((sigmaOpenCover f).f x)) y

Tactic:
simp [← Scheme.stalkMap_comp, Scheme.stalkMap_congr_hom _ _ (Sigma.ι_desc _ _)]

Result:
no goals

Proof state:
case h.e'_5.h
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
this : Topology.IsOpenEmbedding (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f))
x✝ : ↑↑(∐ f).toPresheafedSpace
⊢ (ConcreteCategory.hom (Sigma.desc α).base) x✝ =
    ((⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f)) ∘ ⇑(sigmaMk f).symm) x✝

Tactic:
simp

Result:
no goals

Proof state:
case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
⊢ ∀ (i : ι), IsOpenMap fun a => (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f)) ⟨i, a⟩

Tactic:
intro i

Result:
case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
i : ι
⊢ IsOpenMap fun a => (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f)) ⟨i, a⟩

Proof state:
case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
i : ι
⊢ IsOpenMap fun a => (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f)) ⟨i, a⟩

Tactic:
simpa [← Scheme.comp_base_apply] using (α i).isOpenEmbedding.isOpenMap

Result:
no goals

Proof state:
case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
x : ↑↑(∐ f).toPresheafedSpace
y : ↑↑((sigmaOpenCover f).obj ((sigmaOpenCover f).f x)).toPresheafedSpace
hy : (ConcreteCategory.hom ((sigmaOpenCover f).map ((sigmaOpenCover f).f x)).base) y = x
⊢ IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
rw [← hy]

Result:
case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
x : ↑↑(∐ f).toPresheafedSpace
y : ↑↑((sigmaOpenCover f).obj ((sigmaOpenCover f).f x)).toPresheafedSpace
hy : (ConcreteCategory.hom ((sigmaOpenCover f).map ((sigmaOpenCover f).f x)).base) y = x
⊢ IsIso
    (Scheme.Hom.stalkMap (Sigma.desc α)
      ((ConcreteCategory.hom ((sigmaOpenCover f).map ((sigmaOpenCover f).f x)).base) y))

Proof state:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
⊢ IsOpenImmersion (Sigma.desc α)

Tactic:
rw [IsOpenImmersion.iff_stalk_iso]

Result:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
⊢ Topology.IsOpenEmbedding ⇑(ConcreteCategory.hom (Sigma.desc α).base) ∧
    ∀ (x : ↑↑(∐ f).toPresheafedSpace), IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)

Proof state:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x => Set.range ⇑(ConcreteCategory.hom (α x).base))
ix : ι
x : ↑↑(f ix).toPresheafedSpace
iy : ι
y : ↑↑(f iy).toPresheafedSpace
e :
  (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f)) ⟨ix, x⟩ =
    (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f)) ⟨iy, y⟩
this : (ConcreteCategory.hom (α ix).base) x = (ConcreteCategory.hom (α iy).base) y
h : ¬ix = iy
⊢ False

Tactic:
exact Set.disjoint_iff_forall_ne.mp (hα h) ⟨x, rfl⟩ ⟨y, this.symm⟩ rfl

Result:
no goals