awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
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 ≫ BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
    BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f
h₂ :
  αY ≫ BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
    BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α :=
      ↥(Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
          { as := WalkingPair.left : Discrete WalkingPair }))
      ((BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f) x :
        ↥(Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
      ((αX ≫ BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) x :
        ↥(Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
            { as := WalkingPair.left : Discrete WalkingPair }))
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αX f
      (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) ∧
    IsPullback (BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αY f
      (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
have h₂' : ∀ (x : ↥Y'),
  Eq (α :=
    ↥(Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
        { as := WalkingPair.right : Discrete WalkingPair }))
    ((BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f) x :
      ↥(Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
    ((αY ≫ BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) x :
      ↥(Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
          { as := WalkingPair.right : Discrete WalkingPair }))
Tactic: have h₂' (x : _) := congr($h₂ x).symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αX f
      (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) ∧
    IsPullback (BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αY f
      (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
have refine_1 : f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl = Scheme.Hom.opensRange coprod.inl
Tactic: refine ⟨(IsOpenImmersion.isPullback _ _ _ _ h₁.symm ?_).flip,
        (IsOpenImmersion.isPullback _ _ _ _ h₂.symm ?_).flip⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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 : f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl = Scheme.Hom.opensRange coprod.inl
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αX f
      (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) ∧
    IsPullback (BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αY f
      (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
have refine_1₁ : f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr = Scheme.Hom.opensRange coprod.inr
Tactic: refine ⟨(IsOpenImmersion.isPullback _ _ _ _ h₁.symm ?_).flip,
        (IsOpenImmersion.isPullback _ _ _ _ h₂.symm ?_).flip⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl = Scheme.Hom.opensRange coprod.inl
have refine_1 : ∀ (x : ↥(X' ⨿ Y')),
  x ∈ (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y')) ↔
    x ∈ (↑(Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr = Scheme.Hom.opensRange coprod.inr
have refine_1 : ∀ (x : ↥(X' ⨿ Y')),
  x ∈ (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y')) ↔
    x ∈ (↑(Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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')
⊢ x ∈ (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y')) ↔
    x ∈ (↑(Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
have 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'))
Tactic: obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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'))
⊢ x ∈ (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y')) ↔
    x ∈ (↑(Scheme.Hom.opensRange coprod.inl) : Set ↥(X' ⨿ Y'))
have 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'))
Tactic: obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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')
⊢ x ∈ (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y')) ↔
    x ∈ (↑(Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
have 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'))
Tactic: obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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'))
⊢ x ∈ (↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y')) ↔
    x ∈ (↑(Scheme.Hom.opensRange coprod.inr) : Set ↥(X' ⨿ Y'))
have 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'))
Tactic: obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ {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)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ {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))
have 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))
Tactic: refine fun {Z} f ↦ (nonempty_isColimit_binaryCofanMk_of_isCompl _ _ ?_).some
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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 (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))
have refine_2 : IsCompl (f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr)
Tactic: rw [Scheme.Hom.opensRange_pullbackFst, Scheme.Hom.opensRange_pullbackFst]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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)
have 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)
Tactic: convert! (isCompl_range_inl_inr X Y).map (CompleteLatticeHom.setPreimage f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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
⊢ ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊔ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = U
have simp_rw : Hom.opensRange ι₁ ⊓ U ⊔ Hom.opensRange ι₂ ⊓ U = U
Tactic: simp_rw [Scheme.Hom.image_preimage_eq_opensRange_inf]