awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
x : ↥(∐ f)
y :
  ↥(PreZeroHypercover.X (S := colimit (Discrete.functor f))
      (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
        PreZeroHypercover (colimit (Discrete.functor f)))
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x :
        PreZeroHypercover.I₀ (S := colimit (Discrete.functor f))
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
            PreZeroHypercover (colimit (Discrete.functor f)))))
hy :
  (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)
have right : IsIso (X :=
  X.presheaf.stalk
    ((Sigma.desc α)
      ((PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
          y :
        ↥(colimit (Discrete.functor f)))))
  (Scheme.Hom.stalkMap (Sigma.desc α)
    ((PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y))
Tactic: rw [← hy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
x : ↥(∐ f)
y :
  ↥(PreZeroHypercover.X (S := colimit (Discrete.functor f))
      (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
        PreZeroHypercover (colimit (Discrete.functor f)))
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x :
        PreZeroHypercover.I₀ (S := colimit (Discrete.functor f))
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
            PreZeroHypercover (colimit (Discrete.functor f)))))
hy :
  (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ IsIso (X :=
    X.presheaf.stalk
      ((Sigma.desc α)
        ((PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
              (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
            y :
          ↥(colimit (Discrete.functor f)))))
    (Scheme.Hom.stalkMap (Sigma.desc α)
      ((PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y))
have right : Eq (α := ↥X)
  ((Sigma.desc α)
      ((PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
          y :
        ↥(colimit (Discrete.functor f))) :
    ↥X)
  ((α (Discrete.as (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))) y : ↥X)
Tactic: refine IsIso.of_isIso_fac_right
      (f := ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f _).stalkMap y)
      (h := (X.presheaf.stalkCongr (.of_eq ?_)).hom ≫ (α _).stalkMap _) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
⊢ IsOpenImmersion (X := ∐ g) (Sigma.desc α)
have obtain : ∀ (ι : Type u) (e : σ ≃ ι), IsOpenImmersion (X := ∐ g) (Sigma.desc α)
Tactic: obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small (α := σ)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ IsOpenImmersion (X := ∐ g) (Sigma.desc α)
have h : Eq (α := ∐ g ⟶ X) (Sigma.desc α)
  (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
    (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i)))
Tactic: convert! IsOpenImmersion.comp ((Sigma.reindex e.symm g).inv) (Sigma.desc fun i ↦ α _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
h :
  Eq (α := ∐ g ⟶ X) (Sigma.desc α)
    (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
      (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i)))
⊢ IsOpenImmersion (X := ∐ g) (Sigma.desc α)
have convert! : IsOpenImmersion.{u} (X := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Y := X)
  (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i))
Tactic: convert! IsOpenImmersion.comp ((Sigma.reindex e.symm g).inv) (Sigma.desc fun i ↦ α _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ Eq (α := ∐ g ⟶ X) (Sigma.desc α)
    (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
      (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i)))
have h : ∀ (i : σ),
  CategoryStruct.comp (Y := ∐ g) (Sigma.ι g i) (Sigma.desc α) =
    CategoryStruct.comp (Y := ∐ g) (Sigma.ι g i)
      (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
        (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i)))
Tactic: refine Sigma.hom_ext _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
i : σ
⊢ CategoryStruct.comp (Y := ∐ g) (Sigma.ι g i) (Sigma.desc α) =
    CategoryStruct.comp (Y := ∐ g) (Sigma.ι g i)
      (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
        (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i)))
have h : ∀ (i : ι),
  Eq (α := g ((e.symm : (a : ι) → σ) i) ⟶ X)
    (CategoryStruct.comp (Y := ∐ g) (Sigma.ι g ((e.symm : (a : ι) → σ) i)) (Sigma.desc α))
    (CategoryStruct.comp (Y := ∐ g) (Sigma.ι g ((e.symm : (a : ι) → σ) i))
      (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
        (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i))))
