-- 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
ι : 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) ∘ ⇑(sigmaMk f))

Tactic:
refine .of_continuous_injective_isOpenMap ?_ ?_ ?_

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

case left.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))
⊢ Function.Injective (⇑(ConcreteCategory.hom (Sigma.desc α).base) ∘ ⇑(sigmaMk f))

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

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

Tactic:
suffices Topology.IsOpenEmbedding ((Sigma.desc α).base ∘ sigmaMk f) by
  convert this.comp (sigmaMk f).symm.isOpenEmbedding; ext; simp

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) ∘ ⇑(sigmaMk f))

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

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 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⟩

Tactic:
rw [(α ix).isOpenEmbedding.injective this]

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⟩
⊢ ⟨ix, x⟩ = ⟨iy, y⟩

Tactic:
have : (α ix).base x = (α iy).base y := by
  simpa [← Scheme.comp_base_apply] using e

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 : ↑↑(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⟩

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

Tactic:
ext

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

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
⊢ ix = iy

Tactic:
by_contra h

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

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

Tactic:
rintro ⟨ix, x⟩ ⟨iy, y⟩ e

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 : ↑↑(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⟩
⊢ ⟨ix, x⟩ = ⟨iy, y⟩