awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Limits
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)

Tactic:
isOpenImmersion_sigmaDesc _ _ (fun i j hij ↦ ?_)

Premises used: AlgebraicGeometry.isOpenImmersion_sigmaDesc
-- Module: Mathlib.AlgebraicGeometry.Limits
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))
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
⊢ IsOpenImmersion (X := ∐ X) (Sigma.desc f)

Tactic:
refine isOpenImmersion_sigmaDesc _ _ (fun i j hij ↦ ?_)

Premises used: AlgebraicGeometry.isOpenImmersion_sigmaDesc
-- Module: Mathlib.AlgebraicGeometry.Limits
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))
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:
simpa [Function.onFun_apply, disjoint_iff, Opens.ext_iff] using hdisj hij

Premises used: disjoint_iff, Function.onFun_apply, TopologicalSpace.Opens.ext_iff
-- Module: Mathlib.AlgebraicGeometry.Limits
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)

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
-- Module: Mathlib.AlgebraicGeometry.Limits
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)
simp : IsIso (X := ∐ X) (Sigma.desc f)
⊢ Nonempty (IsColimit (Cofan.mk S f))

Tactic:
simp only [Cofan.nonempty_isColimit_iff_isIso_sigmaDesc (Cofan.mk S f), cofan_mk_inj, Cofan.mk_pt]

Premises used: CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.cofan_mk_inj, CategoryTheory.Limits.Cofan.mk, CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc
-- Module: Mathlib.AlgebraicGeometry.Limits
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)
hf : Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f) = ⊤
⊢ IsIso (X := ∐ X) (Sigma.desc f)

Tactic:
apply isIso_of_isOpenImmersion_of_opensRange_eq_top

Premises used: AlgebraicGeometry.isIso_of_isOpenImmersion_of_opensRange_eq_top
-- Module: Mathlib.AlgebraicGeometry.Limits
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)
hf : ⊤ ≤ Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f)
⊢ Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f) = ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.AlgebraicGeometry.Limits
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
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := S.Opens) ⊤ x
⊢ Membership.mem (γ := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) x

Tactic:
rwa [hcov]
-- Module: Mathlib.AlgebraicGeometry.Limits
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
⊢ Membership.mem (γ := S.Opens) (⨆ (i : σ), Scheme.Hom.opensRange (f i)) x

Tactic:
have : x ∈ ⨆ i, (f i).opensRange := by rwa [hcov]
-- Module: Mathlib.AlgebraicGeometry.Limits
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
⊢ ∃ (i : σ), x ∈ (Scheme.Hom.opensRange (f i)).carrier

Tactic:
simpa only [Opens.iSup_mk, Opens.mem_mk, Set.mem_iUnion] using this

Premises used: TopologicalSpace.Opens.iSup_mk, Set.mem_iUnion, TopologicalSpace.Opens.mem_mk
-- Module: Mathlib.AlgebraicGeometry.Limits
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
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)
⊢ x ∈ Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f)

Tactic:
obtain ⟨i, y, rfl⟩ := by simpa only [Opens.iSup_mk, Opens.mem_mk, Set.mem_iUnion] using this

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
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)
h : Eq (α := ↥S) ((Sigma.desc f) ((Sigma.ι X i) y : ↥(∐ X)) : ↥S) ((f i) y : ↥S)
⊢ Membership.mem (α := ↥S) (Scheme.Hom.opensRange (X := ∐ X) (Sigma.desc f)) ((f i) y : ↥S)

Tactic:
use Sigma.ι X i y

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Sigma.ι, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Limits
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)
⊢ Eq (α := ↥S) ((Sigma.desc f) ((Sigma.ι X i) y : ↥(∐ X)) : ↥S) ((f i) y : ↥S)

Tactic:
simp [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : WalkingPair
⊢ Iso (C := Scheme)
    (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme)
        (ULift.down.{u, 0} ((Equiv.symm Equiv.ulift : (a : WalkingPair) → ULift.{u, 0} WalkingPair) x)) X Y :
      Scheme.{u})
    (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y : Scheme.{u})

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
⊢ 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 =
    coprod.inl

Tactic:
Sigma.ι_comp_map' _ _ _

Premises used: CategoryTheory.NatTrans.vcomp, Set.Mem, ContinuousMap.comp, CategoryTheory.Limits.colimit, CategoryTheory.Limits.pair, AlgebraicGeometry.PresheafedSpace.comp, AlgebraicGeometry.LocallyRingedSpace.comp, CategoryTheory.Limits.Sigma.ι_comp_map', CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
⊢ 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 =
    coprod.inr

