-- Mathlib/AlgebraicGeometry/Limits.lean
/-- The images of each component in the coproduct is disjoint. -/
lemma disjoint_opensRange_sigmaι (i j : ι) (h : i ≠ j) :
    Disjoint (Sigma.ι f i).opensRange (Sigma.ι f j).opensRange

Proof state:
case intro.intro
ι : Type u
f : ι → Scheme
i j : ι
h : i ≠ j
U : (∐ f).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι f j)
x : ↑↑(f i).toPresheafedSpace
hx : (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑U
y : ↑↑(f j).toPresheafedSpace
hy : (ConcreteCategory.hom (Sigma.ι f j).base) y = (ConcreteCategory.hom (Sigma.ι f i).base) x
⊢ (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑⊥

Tactic:
obtain ⟨rfl⟩ := (sigmaι_eq_iff _ _ _ _ _).mp hy

Result:
case intro.intro.refl
ι : Type u
f : ι → Scheme
i : ι
U : (∐ f).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)
x : ↑↑(f i).toPresheafedSpace
hx : (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑U
h : i ≠ i
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)
hy : (ConcreteCategory.hom (Sigma.ι f i).base) x = (ConcreteCategory.hom (Sigma.ι f i).base) x
⊢ (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑⊥

Proof state:
case intro.intro.refl
ι : Type u
f : ι → Scheme
i : ι
U : (∐ f).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)
x : ↑↑(f i).toPresheafedSpace
hx : (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑U
h : i ≠ i
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)
hy : (ConcreteCategory.hom (Sigma.ι f i).base) x = (ConcreteCategory.hom (Sigma.ι f i).base) x
⊢ (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑⊥

Tactic:
cases h rfl

Result:
no goals

Proof state:
ι : Type u
f : ι → Scheme
i j : ι
h : i ≠ j
⊢ Disjoint (Scheme.Hom.opensRange (Sigma.ι f i)) (Scheme.Hom.opensRange (Sigma.ι f j))

Tactic:
intro U hU hU' x hx

Result:
ι : Type u
f : ι → Scheme
i j : ι
h : i ≠ j
U : (∐ f).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι f j)
x : ↑↑(∐ f).toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑⊥

Proof state:
ι : Type u
f : ι → Scheme
i j : ι
h : i ≠ j
U : (∐ f).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι f j)
x : ↑↑(∐ f).toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑⊥

Tactic:
obtain ⟨x, rfl⟩ := hU hx

Result:
case intro
ι : Type u
f : ι → Scheme
i j : ι
h : i ≠ j
U : (∐ f).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι f j)
x : ↑↑(f i).toPresheafedSpace
hx : (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑U
⊢ (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑⊥

Proof state:
case intro
ι : Type u
f : ι → Scheme
i j : ι
h : i ≠ j
U : (∐ f).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι f j)
x : ↑↑(f i).toPresheafedSpace
hx : (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑U
⊢ (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑⊥

Tactic:
obtain ⟨y, hy⟩ := hU' hx

Result:
case intro.intro
ι : Type u
f : ι → Scheme
i j : ι
h : i ≠ j
U : (∐ f).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι f j)
x : ↑↑(f i).toPresheafedSpace
hx : (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑U
y : ↑↑(f j).toPresheafedSpace
hy : (ConcreteCategory.hom (Sigma.ι f j).base) y = (ConcreteCategory.hom (Sigma.ι f i).base) x
⊢ (ConcreteCategory.hom (Sigma.ι f i).base) x ∈ ↑⊥