awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X ⊕ ↥Y
⊢ Membership.mem (α := ↥(X ⨿ Y)) (γ := Set ↥(X ⨿ Y))
    (Set.range (ι :=
      ↥(PreZeroHypercover.X.{w, u, u + 1} (S := X ⨿ Y)
          { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1},
            X := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x,
            f := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
                Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
                (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr) x :
            PreZeroHypercover.{w, u, u + 1} (X ⨿ Y) }
          (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
            (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y)
              ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))))))
      ⇑(PreZeroHypercover.f
          { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1},
            X := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x,
            f := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
                Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
                (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr) x }
          (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
            (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y)
              ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))))))
    ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))
have h : ∃ (y :
  ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
      (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
        (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y) ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y)))))),
  Eq (α := ↥(X ⨿ Y))
    ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
          Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
          (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
          (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
            (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y)
              ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y)))))
        y :
      ↥(X ⨿ Y))
    ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))
Tactic: simp only [Sum.elim_inl, Sum.elim_inr, Set.mem_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X ⊕ ↥Y
⊢ ∃ (y :
    ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
        (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
          (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y)
            ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y)))))),
    Eq (α := ↥(X ⨿ Y))
      ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
            (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
              (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y)
                ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y)))))
          y :
        ↥(X ⨿ Y))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))
have h : ∃ (y :
  ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
      (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) x))),
  Eq (α := ↥(X ⨿ Y))
    ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
          Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
          (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
          (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) x))
        y :
      ↥(X ⨿ Y))
    ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))
Tactic: rw [Homeomorph.symm_apply_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X ⊕ ↥Y
⊢ ∃ (y :
    ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
        (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) x))),
    Eq (α := ↥(X ⨿ Y))
      ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
            (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) x))
          y :
        ↥(X ⨿ Y))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))
have h : ∀ (x : ↥X),
  ∃ (y :
    ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
        (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inl x)))),
    Eq (α := ↥(X ⨿ Y))
      ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
            (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inl x)))
          y :
        ↥(X ⨿ Y))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y))
Tactic: obtain (x | x) := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X ⊕ ↥Y
h :
  ∀ (x : ↥X),
    ∃ (y :
      ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
          (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inl x)))),
      Eq (α := ↥(X ⨿ Y))
        ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
              (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
              (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inl x)))
            y :
          ↥(X ⨿ Y))
        ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y))
⊢ ∃ (y :
    ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
        (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) x))),
    Eq (α := ↥(X ⨿ Y))
      ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
            (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) x))
          y :
        ↥(X ⨿ Y))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))
have h₁ : ∀ (x : ↥Y),
  ∃ (y :
    ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
        (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inr x)))),
    Eq (α := ↥(X ⨿ Y))
      ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
            (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inr x)))
          y :
        ↥(X ⨿ Y))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y))
Tactic: obtain (x | x) := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan (C := Scheme) fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y :=
  Cofan.mk S fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
