awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
rw :
  Membership.mem (α := ↥X) (↑V : X.Opens)
    ((pullback.snd ((directedCover X).f U) ((directedCover X).f V) ≫ (directedCover X).f V) x : ↥X)
⊢ Membership.mem (α := ↥X) (↑V : X.Opens)
    ((pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x : ↥X)

Tactic:
rw [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
⊢ Membership.mem (α := ↥X) (↑V : X.Opens)
    ((pullback.snd ((directedCover X).f U) ((directedCover X).f V) ≫ (directedCover X).f V) x : ↥X)

Tactic:
(pullback.snd U.1.ι V.1.ι x).2

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.restrict, AlgebraicGeometry.Scheme.ofRestrict, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, Subtype.val, AlgebraicGeometry.Scheme.Opens.toScheme, DFunLike.coe, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
⊢ Membership.mem (α := ↥X) (↑V : X.Opens)
    ((pullback.snd ((directedCover X).f U) ((directedCover X).f V) ≫ (directedCover X).f V) x : ↥X)

Tactic:
exact (pullback.snd U.1.ι V.1.ι x).2

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
⊢ a ∈ (↑V : X.Opens)

Tactic:
have haV : a ∈ V.1 := by unfold a; rw [pullback.condition]; exact (pullback.snd U.1.ι V.1.ι x).2
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
haV : a ∈ (↑V : X.Opens)
obtain :
  ∀ (f : (↑Γ(X, (↑U : X.Opens)) : Type u)) (g : (↑Γ(X, (↑V : X.Opens)) : Type u)) (e : X.basicOpen f = X.basicOpen g)
    (hxf : a ∈ X.basicOpen f),
    ∃ (k : (directedCover X).I₀) (hki : k ⟶ U) (hkj : k ⟶ V) (y : ↥((directedCover X).X k)),
      (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯) y = x
⊢ ∃ (k : (directedCover X).I₀) (hki : k ⟶ U) (hkj : k ⟶ V) (y : ↥((directedCover X).X k)),
    (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯) y = x

Tactic:
obtain ⟨f, g, e, hxf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 _ ⟨haU, haV⟩

Premises used: And.intro, AlgebraicGeometry.exists_basicOpen_le_affine_inter, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
haV : a ∈ (↑V : X.Opens)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
e : X.basicOpen f = X.basicOpen g
hxf : a ∈ X.basicOpen f
⊢ (↑(basicOpen U f) : X.Opens) = (↑(basicOpen V g) : X.Opens)

Tactic:
e

Premises used: Set.Mem, setOf, AlgebraicGeometry.RingedSpace.basicOpen, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
haV : a ∈ (↑V : X.Opens)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
e : X.basicOpen f = X.basicOpen g
hxf : a ∈ X.basicOpen f
⊢ (↑(basicOpen U f) : X.Opens) = (↑(basicOpen V g) : X.Opens)

Tactic:
exact e
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
haV : a ∈ (↑V : X.Opens)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
e : X.basicOpen f = X.basicOpen g
hxf : a ∈ X.basicOpen f
refine :
  (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯)
      (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ (↑(basicOpen U f) : X.Opens)) a hxf) =
    x
⊢ ∃ (k : (directedCover X).I₀) (hki : k ⟶ U) (hkj : k ⟶ V) (y : ↥((directedCover X).X k)),
    (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯) y = x

Tactic:
refine ⟨U.basicOpen f, homOfLE (U.basicOpen_le f), eqToHom (Subtype.ext (by exact e)) ≫
      homOfLE (V.basicOpen_le g), ⟨a, hxf⟩, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
haV : a ∈ (↑V : X.Opens)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
e : X.basicOpen f = X.basicOpen g
hxf : a ∈ X.basicOpen f
a₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯)
      (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ (↑(basicOpen U f) : X.Opens)) a hxf) =
    x

Tactic:
apply (pullback.fst _ _ ≫ U.1.ι).isOpenEmbedding.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.Limits.pullback.fst, Topology.IsEmbedding.injective, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.Opens.ι, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
haV : a ∈ (↑V : X.Opens)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
e : X.basicOpen f = X.basicOpen g
hxf : a ∈ X.basicOpen f
a₁ :
  a =
    (↑((TopCat.Hom.hom
              (PresheafedSpace.Hom.base
                (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (pullback.fst (↑U : X.Opens).ι (↑V : X.Opens).ι)))) :
            (a : ↥(pullback (↑U : X.Opens).ι (↑V : X.Opens).ι)) → ↥(↑(↑U : X.Opens) : Scheme))
          x) :
      ↥X)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [pullback.lift_fst_assoc, homOfLE_ι, Opens.ι_apply]