Tactic: obtain ⟨i, rfl⟩ := e.symm.surjective i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ IsOpenImmersion.{u} (X := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Y := X)
    (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i))
have hα₁ : _root_.Pairwise.{u} (α := ι)
  (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦
    Set.range (ι := ↥((g ∘ (⇑e.symm : (a : ι) → σ)) x)) ⇑(α ((e.symm : (a : ι) → σ) x)))
Tactic: apply isOpenImmersion_sigmaDesc_aux
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
inst : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst_1 : ∀ (i : σ), IsOpenImmersion (f i)
hcov : Eq.{u + 1} (α := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) ⊤
hdisj :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := S.Opens) Disjoint fun (x : σ) ↦ Scheme.Hom.opensRange (f x))
⊢ IsOpenImmersion (X := ∐ X) (Sigma.desc f)
have refine : ∀ (i j : σ) (hij : i ≠ j),
  Function.onFun.{v + 1, u + 1, 1} (β := Set ↥S) Disjoint (fun (x : σ) ↦ Set.range (ι := ↥(X x)) ⇑(f x)) i j
Tactic: refine isOpenImmersion_sigmaDesc _ _ (fun i j hij ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
σ : Type v
inst : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst_1 : ∀ (i : σ), IsOpenImmersion (f i)
hcov : Eq.{u + 1} (α := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) ⊤
hdisj :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := S.Opens) Disjoint fun (x : σ) ↦ Scheme.Hom.opensRange (f x))
⊢ Nonempty (IsColimit (Cofan.mk S f))
have this : IsOpenImmersion (X := ∐ X) (Sigma.desc f)
Tactic: have : IsOpenImmersion (Sigma.desc f) := by
    refine isOpenImmersion_sigmaDesc _ _ (fun i j hij ↦ ?_)
    simpa [Function.onFun_apply, disjoint_iff, Opens.ext_iff] using hdisj hij
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
inst : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst_1 : ∀ (i : σ), IsOpenImmersion (f i)
hcov : Eq.{u + 1} (α := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) ⊤
hdisj :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := S.Opens) Disjoint fun (x : σ) ↦ Scheme.Hom.opensRange (f x))
this : IsOpenImmersion (X := ∐ X) (Sigma.desc f)
⊢ Nonempty (IsColimit (Cofan.mk S f))
have simp : IsIso (X := ∐ X) (Sigma.desc f)
Tactic: simp only [Cofan.nonempty_isColimit_iff_isIso_sigmaDesc (Cofan.mk S f), cofan_mk_inj, Cofan.mk_pt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
inst : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst_1 : ∀ (i : σ), IsOpenImmersion (f i)
hcov : Eq.{u + 1} (α := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) ⊤
hdisj :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := S.Opens) Disjoint fun (x : σ) ↦ Scheme.Hom.opensRange (f x))
this : IsOpenImmersion (X := ∐ X) (Sigma.desc f)
⊢ IsIso (X := ∐ X) (Sigma.desc f)
have hf : Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f) = ⊤
Tactic: apply isIso_of_isOpenImmersion_of_opensRange_eq_top
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
inst : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst_1 : ∀ (i : σ), IsOpenImmersion (f i)
hcov : Eq.{u + 1} (α := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) ⊤
hdisj :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := S.Opens) Disjoint fun (x : σ) ↦ Scheme.Hom.opensRange (f x))
this : IsOpenImmersion (X := ∐ X) (Sigma.desc f)
⊢ Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f) = ⊤
have hf : ⊤ ≤ Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f)
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
σ : Type v
inst : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst_1 : ∀ (i : σ), IsOpenImmersion (f i)
hcov : Eq.{u + 1} (α := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) ⊤
hdisj :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := S.Opens) Disjoint fun (x : σ) ↦ Scheme.Hom.opensRange (f x))
this : IsOpenImmersion (X := ∐ X) (Sigma.desc f)
x : ↥S
hx : Membership.mem (γ := Opens ↥S) ⊤ x
⊢ x ∈ Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f)
have this₁ : Membership.mem (γ := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) x
Tactic: have : x ∈ ⨆ i, (f i).opensRange := by rwa [hcov]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
inst : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst_1 : ∀ (i : σ), IsOpenImmersion (f i)
hcov : Eq.{u + 1} (α := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) ⊤
hdisj :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := S.Opens) Disjoint fun (x : σ) ↦ Scheme.Hom.opensRange (f x))
this_1 : IsOpenImmersion (X := ∐ X) (Sigma.desc f)
x : ↥S
hx : Membership.mem (γ := Opens ↥S) ⊤ x
this : Membership.mem (γ := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) x
⊢ x ∈ Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f)
have hf : ∀ (i : σ) (y : ↥(X i)) (hx : Membership.mem (α := ↥S) (γ := Opens ↥S) ⊤ ((f i) y : ↥S))
  (this : Membership.mem (α := ↥S) (γ := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) ((f i) y : ↥S)),
  Membership.mem (α := ↥S) (Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f)) ((f i) y : ↥S)
