awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this_2 : Finite.{u_1 + 1} ↥Z
this : QuasiCompact g
y : ↥Y
z : ↥Z :=
  (Sigma.ι (C := Scheme) (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z))
      (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
        (irreducibleComponent y) ⋯))
    (IsLocalRing.closedPoint
      (↑(pt
            (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
              (irreducibleComponent y) ⋯)) :
        Type u_1))
hz : g z ⤳ y
⊢ Membership.mem (γ := Set ↥Y) (closure (Set.range (ι := ↥Z) ⇑g)) y

Tactic:
exact hz.mem_closed isClosed_closure (subset_closure ⟨_, rfl⟩)
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this_2 : Finite.{u_1 + 1} ↥Z
this : QuasiCompact g
⊢ IsSchemeTheoreticallyDominant g

Tactic:
have H : IsSchemeTheoreticallyDominant g := by
    rw [isSchemeTheoreticallyDominant_iff_isDominant, isDominant_iff, denseRange_iff_closure_range,
      Set.eq_univ_iff_forall]
    intro y
    let z : Z := Sigma.ι (fun Z ↦ Spec (pt Z)) ⟨_, irreducibleComponent_mem_irreducibleComponents y⟩
      (IsLocalRing.closedPoint _)
    have hz : g z ⤳ y := by
      simp only [g, z, Z, ← Scheme.Hom.comp_apply, Sigma.ι_desc, pt,
        Scheme.fromSpecStalk_closedPoint]
      exact (IsIrreducible.isGenericPoint_genericPoint _
        isClosed_irreducibleComponent).specializes mem_irreducibleComponent
    exact hz.mem_closed isClosed_closure (subset_closure ⟨_, rfl⟩)
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this_2 : Finite.{u_1 + 1} ↥Z
this : QuasiCompact g
H : IsSchemeTheoreticallyDominant g
suffices : IsReduced.{u_1} (pullback f g)
⊢ IsReduced X

Tactic:
suffices IsReduced (pullback f g) from IsSchemeTheoreticallyDominant.isReduced (pullback.fst f g)
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this_2 : Finite.{u_1 + 1} ↥Z
this : QuasiCompact g
H : IsSchemeTheoreticallyDominant g
⊢ IsPullback (P :=
    Cocone.pt (J := Discrete (↑(irreducibleComponents ↥Y) : Type u_1)) (F :=
      Discrete.functor fun (i : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
        pullback (Y := (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec.{u_1} (pt Z)) i) f
          (Y.fromSpecStalk (⋯.genericPoint (S := (↑i : Set ↥Y)))))
      (Cofan.mk
        (∐ fun (i : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
          pullback (Y := (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec.{u_1} (pt Z)) i) f
            (Y.fromSpecStalk (⋯.genericPoint (S := (↑i : Set ↥Y)))))
        (Sigma.ι fun (i : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
          pullback (Y := (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec.{u_1} (pt Z)) i) f
            (Y.fromSpecStalk (⋯.genericPoint (S := (↑i : Set ↥Y)))))))
    (Cofan.IsColimit.desc
      (coproductIsCoproduct fun (i : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
        pullback (Y := (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec.{u_1} (pt Z)) i) f
          (Y.fromSpecStalk (⋯.genericPoint (S := (↑i : Set ↥Y)))))
      fun (x : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
      pullback.fst f (Y.fromSpecStalk (⋯.genericPoint (S := (↑x : Set ↥Y)))))
    (Cofan.IsColimit.desc
      (coproductIsCoproduct fun (i : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
        pullback (Y := (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec.{u_1} (pt Z)) i) f
          (Y.fromSpecStalk (⋯.genericPoint (S := (↑i : Set ↥Y)))))
      fun (x : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦
      pullback.snd f (Y.fromSpecStalk (⋯.genericPoint (S := (↑x : Set ↥Y)))) ≫
        Cofan.inj (C := Scheme) (f := fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z))
          (Cofan.mk (∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z))
            (Sigma.ι fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)))
          x)
    f g

Tactic:
have H := IsUniversalColimit.isPullback_of_isColimit_left
    (X := fun Z ↦ Spec (pt Z))
    (FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct _))
    (fun Z ↦ Y.fromSpecStalk _) g f _ _ (fun _ ↦ .of_hasPullback _ _) (coproductIsCoproduct _)
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : IsLocallyNoetherian Y
apply :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    IsReduced.{u_1} ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
⊢ IsReduced X

Tactic:
apply +allowSynthFailures @IsReduced.of_openCover (𝒰 := Y.affineCover.pullback₁ f)

Premises used: AlgebraicGeometry.IsReduced.of_openCover, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ IsReduced.{u_1} (Y.affineCover.X i)

Tactic:
have : IsReduced (Y.affineCover.X i) := isReduced_of_isOpenImmersion (Y.affineCover.f i)
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this_1 : IsReduced.{u_1} (Y.affineCover.X i)
this : IsNoetherian.{u_1} (Y.affineCover.X i) := ⋯
⊢ Finite.{u_1 + 1} (↑(irreducibleComponents ↥(Y.affineCover.X i)) : Type u_1)

Tactic:
TopologicalSpace.NoetherianSpace.finite_irreducibleComponents

Premises used: Set.Finite, TopologicalSpace.NoetherianSpace.finite_irreducibleComponents
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this_1 : IsReduced.{u_1} (Y.affineCover.X i)
this : IsNoetherian.{u_1} (Y.affineCover.X i) := ⋯
⊢ Finite.{u_1 + 1} (↑(irreducibleComponents ↥(Y.affineCover.X i)) : Type u_1)

Tactic:
exact TopologicalSpace.NoetherianSpace.finite_irreducibleComponents

Premises used: TopologicalSpace.NoetherianSpace.finite_irreducibleComponents
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this : IsReduced.{u_1} (Y.affineCover.X i)
⊢ Finite.{u_1 + 1} (↑(irreducibleComponents ↥(Y.affineCover.X i)) : Type u_1)

Tactic:
have : Finite ↑(irreducibleComponents ↥(Y.affineCover.X i)) := by
    let : IsNoetherian (Y.affineCover.X i) := {}
    exact TopologicalSpace.NoetherianSpace.finite_irreducibleComponents
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this_1 : IsReduced.{u_1} (Y.affineCover.X i)
this : Finite.{u_1 + 1} (↑(irreducibleComponents ↥(Y.affineCover.X i)) : Type u_1)
⊢ IsReduced.{u_1} ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)

Tactic:
isReduced_of_flat_of_finite_irreducibleComponents (pullback.snd _ _)

Premises used: AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_finite_irreducibleComponents, CategoryTheory.Limits.pullback.snd
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this_1 : IsReduced.{u_1} (Y.affineCover.X i)
this : Finite.{u_1 + 1} (↑(irreducibleComponents ↥(Y.affineCover.X i)) : Type u_1)
⊢ IsReduced.{u_1} ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)

Tactic:
exact isReduced_of_flat_of_finite_irreducibleComponents (pullback.snd _ _)

Premises used: AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_finite_irreducibleComponents, CategoryTheory.Limits.pullback.snd
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : IsLocallyNoetherian Y
⊢ IsReduced.{u_1} (pullback f g)

Tactic:
GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian (pullback.snd _ _)

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyReduced g
inst_1 : Flat g
inst_2 : IsReduced X
inst_3 : IsLocallyNoetherian X
⊢ IsReduced.{u_1} (pullback f g)

Tactic:
GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian (pullback.fst _ _)

Premises used: AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i j : D.J
⊢ LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.f i j)