Premises used: CategoryTheory.Limits.pullback.lift_fst_assoc, AlgebraicGeometry.Scheme.homOfLE_ι, AlgebraicGeometry.Scheme.Opens.ι_apply
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
haV : a ∈ (↑V : X.Opens)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
e : X.basicOpen f = X.basicOpen g
hxf : a ∈ X.basicOpen f
⊢ a =
    (↑((TopCat.Hom.hom
              (PresheafedSpace.Hom.base
                (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (pullback.fst (↑U : X.Opens).ι (↑V : X.Opens).ι)))) :
            (a : ↥(pullback (↑U : X.Opens).ι (↑V : X.Opens).ι)) → ↥(↑(↑U : X.Opens) : Scheme))
          x) :
      ↥X)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : X.AffineZariskiSite
f : U ⟶ V
dsimp : Spec.map (X.presheaf.map ((toOpensFunctor X).map f).op) ≫ ⋯.fromSpec = ⋯.fromSpec ≫ 𝟙 X
⊢ (toOpensFunctor X ⋙ Functor.rightOp X.presheaf ⋙ Scheme.Spec).map f ≫ ⋯.fromSpec =
    ⋯.fromSpec ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const X.AffineZariskiSite) X) f

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : X.AffineZariskiSite
f : U ⟶ V
rw : ⋯.fromSpec = ⋯.fromSpec ≫ 𝟙 X
⊢ Spec.map (X.presheaf.map ((toOpensFunctor X).map f).op) ≫ ⋯.fromSpec = ⋯.fromSpec ≫ 𝟙 X

Tactic:
rw [V.2.map_fromSpec U.2]

Premises used: AlgebraicGeometry.IsAffineOpen.map_fromSpec, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : X.AffineZariskiSite
f : U ⟶ V
⊢ ⋯.fromSpec = ⋯.fromSpec ≫ 𝟙 X

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
trans :
  NatTrans.Coequifibered α ↔
    ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op)
trans₁ :
  (∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op)) ↔
    ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
                (α.app (Opposite.op U)) :
              (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
                (↑(F.obj (Opposite.op U)) : Type u))
            f :
          (↑(F.obj (Opposite.op U)) : Type u))
        (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
⊢ NatTrans.Coequifibered α ↔
    ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
                (α.app (Opposite.op U)) :
              (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
                (↑(F.obj (Opposite.op U)) : Type u))
            f :
          (↑(F.obj (Opposite.op U)) : Type u))
        (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
trans ∀ (U : X.AffineZariskiSite) (f : Γ(X, U.1)),
    IsPushout (X.presheaf.map (homOfLE (X.basicOpen_le f)).op)
      (α.app _) (α.app (.op (U.basicOpen f))) (F.map (homOfLE (U.basicOpen_le f)).op)
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
⊢ NatTrans.Coequifibered α ↔
    ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op)

Tactic:
⟨fun H U f ↦ H (homOfLE (U.basicOpen_le f)).op, fun H ⟨V⟩ ⟨U⟩ ⟨f, hf⟩ ↦ ?_⟩

Premises used: _private.0.AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway.match_1, CategoryTheory.Functor.op, AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen_le, Quiver.Hom.op, CategoryTheory.Functor.comp, _private.0.AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway.match_3, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.IsPushout, Opposite.op, CategoryTheory.homOfLE, Iff.intro, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, _private.0.AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway.match_2, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor, CategoryTheory.NatTrans.app, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
refine :
  ∀
    (H :
      ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
        IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
          (F.map (homOfLE ⋯).op))
    (x x : X.AffineZariskiSiteᵒᵖ) (V U : X.AffineZariskiSite) (x : Opposite.op V ⟶ Opposite.op U)
    (f : (↑Γ(X, (Opposite.unop (Opposite.op V)).toOpens) : Type u))
    (hf : X.basicOpen f = (Opposite.unop (Opposite.op U)).toOpens),
    IsPushout (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
      (((toOpensFunctor X).op ⋙ X.presheaf).map (Opposite.op { down := { down := ⋯ } })) (α.app (Opposite.op V))
      (α.app (Opposite.op U)) (F.map (Opposite.op { down := { down := ⋯ } }))
⊢ NatTrans.Coequifibered α ↔
    ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op)

Tactic:
refine ⟨fun H U f ↦ H (homOfLE (U.basicOpen_le f)).op, fun H ⟨V⟩ ⟨U⟩ ⟨f, hf⟩ ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H :
  ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
      (F.map (homOfLE ⋯).op)