⊢ Nonempty (IsColimit (BinaryCofan.mk f g))
have refine : Nonempty.{u + 2} (IsColimit c')
Tactic: refine ⟨IsColimit.ofIsoColimit (Nonempty.some ?_) i.symm⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan (C := Scheme) fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y :=
  Cofan.mk S fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y ⟶ S :=
  fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
⊢ Nonempty.{u + 2} (IsColimit c')
have convert_1 : ∀ (i : WalkingPair), IsOpenImmersion (fi i)
Tactic: convert! nonempty_isColimit_cofanMk_of fi _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan (C := Scheme) fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y :=
  Cofan.mk S fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y ⟶ S :=
  fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
convert_1 : ∀ (i : WalkingPair), IsOpenImmersion (fi i)
⊢ Nonempty.{u + 2} (IsColimit c')
have convert_2 : Eq.{u + 1} (α := S.Opens) (⨆ (i : WalkingPair), Scheme.Hom.opensRange (fi i)) ⊤
Tactic: convert! nonempty_isColimit_cofanMk_of fi _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan (C := Scheme) fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y :=
  Cofan.mk S fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y ⟶ S :=
  fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
convert_1 : ∀ (i : WalkingPair), IsOpenImmersion (fi i)
convert_2 : Eq.{u + 1} (α := S.Opens) (⨆ (i : WalkingPair), Scheme.Hom.opensRange (fi i)) ⊤
⊢ Nonempty.{u + 2} (IsColimit c')
have convert_3 : _root_.Pairwise (α := WalkingPair)
  (Function.onFun.{1, u + 1, 1} (β := S.Opens) Disjoint fun (x : WalkingPair) ↦ Scheme.Hom.opensRange (fi x))
Tactic: convert! nonempty_isColimit_cofanMk_of fi _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ IsPullback (Y := X ⨿ Y) (Z := X' ⨿ Y') f coprod.inl coprod.inl (coprod.map f g)
have refine : Eq (α := (X ⨿ Y).Opens) (coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inl)
Tactic: refine IsOpenImmersion.isPullback _ _ _ _ (by simp) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ Eq (α := (X ⨿ Y).Opens) (coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inl)
have a : LE.le (α := (X ⨿ Y).Opens) (coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inl)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
a : LE.le (α := (X ⨿ Y).Opens) (coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inl)
⊢ Eq (α := (X ⨿ Y).Opens) (coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inl)
have a₁ : LE.le (α := (X ⨿ Y).Opens) (Scheme.Hom.opensRange coprod.inl) (coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
x : ↥(X ⨿ Y)
y : ↥X'
hxy : Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y')) ((coprod.map f g) x : ↥(X' ⨿ Y'))
⊢ Membership.mem (γ := Opens ↥(X ⨿ Y)) (Scheme.Hom.opensRange coprod.inl) x
have a : ∀ (x : ↥X)
  (hxy :
    Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y'))
      ((coprod.map f g) ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y)) : ↥(X' ⨿ Y'))),
  Membership.mem (α := ↥(X ⨿ Y)) (γ := Opens ↥(X ⨿ Y)) (Scheme.Hom.opensRange coprod.inl)
    ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y))
Tactic: obtain ⟨(x | x), rfl⟩ := (coprodMk _ _).surjective x
Cleared hypotheses: x, hxy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
x : ↥(X ⨿ Y)
y : ↥X'
hxy : Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y')) ((coprod.map f g) x : ↥(X' ⨿ Y'))
a :
  ∀ (x : ↥X)
    (hxy :
      Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y'))
        ((coprod.map f g) ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y)) : ↥(X' ⨿ Y'))),
    Membership.mem (α := ↥(X ⨿ Y)) (γ := Opens ↥(X ⨿ Y)) (Scheme.Hom.opensRange coprod.inl)
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y))
⊢ Membership.mem (γ := Opens ↥(X ⨿ Y)) (Scheme.Hom.opensRange coprod.inl) x
have a₁ : ∀ (x : ↥Y)
  (hxy :
    Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y'))
      ((coprod.map f g) ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y)) : ↥(X' ⨿ Y'))),
  Membership.mem (α := ↥(X ⨿ Y)) (γ := Opens ↥(X ⨿ Y)) (Scheme.Hom.opensRange coprod.inl)
    ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y))
Tactic: obtain ⟨(x | x), rfl⟩ := (coprodMk _ _).surjective x
Cleared hypotheses: x, hxy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥Y
hxy :
  Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y'))
    ((coprod.map f g) ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y)) : ↥(X' ⨿ Y'))
⊢ Membership.mem (α := ↥(X ⨿ Y)) (γ := Opens ↥(X ⨿ Y)) (Scheme.Hom.opensRange coprod.inl)
    ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y))
have hxy₁ : Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y')) ((g ≫ coprod.inr) x : ↥(X' ⨿ Y'))
Tactic: simp only [coprodMk_inr, ← Scheme.Hom.comp_apply, coprod.inr_map] at hxy
Cleared hypotheses: hxy
-- 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
⊢ IsVanKampenColimit c
have suffices : IsVanKampenColimit.{0, 0, u_1, u_1 + 1} (C := Scheme) (F := pair X Y)
  (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)
Tactic: suffices IsVanKampenColimit (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) from
      this.of_iso (hc.uniqueUpToIso (coprodIsCoprod _ _)).symm
-- 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
⊢ IsVanKampenColimit.{0, 0, u_1, u_1 + 1} (C := Scheme) (F := pair X Y)
    (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)
have refine_1 : ∀ {X' Y' : Scheme.{u_1}} (α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))),
  αX ≫ BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
      BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f →
    αY ≫ BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
        BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f →
      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))
Tactic: refine BinaryCofan.isVanKampen_mk _ _ (fun _ _ ↦ coprodIsCoprod _ _) _
      (fun _ _ ↦ pullbackIsPullback _ _) ?_ ?_
-- 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
refine_1 :
  ∀ {X' Y' : Scheme.{u_1}} (α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))),
    αX ≫ BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
        BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f →
      αY ≫ BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
          BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f →
        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))
⊢ IsVanKampenColimit.{0, 0, u_1, u_1 + 1} (C := Scheme) (F := pair X Y)
    (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)
have refine_2 : {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))) sorry).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))) sorry).fst)
Tactic: refine BinaryCofan.isVanKampen_mk _ _ (fun _ _ ↦ coprodIsCoprod _ _) _
      (fun _ _ ↦ pullbackIsPullback _ _) ?_ ?_
-- 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
⊢ 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 : ↥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 }))
Tactic: have h₁' (x : _) := congr($h₁ x).symm