awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ Scheme.Spec.map
        (Quiver.Hom.op
          (Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
            (X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u))))
            ⋯)) ≫
      ⋯.isoSpec.symm.hom =
    e.symm.hom ≫ Cover.pullbackHom (P := IsOpenImmersion) Y.openCoverBasicOpenTop f r
have refine_1 : e.hom ≫
    Scheme.Spec.map
      (Quiver.Hom.op
        (Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
          (X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (↑r : (↑Γ(Y, ⊤) : Type u))))
          sorry)) =
  Cover.pullbackHom (P := IsOpenImmersion) Y.openCoverBasicOpenTop f r ≫ sorry.isoSpec.hom
Tactic: simp only [Iso.symm_hom, Iso.eq_inv_comp, ← Category.assoc, Iso.comp_inv_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ e.hom ≫
      Scheme.Spec.map
        (Quiver.Hom.op
          (Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
            (X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u))))
            ⋯)) =
    Cover.pullbackHom (P := IsOpenImmersion) Y.openCoverBasicOpenTop f r ≫ ⋯.isoSpec.hom
have refine_1 : (Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫
      Iso.hom (X.isoOfEq sorry) ≫
        (X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (↑r : (↑Γ(Y, ⊤) : Type u)))).toSpecΓ) ≫
    Spec.map (Hom.app f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE sorry))) =
  pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ
Tactic: dsimp [e, Scheme.Cover.pullbackHom, IsAffineOpen.isoSpec_hom, Scheme.Hom.appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ (Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫
        Iso.hom (X.isoOfEq ⋯) ≫
          (X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u)))).toSpecΓ) ≫
      Spec.map (Hom.app f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ
have refine_1 : Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫
    Iso.hom (X.isoOfEq sorry) ≫
      X.homOfLE sorry ≫ f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)) ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ =
  pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ
Tactic: simp only [homOfLE_leOfHom, Spec.map_comp, Category.assoc,
      Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, Scheme.Opens.toSpecΓ_naturality]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫
      Iso.hom (X.isoOfEq ⋯) ≫
        X.homOfLE ⋯ ≫ f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)) ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ
have refine_1 : (((Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫ Iso.hom (X.isoOfEq sorry)) ≫
        X.homOfLE sorry) ≫
      f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≫
    (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ =
  pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ
Tactic: simp_rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ (((Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫ Iso.hom (X.isoOfEq ⋯)) ≫
          X.homOfLE ⋯) ≫
        f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≫
      (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ
have refine_1 : ((Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫ Iso.hom (X.isoOfEq sorry)) ≫
      X.homOfLE sorry) ≫
    f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)) =
  pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ ((Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫ Iso.hom (X.isoOfEq ⋯)) ≫
        X.homOfLE ⋯) ≫
      f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)) =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι
have refine_1 : (((Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫ Iso.hom (X.isoOfEq sorry)) ≫
        X.homOfLE sorry) ≫
      f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≫
    (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι =
  pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι
Tactic: rw [← cancel_mono (Scheme.Opens.ι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ Scheme.Spec.map (Quiver.Hom.op (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) ≫
      Iso.hom (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))) =
    e.symm.hom ≫ (Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ
have refine_2 : e.hom ≫
    Scheme.Spec.map (Quiver.Hom.op (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))) ≫
      Iso.hom (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))) =
  (Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ
Tactic: simp only [Iso.symm_hom, Iso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq :
  Eq (α := ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fi)) : (a : ↥(F.obj i)) → ↥(F.obj k)) xi : ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fj)) : (a : ↥(F.obj j)) → ↥(F.obj k)) xj : ↥(F.obj k))
⊢ Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fi) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj k))
        ((s.app i) xi : ↥(G.obj i)) :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fj) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj k))
        ((s.app j) xj : ↥(G.obj j)) :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj k))
have simp : Eq (α := ↥(G.obj k)) ((G.map fi) ((s.app i) xi : ↥(G.obj i)) : ↥(G.obj k))
  ((G.map fj) ((s.app j) xj : ↥(G.obj j)) : ↥(G.obj k))
Tactic: simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : Eq (α := ↥(F.obj k)) ((F.map fi) xi : ↥(F.obj k)) ((F.map fj) xj : ↥(F.obj k))
⊢ Eq (α := ↥(G.obj k)) ((G.map fi) ((s.app i) xi : ↥(G.obj i)) : ↥(G.obj k))
    ((G.map fj) ((s.app j) xj : ↥(G.obj j)) : ↥(G.obj k))
have rw : Eq (α := ↥(G.obj k)) ((s.app j ≫ G.map fj) xj : ↥(G.obj k)) ((G.map fj) ((s.app j) xj : ↥(G.obj j)) : ↥(G.obj k))
Tactic: rw [← Scheme.Hom.comp_apply, ← s.naturality, Scheme.Hom.comp_apply, heq,
        ← Scheme.Hom.comp_apply, s.naturality]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq :
  Eq (α := ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fi)) : (a : ↥(F.obj i)) → ↥(F.obj k)) xi : ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fj)) : (a : ↥(F.obj j)) → ↥(F.obj k)) xj : ↥(F.obj k))
⊢ ∃ (l : J) (fli : l ⟶ i) (flj : l ⟶ j) (x : (F ⋙ forget).obj l),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
          x =
        xi ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
          x =
        xj
have obtain : ∀ (l : J) (fli : l ⟶ i) (flj : l ⟶ j) (x : (G ⋙ forget).obj l)
  (hi :
    Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fli) :
            (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
          x :
        (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
      ((s.app i) xi : ↥(G.obj i)))
  (hj :
    Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map flj) :
            (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
          x :
        (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
      ((s.app j) xj : ↥(G.obj j))),
  ∃ (l : J) (fli : l ⟶ i) (flj : l ⟶ j) (x : (F ⋙ forget).obj l),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
          x =
        xi ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
          x =
        xj
Tactic: obtain ⟨l, fli, flj, x, hi, hj⟩ := (G ⋙ Scheme.forget).exists_map_eq_of_isLocallyDirected fi fj
        (s.app i xi) (s.app j xj) <| by
      simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
      dsimp at heq
      rw [← Scheme.Hom.comp_apply, ← s.naturality, Scheme.Hom.comp_apply, heq,
        ← Scheme.Hom.comp_apply, s.naturality]
      simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq :
  Eq (α := ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fi)) : (a : ↥(F.obj i)) → ↥(F.obj k)) xi : ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fj)) : (a : ↥(F.obj j)) → ↥(F.obj k)) xj : ↥(F.obj k))
l : J
fli : l ⟶ i
flj : l ⟶ j
x : (G ⋙ forget).obj l
hi :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fli) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((s.app i) xi : ↥(G.obj i))
hj :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map flj) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((s.app j) xj : ↥(G.obj j))
⊢ ∃ (l : J) (fli : l ⟶ i) (flj : l ⟶ j) (x : (F ⋙ forget).obj l),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
          x =
        xi ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
          x =
        xj
have h : ∃ (x : (F ⋙ forget).obj l),
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
        x =
      xi ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
        x =
      xj
Tactic: use l, fli, flj