Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
⊢ IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
    IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr

Tactic:
refine ⟨(IsOpenImmersion.isPullback _ _ _ _ h₁.symm ?_).flip,
        (IsOpenImmersion.isPullback _ _ _ _ h₂.symm ?_).flip⟩ <;>
        ext x <;> obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x

Goal state after:
case refine_1.refine_1.inl
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥X'
⊢ (coprodMk X' Y') (Sum.inl x) ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) ↔
    (coprodMk X' Y') (Sum.inl x) ∈ ↑(Scheme.Hom.opensRange coprod.inl)

case refine_1.refine_1.inr
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥Y'
⊢ (coprodMk X' Y') (Sum.inr x) ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) ↔
    (coprodMk X' Y') (Sum.inr x) ∈ ↑(Scheme.Hom.opensRange coprod.inl)

case refine_1.refine_2.inl
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥X'
⊢ (coprodMk X' Y') (Sum.inl x) ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) ↔
    (coprodMk X' Y') (Sum.inl x) ∈ ↑(Scheme.Hom.opensRange coprod.inr)

case refine_1.refine_2.inr
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥Y'
⊢ (coprodMk X' Y') (Sum.inr x) ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) ↔
    (coprodMk X' Y') (Sum.inr x) ∈ ↑(Scheme.Hom.opensRange coprod.inr)