Tactic:
apply GlueData.f_open

Premises used: AlgebraicGeometry.Scheme.GlueData.f_open
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i j : D.J
⊢ SheafedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.f i j)

Tactic:
apply GlueData.f_open

Premises used: AlgebraicGeometry.Scheme.GlueData.f_open
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i j : D.J
⊢ PresheafedSpace.IsOpenImmersion
    (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.f i j)

Tactic:
apply GlueData.f_open

Premises used: AlgebraicGeometry.Scheme.GlueData.f_open
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.J
⊢ LocallyRingedSpace.IsOpenImmersion (Y := D.toLocallyRingedSpaceGlueData.glued) (D.toLocallyRingedSpaceGlueData.ι i)

Tactic:
apply LocallyRingedSpace.GlueData.ι_isOpenImmersion

Premises used: AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
apply :
  ∀ (x : (↑D.toLocallyRingedSpaceGlueData.glued.toTopCat : Type u)),
    ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ D.toLocallyRingedSpaceGlueData.glued),
      Membership.mem (γ := Set (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
          (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)))
          x ∧
        LocallyRingedSpace.IsOpenImmersion f
⊢ Scheme

Tactic:
apply LocallyRingedSpace.IsOpenImmersion.scheme
    D.toLocallyRingedSpaceGlueData.toGlueData.glued