x x_1 : X.AffineZariskiSiteᵒᵖ
V U : X.AffineZariskiSite
x_2 : Opposite.op V ⟶ Opposite.op U
f : (↑Γ(X, (Opposite.unop (Opposite.op V)).toOpens) : Type u)
hf : X.basicOpen f = (Opposite.unop (Opposite.op U)).toOpens
⊢ V.basicOpen f = U

Tactic:
Subtype.ext hf

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H :
  ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
      (F.map (homOfLE ⋯).op)
x x_1 : X.AffineZariskiSiteᵒᵖ
V U : X.AffineZariskiSite
x_2 : Opposite.op V ⟶ Opposite.op U
f : (↑Γ(X, (Opposite.unop (Opposite.op V)).toOpens) : Type u)
hf : X.basicOpen f = (Opposite.unop (Opposite.op U)).toOpens
obtain :
  ∀ (x : Opposite.op V ⟶ Opposite.op (V.basicOpen f))
    (hf : X.basicOpen f = (Opposite.unop (Opposite.op (V.basicOpen f))).toOpens),
    IsPushout (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op (V.basicOpen f)))
      (((toOpensFunctor X).op ⋙ X.presheaf).map (Opposite.op { down := { down := ⋯ } })) (α.app (Opposite.op V))
      (α.app (Opposite.op (V.basicOpen f))) (F.map (Opposite.op { down := { down := ⋯ } }))
⊢ IsPushout (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
    (((toOpensFunctor X).op ⋙ X.presheaf).map (Opposite.op { down := { down := ⋯ } })) (α.app (Opposite.op V))
    (α.app (Opposite.op U)) (F.map (Opposite.op { down := { down := ⋯ } }))

Tactic:
obtain rfl : V.basicOpen f = U := Subtype.ext hf

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen, rfl, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H :
  ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
      (F.map (homOfLE ⋯).op)
x x_1 : X.AffineZariskiSiteᵒᵖ
V : X.AffineZariskiSite
f : (↑Γ(X, (Opposite.unop (Opposite.op V)).toOpens) : Type u)
x_2 : Opposite.op V ⟶ Opposite.op (V.basicOpen f)
hf : X.basicOpen f = (Opposite.unop (Opposite.op (V.basicOpen f))).toOpens
⊢ IsPushout (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op (V.basicOpen f)))
    (((toOpensFunctor X).op ⋙ X.presheaf).map (Opposite.op { down := { down := ⋯ } })) (α.app (Opposite.op V))
    (α.app (Opposite.op (V.basicOpen f))) (F.map (Opposite.op { down := { down := ⋯ } }))

Tactic:
H V f

Premises used: Set.Mem, Quiver.Hom.op, setOf, AlgebraicGeometry.RingedSpace.basicOpen, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H :
  ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
      (F.map (homOfLE ⋯).op)
x x_1 : X.AffineZariskiSiteᵒᵖ
V : X.AffineZariskiSite
f : (↑Γ(X, (Opposite.unop (Opposite.op V)).toOpens) : Type u)
x_2 : Opposite.op V ⟶ Opposite.op (V.basicOpen f)
hf : X.basicOpen f = (Opposite.unop (Opposite.op (V.basicOpen f))).toOpens
⊢ IsPushout (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op (V.basicOpen f)))
    (((toOpensFunctor X).op ⋙ X.presheaf).map (Opposite.op { down := { down := ⋯ } })) (α.app (Opposite.op V))
    (α.app (Opposite.op (V.basicOpen f))) (F.map (Opposite.op { down := { down := ⋯ } }))

Tactic:
exact H V f
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
⊢ (∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op)) ↔
    ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
                (α.app (Opposite.op U)) :
              (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
                (↑(F.obj (Opposite.op U)) : Type u))
            f :
          (↑(F.obj (Opposite.op U)) : Type u))
        (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
forall₂_congr fun U f ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
refine :
  ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op) ↔
      IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
                (α.app (Opposite.op U)) :
              (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
                (↑(F.obj (Opposite.op U)) : Type u))
            f :
          (↑(F.obj (Opposite.op U)) : Type u))
        (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
⊢ (∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op)) ↔
    ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
                (α.app (Opposite.op U)) :
              (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
                (↑(F.obj (Opposite.op U)) : Type u))
            f :
          (↑(F.obj (Opposite.op U)) : Type u))
        (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
refine forall₂_congr fun U f ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
set :
  let αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U);
  IsPushout (X.presheaf.map (homOfLE ⋯).op) αU (α.app (Opposite.op (U.basicOpen f))) (F.map (homOfLE ⋯).op) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
⊢ IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
      (F.map (homOfLE ⋯).op) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
              (α.app (Opposite.op U)) :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
set αU : Γ(X, U.toOpens) ⟶ F.obj (.op U) := α.app (.op U)

Premises used: Opposite.op, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app