awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
                (a : ↥X') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
            (a : ↥X) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αX.base : (a : ↥X') → ↥X) x : ↥X) :
        ↥(X ⨿ Y))
h₂' :
  ∀ (x : ↥Y'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
                (a : ↥Y') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
            (a : ↥Y) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αY.base : (a : ↥Y') → ↥Y) x : ↥Y) :
        ↥(X ⨿ Y))
refine_1 :
  ∀ (x : ↥(X' ⨿ Y')),
    x ∈ (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y')) ↔
      x ∈ (↑(Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl = Scheme.Hom.opensRange coprod.inl

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
                (a : ↥X') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
            (a : ↥X) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αX.base : (a : ↥X') → ↥X) x : ↥X) :
        ↥(X ⨿ Y))
h₂' :
  ∀ (x : ↥Y'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
                (a : ↥Y') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
            (a : ↥Y) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αY.base : (a : ↥Y') → ↥Y) x : ↥Y) :
        ↥(X ⨿ Y))
refine_1 :
  ∀ (x : ↥(X' ⨿ Y')),
    x ∈ (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y')) ↔
      x ∈ (↑(Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr = Scheme.Hom.opensRange coprod.inr

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
                (a : ↥X') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
            (a : ↥X) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αX.base : (a : ↥X') → ↥X) x : ↥X) :
        ↥(X ⨿ Y))
h₂' :
  ∀ (x : ↥Y'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
                (a : ↥Y') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
            (a : ↥Y) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αY.base : (a : ↥Y') → ↥Y) x : ↥Y) :
        ↥(X ⨿ Y))
x : ↥(X' ⨿ Y')
refine_1 :
  ∀ (x : ↥X'),
    Membership.mem (α := ↥(X' ⨿ Y')) (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
        ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inl x) : ↥(X' ⨿ Y')) ↔
      Membership.mem (α := ↥(X' ⨿ Y')) (↑(Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
        ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inl x) : ↥(X' ⨿ Y'))
refine_1₁ :
  ∀ (x : ↥Y'),
    Membership.mem (α := ↥(X' ⨿ Y')) (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
        ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inr x) : ↥(X' ⨿ Y')) ↔
      Membership.mem (α := ↥(X' ⨿ Y')) (↑(Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
        ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inr x) : ↥(X' ⨿ Y'))
⊢ x ∈ (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y')) ↔
    x ∈ (↑(Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))

Tactic:
obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x

Premises used: AlgebraicGeometry.coprodMk, Homeomorph.surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
                (a : ↥X') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
            (a : ↥X) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αX.base : (a : ↥X') → ↥X) x : ↥X) :
        ↥(X ⨿ Y))
h₂' :
  ∀ (x : ↥Y'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
                (a : ↥Y') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
            (a : ↥Y) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αY.base : (a : ↥Y') → ↥Y) x : ↥Y) :
        ↥(X ⨿ Y))
x : ↥(X' ⨿ Y')
refine_1 :
  ∀ (x : ↥X'),
    Membership.mem (α := ↥(X' ⨿ Y')) (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
        ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inl x) : ↥(X' ⨿ Y')) ↔
      Membership.mem (α := ↥(X' ⨿ Y')) (↑(Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
        ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inl x) : ↥(X' ⨿ Y'))
refine_1₁ :
  ∀ (x : ↥Y'),
    Membership.mem (α := ↥(X' ⨿ Y')) (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
        ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inr x) : ↥(X' ⨿ Y')) ↔
      Membership.mem (α := ↥(X' ⨿ Y')) (↑(Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
        ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inr x) : ↥(X' ⨿ Y'))
⊢ x ∈ (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y')) ↔
    x ∈ (↑(Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))

Tactic:
obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x

Premises used: AlgebraicGeometry.coprodMk, Homeomorph.surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
                (a : ↥X') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
            (a : ↥X) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αX.base : (a : ↥X') → ↥X) x : ↥X) :
        ↥(X ⨿ Y))
h₂' :
  ∀ (x : ↥Y'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
                (a : ↥Y') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
            (a : ↥Y) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αY.base : (a : ↥Y') → ↥Y) x : ↥Y) :
        ↥(X ⨿ Y))
x : ↥X'
⊢ Membership.mem (α := ↥(X' ⨿ Y')) (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
      ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inl x) : ↥(X' ⨿ Y')) ↔
    Membership.mem (α := ↥(X' ⨿ Y')) (↑(Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
      ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inl x) : ↥(X' ⨿ Y'))

Tactic:
simp_all
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
                (a : ↥X') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
            (a : ↥X) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αX.base : (a : ↥X') → ↥X) x : ↥X) :
        ↥(X ⨿ Y))
h₂' :
  ∀ (x : ↥Y'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
                (a : ↥Y') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
            (a : ↥Y) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αY.base : (a : ↥Y') → ↥Y) x : ↥Y) :
        ↥(X ⨿ Y))
x : ↥Y'
⊢ Membership.mem (α := ↥(X' ⨿ Y')) (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
      ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inr x) : ↥(X' ⨿ Y')) ↔
    Membership.mem (α := ↥(X' ⨿ Y')) (↑(Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
      ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inr x) : ↥(X' ⨿ Y'))

Tactic:
simp_all
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
                (a : ↥X') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
            (a : ↥X) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αX.base : (a : ↥X') → ↥X) x : ↥X) :
        ↥(X ⨿ Y))
h₂' :
  ∀ (x : ↥Y'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
                (a : ↥Y') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
            (a : ↥Y) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αY.base : (a : ↥Y') → ↥Y) x : ↥Y) :
        ↥(X ⨿ Y))
x : ↥X'
⊢ Membership.mem (α := ↥(X' ⨿ Y')) (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
      ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inl x) : ↥(X' ⨿ Y')) ↔
    Membership.mem (α := ↥(X' ⨿ Y')) (↑(Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
      ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inl x) : ↥(X' ⨿ Y'))

Tactic:
simp_all
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
                (a : ↥X') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
            (a : ↥X) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αX.base : (a : ↥X') → ↥X) x : ↥X) :
        ↥(X ⨿ Y))
h₂' :
  ∀ (x : ↥Y'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
                (a : ↥Y') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
            (a : ↥Y) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αY.base : (a : ↥Y') → ↥Y) x : ↥Y) :
        ↥(X ⨿ Y))
x : ↥Y'
⊢ Membership.mem (α := ↥(X' ⨿ Y')) (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
      ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inr x) : ↥(X' ⨿ Y')) ↔
    Membership.mem (α := ↥(X' ⨿ Y')) (↑(Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
      ((coprodMk X' Y' : (a : ↥X' ⊕ ↥Y') → ↥(X' ⨿ Y')) (Sum.inr x) : ↥(X' ⨿ Y'))

Tactic:
simp_all
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
refine_2 :
  {Z : Scheme.{u_1}} →
    (f : Z ⟶ X ⨿ Y) →
      IsColimit (F := pair (pullback f coprod.inl) (pullback f coprod.inr))
        (BinaryCofan.mk (pullback.fst f coprod.inl) (pullback.fst f coprod.inr))
⊢ {Z : Scheme.{u_1}} →
    (f : Z ⟶ Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) →
      IsColimit
        (BinaryCofan.mk
          (PullbackCone.mk (W := pullback f (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
              (pullback.fst f (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
              (pullback.snd f (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))) ⋯).fst
          (PullbackCone.mk (W := pullback f (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
              (pullback.fst f (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
              (pullback.snd f (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))) ⋯).fst)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
refine_2 :
  ∀ {Z : Scheme.{u_1}} (f : Z ⟶ X ⨿ Y),
    IsCompl (Scheme.Hom.opensRange (X := pullback f coprod.inl) (pullback.fst f coprod.inl))
      (Scheme.Hom.opensRange (X := pullback f coprod.inr) (pullback.fst f coprod.inr))
⊢ {Z : Scheme.{u_1}} →
    (f : Z ⟶ X ⨿ Y) →
      IsColimit (F := pair (pullback f coprod.inl) (pullback f coprod.inr))
        (BinaryCofan.mk (pullback.fst f coprod.inl) (pullback.fst f coprod.inr))

Tactic:
refine fun {Z} f ↦ (nonempty_isColimit_binaryCofanMk_of_isCompl _ _ ?_).some

Premises used: Nonempty.some, AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isCompl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
Z : Scheme
f : Z ⟶ X ⨿ Y
refine_2 : IsCompl (f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr)
⊢ IsCompl (Scheme.Hom.opensRange (X := pullback f coprod.inl) (pullback.fst f coprod.inl))
    (Scheme.Hom.opensRange (X := pullback f coprod.inr) (pullback.fst f coprod.inr))

Tactic:
rw [Scheme.Hom.opensRange_pullbackFst, Scheme.Hom.opensRange_pullbackFst]

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
Z : Scheme
f : Z ⟶ X ⨿ Y
⊢ IsCompl (α := Set ↥Z)
    ((CompleteLatticeHom.setPreimage ⇑f : (a : Set ↥(X ⨿ Y)) → Set ↥Z) (Set.range (ι := ↥X) ⇑coprod.inl) : Set ↥Z)
    ((CompleteLatticeHom.setPreimage ⇑f : (a : Set ↥(X ⨿ Y)) → Set ↥Z) (Set.range (ι := ↥Y) ⇑coprod.inr) : Set ↥Z)

Tactic:
(isCompl_range_inl_inr X Y).map (CompleteLatticeHom.setPreimage f)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.isCompl_range_inl_inr, CompleteLatticeHom.setPreimage, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', IsCompl.map, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
Z : Scheme
f : Z ⟶ X ⨿ Y
a :
  IsCompl (f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) ↔
    IsCompl (α := Set ↥Z)
      ((CompleteLatticeHom.setPreimage ⇑f : (a : Set ↥(X ⨿ Y)) → Set ↥Z) (Set.range (ι := ↥X) ⇑coprod.inl) : Set ↥Z)
      ((CompleteLatticeHom.setPreimage ⇑f : (a : Set ↥(X ⨿ Y)) → Set ↥Z) (Set.range (ι := ↥Y) ⇑coprod.inr) : Set ↥Z)
⊢ IsCompl (f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr)

Tactic:
convert! (isCompl_range_inl_inr X Y).map (CompleteLatticeHom.setPreimage f)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.isCompl_range_inl_inr, CompleteLatticeHom.setPreimage, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', IsCompl.map, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
Z : Scheme
f : Z ⟶ X ⨿ Y
⊢ IsCompl (f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) ↔
    IsCompl (α := Set ↥Z)
      ((CompleteLatticeHom.setPreimage ⇑f : (a : Set ↥(X ⨿ Y)) → Set ↥Z) (Set.range (ι := ↥X) ⇑coprod.inl) : Set ↥Z)
      ((CompleteLatticeHom.setPreimage ⇑f : (a : Set ↥(X ⨿ Y)) → Set ↥Z) (Set.range (ι := ↥Y) ⇑coprod.inr) : Set ↥Z)

Tactic:
simp [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:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
simp_rw : Hom.opensRange ι₁ ⊓ U ⊔ Hom.opensRange ι₂ ⊓ U = U
⊢ ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊔ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = U

Tactic:
simp_rw [Scheme.Hom.image_preimage_eq_opensRange_inf]

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
rw : (Hom.opensRange ι₁ ⊔ Hom.opensRange ι₂) ⊓ U = U
rw₁ : ⊤ ⊓ U = U
rw₂ rw₃ : U = U
⊢ Hom.opensRange ι₁ ⊓ U ⊔ Hom.opensRange ι₂ ⊓ U = U

Tactic:
rw [← inf_sup_right, (isCompl_opensRange_inl_inr X Y).sup_eq_top, top_inf_eq]

Premises used: IsCompl.sup_eq_top, top_inf_eq, inf_sup_right, AlgebraicGeometry.isCompl_opensRange_inl_inr
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
h₁ : ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊔ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = U
simp_rw : Hom.opensRange ι₁ ⊓ U ⊓ (Hom.opensRange ι₂ ⊓ U) = ⊥
⊢ ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊓ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = ⊥

Tactic:
simp_rw [Scheme.Hom.image_preimage_eq_opensRange_inf]

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
h₁ : ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊔ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = U
rw : Hom.opensRange ι₁ ⊓ Hom.opensRange ι₂ ⊓ U = ⊥
rw₁ : ⊥ ⊓ U = ⊥
rw₂ rw₃ : Eq.{u + 1} (α := (X ⨿ Y).Opens) ⊥ ⊥
⊢ Hom.opensRange ι₁ ⊓ U ⊓ (Hom.opensRange ι₂ ⊓ U) = ⊥

Tactic:
rw [← inf_inf_distrib_right, (isCompl_opensRange_inl_inr X Y).inf_eq_bot, bot_inf_eq]

Premises used: IsCompl.inf_eq_bot, AlgebraicGeometry.isCompl_opensRange_inl_inr, inf_inf_distrib_right, bot_inf_eq