Tactic: obtain ⟨i, y, rfl⟩ := by simpa only [Opens.iSup_mk, Opens.mem_mk, Set.mem_iUnion] using this
Cleared hypotheses: x, hx, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
inst : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst_1 : ∀ (i : σ), IsOpenImmersion (f i)
hcov : Eq.{u + 1} (α := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) ⊤
hdisj :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := S.Opens) Disjoint fun (x : σ) ↦ Scheme.Hom.opensRange (f x))
this_1 : IsOpenImmersion (X := ∐ X) (Sigma.desc f)
i : σ
y : ↥(X i)
hx : Membership.mem (α := ↥S) (γ := Opens ↥S) ⊤ ((f i) y : ↥S)
this : Membership.mem (α := ↥S) (γ := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) ((f i) y : ↥S)
⊢ Membership.mem (α := ↥S) (Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f)) ((f i) y : ↥S)
have h : Eq (α := ↥S) ((Sigma.desc f) ((Sigma.ι X i) y : ↥(∐ X)) : ↥S) ((f i) y : ↥S)
Tactic: use Sigma.ι X i y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion.{u} (X := X) (Y := X ⨿ Y) coprod.inl
have rw : IsOpenImmersion
  (Sigma.ι (C := Scheme)
      (fun (i : ULift.{u, 0} WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) i.down X Y)
      { down := WalkingPair.left : ULift.{u, 0} WalkingPair } ≫
    (coprodIsoSigma X Y).inv)
