-- 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:
ι : 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))
⊢ Topology.IsOpenEmbedding ⇑(ConcreteCategory.hom (Sigma.desc α).base)

Tactic:
convert this.comp (sigmaMk f).symm.isOpenEmbedding

Result:
case h.e'_5
ι : 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))
⊢ ⇑(ConcreteCategory.hom (Sigma.desc α).base) =
    (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f)) ∘ ⇑(sigmaMk f).symm

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⟩
⊢ (ConcreteCategory.hom (α ix).base) x = (ConcreteCategory.hom (α iy).base) y

Tactic:
simpa [← Scheme.comp_base_apply] using e

Result:
no goals

Proof state:
case left.refine_2.mk.mk
ι : 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
⊢ ⟨ix, x⟩ = ⟨iy, y⟩

Tactic:
obtain rfl : ix = iy := by
  by_contra h
  exact Set.disjoint_iff_forall_ne.mp (hα h) ⟨x, rfl⟩ ⟨y, this.symm⟩ rfl

Result:
case left.refine_2.mk.mk
ι : 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 y : ↑↑(f ix).toPresheafedSpace
e :
  (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f)) ⟨ix, x⟩ =
    (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f)) ⟨ix, y⟩
this : (ConcreteCategory.hom (α ix).base) x = (ConcreteCategory.hom (α ix).base) y
⊢ ⟨ix, x⟩ = ⟨ix, y⟩

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 α)
      ((ConcreteCategory.hom ((sigmaOpenCover f).map ((sigmaOpenCover f).f x)).base) y))

Tactic:
refine IsIso.of_isIso_fac_right (g := ((sigmaOpenCover f).map _).stalkMap y)
  (h := (X.presheaf.stalkCongr (.of_eq ?_)).hom ≫ (α _).stalkMap _) ?_

Result:
case right.refine_1
ι : 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
⊢ (ConcreteCategory.hom (Sigma.desc α).base)
      ((ConcreteCategory.hom ((sigmaOpenCover f).map ((sigmaOpenCover f).f x)).base) y) =
    (ConcreteCategory.hom (α ((sigmaOpenCover f).f x)).base) y

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

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))
⊢ Topology.IsOpenEmbedding ⇑(ConcreteCategory.hom (Sigma.desc α).base) ∧
    ∀ (x : ↑↑(∐ f).toPresheafedSpace), IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
constructor

Result:
case left
ι : 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)

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), IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)

Proof state:
case left.refine_1
ι : 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))
⊢ Continuous (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f))

Tactic:
fun_prop

Result:
no goals

Proof state:
case right.refine_1
ι : 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
⊢ (ConcreteCategory.hom (Sigma.desc α).base)
      ((ConcreteCategory.hom ((sigmaOpenCover f).map ((sigmaOpenCover f).f x)).base) y) =
    (ConcreteCategory.hom (α ((sigmaOpenCover f).f x)).base) y

Tactic:
simp [← Scheme.comp_base_apply]

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
⊢ IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
have ⟨y, hy⟩ := (sigmaOpenCover f).covers x

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 α) x)