Tactic:
Sigma.ι_comp_map' _ _ _

Premises used: CategoryTheory.NatTrans.vcomp, Set.Mem, ContinuousMap.comp, CategoryTheory.Limits.colimit, CategoryTheory.Limits.pair, AlgebraicGeometry.PresheafedSpace.comp, AlgebraicGeometry.LocallyRingedSpace.comp, CategoryTheory.Limits.Sigma.ι_comp_map', CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
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)
⊢ IsOpenImmersion.{u} (X := X) (Y := X ⨿ Y) coprod.inl

Tactic:
rw [← ι_left_coprodIsoSigma_inv]

Premises used: AlgebraicGeometry.ι_left_coprodIsoSigma_inv
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ 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:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
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)
⊢ IsOpenImmersion.{u} (X := Y) (Y := X ⨿ Y) coprod.inr

Tactic:
rw [← ι_right_coprodIsoSigma_inv]

Premises used: AlgebraicGeometry.ι_right_coprodIsoSigma_inv
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ 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:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
⊢ IsCompl (α := Set ↥(X ⨿ Y)) (Set.range (ι := ↥X) ⇑coprod.inl) (Set.range (ι := ↥Y) ⇑coprod.inr)

Tactic:
((TopCat.binaryCofan_isColimit_iff _).mp
    ⟨mapIsColimitOfPreservesOfIsColimit Scheme.forgetToTop.{u} _ _ (coprodIsCoprod X Y)⟩).2.2

Premises used: TopCat.binaryCofan_isColimit_iff, CategoryTheory.Limits.coprodIsCoprod, AlgebraicGeometry.Scheme.forgetToTop, CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit, Nonempty.intro, And.right, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
⊢ IsCompl (α := Set ↥(X ⨿ Y)) (Set.range (ι := ↥X) ⇑coprod.inl) (Set.range (ι := ↥Y) ⇑coprod.inr)

Tactic:
isCompl_range_inl_inr X Y

Premises used: AlgebraicGeometry.isCompl_range_inl_inr
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
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)
⊢ IsCompl.{u} (α := (X ⨿ Y).Opens) (Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inr)

Tactic:
convert! isCompl_range_inl_inr X Y

Premises used: AlgebraicGeometry.isCompl_range_inl_inr
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
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) ⊤
⊢ 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:
simp only [isCompl_iff, disjoint_iff, codisjoint_iff, ← TopologicalSpace.Opens.coe_inj]

Premises used: codisjoint_iff, disjoint_iff, isCompl_iff, TopologicalSpace.Opens.coe_inj
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
⊢ (↑(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:
rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
x : ↥X
y : ↥Y
⊢ Ne (α := ↥(X ⨿ Y)) (coprod.inl x : ↥(X ⨿ Y)) (coprod.inr y : ↥(X ⨿ Y))

Tactic:
Set.disjoint_iff_forall_ne.mp (isCompl_range_inl_inr X Y).disjoint ⟨x, rfl⟩ ⟨y, rfl⟩

Premises used: AlgebraicGeometry.isCompl_range_inl_inr, Set.disjoint_iff_forall_ne, Exists.intro, Iff.mp, IsCompl.disjoint, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
x : ↥X
y : ↥Y
⊢ Ne (α := ↥(X ⨿ Y)) (coprod.inr y : ↥(X ⨿ Y)) (coprod.inl x : ↥(X ⨿ Y))

Tactic:
(inl_ne_inr _ _ _ _).symm

Premises used: AlgebraicGeometry.inl_ne_inr, Ne.symm
-- Module: Mathlib.AlgebraicGeometry.Limits
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)

Tactic:
(colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv_assoc, CategoryTheory.Limits.ColimitCocone.mk, Eq.trans, TopCat.binaryCofanIsColimit
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
x : ↥X
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)
⊢ 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)

Tactic:
refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv_assoc, CategoryTheory.Limits.ColimitCocone.mk, Eq.trans, TopCat.binaryCofanIsColimit
-- Module: Mathlib.AlgebraicGeometry.Limits
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 := 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:
coprodComparison_inl Scheme.forgetToTop

Premises used: CategoryTheory.Limits.coprodComparison_inl, AlgebraicGeometry.Scheme.forgetToTop
-- Module: Mathlib.AlgebraicGeometry.Limits
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 := 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:
exact coprodComparison_inl Scheme.forgetToTop

Premises used: CategoryTheory.Limits.coprodComparison_inl, AlgebraicGeometry.Scheme.forgetToTop