Tactic: rw [← ι_left_coprodIsoSigma_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion.{u} (X := Y) (Y := X ⨿ Y) coprod.inr
have rw : IsOpenImmersion
  (Sigma.ι (C := Scheme)
      (fun (i : ULift.{u, 0} WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) i.down X Y)
      { down := WalkingPair.right : ULift.{u, 0} WalkingPair } ≫
    (coprodIsoSigma X Y).inv)
Tactic: rw [← ι_right_coprodIsoSigma_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y : Scheme
⊢ IsCompl.{u} (α := (X ⨿ Y).Opens) (Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inr)
have a : IsCompl.{u} (α := (X ⨿ Y).Opens) (Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inr) ↔
  IsCompl (α := Set ↥(X ⨿ Y)) (Set.range (ι := ↥X) ⇑coprod.inl) (Set.range (ι := ↥Y) ⇑coprod.inr)
Tactic: convert! isCompl_range_inl_inr X Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y : Scheme
⊢ IsCompl.{u} (α := (X ⨿ Y).Opens) (Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inr) ↔
    IsCompl (α := Set ↥(X ⨿ Y)) (Set.range (ι := ↥X) ⇑coprod.inl) (Set.range (ι := ↥Y) ⇑coprod.inr)
have a : (↑(Scheme.Hom.opensRange coprod.inl ⊓ Scheme.Hom.opensRange coprod.inr) : Set ↥(X ⨿ Y)) = (↑⊥ : Set ↥(X ⨿ Y)) ∧
    (↑(Scheme.Hom.opensRange coprod.inl ⊔ Scheme.Hom.opensRange coprod.inr) : Set ↥(X ⨿ Y)) = (↑⊤ : Set ↥(X ⨿ Y)) ↔
  Eq (α := Set ↥(X ⨿ Y)) (Set.range (ι := ↥X) ⇑coprod.inl ⊓ Set.range (ι := ↥Y) ⇑coprod.inr) ⊥ ∧
    Eq (α := Set ↥(X ⨿ Y)) (Set.range (ι := ↥X) ⇑coprod.inl ⊔ Set.range (ι := ↥Y) ⇑coprod.inr) ⊤
Tactic: simp only [isCompl_iff, disjoint_iff, codisjoint_iff, ← TopologicalSpace.Opens.coe_inj]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y : Scheme
x : ↥X
⊢ Eq (α :=
    Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Scheme.forgetToTop.obj (X ⨿ Y))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
            ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat)) :
        Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
            { as := WalkingPair.left : Discrete WalkingPair } ⟶
          Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
            { as := WalkingPair.left : Discrete WalkingPair })
      (CategoryStruct.comp (Y := colimit (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)))
          (Iso.inv
            (colimit.isoColimitCocone
              { cocone := (↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat),
                isColimit := (↑X.toPresheafedSpace : TopCat).binaryCofanIsColimit (↑Y.toPresheafedSpace : TopCat) }))
          (Iso.hom (PreservesColimitPair.iso Scheme.forgetToTop X Y)) :
        Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
            { as := WalkingPair.left : Discrete WalkingPair } ⟶
          Scheme.forgetToTop.obj (X ⨿ Y)))
    (Scheme.forgetToTop.map coprod.inl)
have e_a : Eq (α :=
  Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
      { as := WalkingPair.left : Discrete WalkingPair } ⟶
    Scheme.forgetToTop.obj (X ⨿ Y))
  (CategoryStruct.comp (Y := colimit (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)))
    (colimit.ι (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)) { as := WalkingPair.left })
    (Iso.hom (PreservesColimitPair.iso Scheme.forgetToTop X Y)))
  (Scheme.forgetToTop.map coprod.inl)
Tactic: refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y : Scheme
x : ↥Y
⊢ Eq (α :=
    Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Scheme.forgetToTop.obj (X ⨿ Y))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
            ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat)) :
        Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
            { as := WalkingPair.right : Discrete WalkingPair } ⟶
          Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
            { as := WalkingPair.right : Discrete WalkingPair })
      (CategoryStruct.comp (Y := colimit (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)))
          (Iso.inv
            (colimit.isoColimitCocone
              { cocone := (↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat),
                isColimit := (↑X.toPresheafedSpace : TopCat).binaryCofanIsColimit (↑Y.toPresheafedSpace : TopCat) }))
          (Iso.hom (PreservesColimitPair.iso Scheme.forgetToTop X Y)) :
        Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
            { as := WalkingPair.right : Discrete WalkingPair } ⟶
          Scheme.forgetToTop.obj (X ⨿ Y)))
    (Scheme.forgetToTop.map coprod.inr)
have e_a : Eq (α :=
  Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
      { as := WalkingPair.right : Discrete WalkingPair } ⟶
    Scheme.forgetToTop.obj (X ⨿ Y))
  (CategoryStruct.comp (Y := colimit (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)))
    (colimit.ι (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)) { as := WalkingPair.right })
    (Iso.hom (PreservesColimitPair.iso Scheme.forgetToTop X Y)))
  (Scheme.forgetToTop.map coprod.inr)
Tactic: refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_