Premises used: AlgebraicGeometry.LocallyRingedSpace.GlueData.toGlueData, AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.scheme, CategoryTheory.GlueData.glued
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
x : (↑D.toLocallyRingedSpaceGlueData.glued.toTopCat : Type u)
obtain :
  ∀ (i : D.toLocallyRingedSpaceGlueData.J) (y : (↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat : Type u)),
    ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ D.toLocallyRingedSpaceGlueData.glued),
      Membership.mem (α := (↑D.toLocallyRingedSpaceGlueData.glued.toTopCat : Type u)) (γ :=
          Set (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
          (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  (Y := (↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat))
                  (Hom.base (LocallyRingedSpace.Hom.toHom (D.toLocallyRingedSpaceGlueData.ι i))) :
                (a : (↑(↑(D.toLocallyRingedSpaceGlueData.U i).toPresheafedSpace : TopCat) : Type u)) →
                  (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
              y :
            (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)) ∧
        LocallyRingedSpace.IsOpenImmersion f
⊢ ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ D.toLocallyRingedSpaceGlueData.glued),
    Membership.mem (γ := Set (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
        (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) f.base) :
            (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)))
        x ∧
      LocallyRingedSpace.IsOpenImmersion f

Tactic:
obtain ⟨i, y, rfl⟩ := D.toLocallyRingedSpaceGlueData.ι_jointly_surjective x

Premises used: AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.toLocallyRingedSpaceGlueData.J
y : (↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat : Type u)
j : PreZeroHypercover.I₀ (S := D.U i) (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover)
z : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover) j)
hz : (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover) j) z = y
⊢ ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ D.toLocallyRingedSpaceGlueData.glued),
    Membership.mem (α := (↑D.toLocallyRingedSpaceGlueData.glued.toTopCat : Type u)) (γ :=
        Set (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
        (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) f.base) :
            (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (Y := (↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat))
                (Hom.base (LocallyRingedSpace.Hom.toHom (D.toLocallyRingedSpaceGlueData.ι i))) :
              (a : (↑(↑(D.toLocallyRingedSpaceGlueData.U i).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
            y :
          (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)) ∧
      LocallyRingedSpace.IsOpenImmersion f

Tactic:
⟨_, ((D.U i).affineCover.f j).toLRSHom ≫
    D.toLocallyRingedSpaceGlueData.toGlueData.ι i, ?_⟩

Premises used: AlgebraicGeometry.LocallyRingedSpace.GlueData.toGlueData, AlgebraicGeometry.Scheme.Hom.toLRSHom, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData, CategoryTheory.GlueData.ι, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.GlueData.toGlueData, CategoryTheory.GlueData.U, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.toLocallyRingedSpaceGlueData.J
y : (↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat : Type u)
j : PreZeroHypercover.I₀ (S := D.U i) (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover)
z : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover) j)
hz : (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover) j) z = y
⊢ LocallyRingedSpace.IsOpenImmersion (Y := D.toLocallyRingedSpaceGlueData.glued)
    (Hom.toLRSHom (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover) j) ≫
      D.toLocallyRingedSpaceGlueData.ι i)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
⊢ PreservesColimit D.diagram.multispan forgetToTop

Tactic:
inferInstanceAs (PreservesColimit (𝖣.diagram).multispan (forgetToLocallyRingedSpace ⋙
      LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat))

Premises used: _private.0.AlgebraicGeometry.Scheme.GlueData.instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop._proof_1
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
⊢ PreservesColimit D.diagram.multispan forget

Tactic:
inferInstanceAs (PreservesColimit (𝖣.diagram).multispan (forgetToTop ⋙ CategoryTheory.forget _))

Premises used: _private.0.AlgebraicGeometry.Scheme.GlueData.instPreservesColimitWalkingMultispanProdJMultispanDiagramForget._proof_1
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
⊢ HasMulticoequalizer D.diagram

Tactic:
hasColimit_of_created _ forgetToLocallyRingedSpace

Premises used: AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace, CategoryTheory.hasColimit_of_created
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.J
⊢ D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv = Hom.toLRSHom (D.ι i)

Tactic:
𝖣.ι_gluedIso_inv forgetToLocallyRingedSpace i

Premises used: CategoryTheory.GlueData.ι_gluedIso_inv, CategoryTheory.GlueData.mapGlueData, AlgebraicGeometry.Scheme.GlueData.toGlueData, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.J
rw : LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv)
⊢ IsOpenImmersion (Y := D.glued) (D.ι i)

Tactic:
rw [IsOpenImmersion, ← D.ι_isoLocallyRingedSpace_inv]

Premises used: AlgebraicGeometry.IsOpenImmersion, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.J
⊢ LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
x : ↥D.glued
⊢ ∃ (i : D.J) (y : ↥(D.U i)), (D.ι i) y = x

Tactic:
𝖣.ι_jointly_surjective forget x

Premises used: AlgebraicGeometry.Scheme.forget, AlgebraicGeometry.Scheme.GlueData.toGlueData, CategoryTheory.GlueData.ι_jointly_surjective
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i j : D.J
⊢ D.t i j ≫ D.f j i ≫ D.ι j = D.f i j ≫ D.ι i

Tactic:
𝖣.glue_condition i j

Premises used: CategoryTheory.GlueData.glue_condition, AlgebraicGeometry.Scheme.GlueData.toGlueData
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i j : D.J
⊢ D.f i j ≫ D.ι i = (D.t i j ≫ D.f j i) ≫ D.ι j

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
refine :
  D.glued.toPresheafedSpace ≅ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.glued
⊢ (↑D.glued.toPresheafedSpace : TopCat) ≅
    D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued

Tactic:
refine (PresheafedSpace.forget _).mapIso ?_ ≪≫
    GlueData.gluedIso _ (PresheafedSpace.forget.{_, _, u} _)

Premises used: AlgebraicGeometry.PresheafedSpace.forget, CategoryTheory.Functor.mapIso
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
refine : D.glued.toSheafedSpace ≅ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.glued
⊢ D.glued.toPresheafedSpace ≅ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.glued

Tactic:
refine SheafedSpace.forgetToPresheafedSpace.mapIso ?_ ≪≫
    SheafedSpace.GlueData.isoPresheafedSpace _

Premises used: AlgebraicGeometry.SheafedSpace.GlueData.isoPresheafedSpace, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, CategoryTheory.Functor.mapIso