awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ Eq (α := 𝒰.X i.1 ⟶ Y)
    (CategoryStruct.comp (Y := pullback f (𝟙 Y)) (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (pullback.snd f (𝟙 Y)))
    (𝒰.f i.1 ≫ f)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ Eq (α := 𝒰.X i.2 ⟶ Y)
    (CategoryStruct.comp (Y := pullback f (𝟙 Y)) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) (pullback.snd f (𝟙 Y)))
    (𝒰.f i.2 ≫ f)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ Eq (α :=
    pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (Z := pullback f (𝟙 Y)) (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯)
        (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ⟶
      X)
    ((pullback.fst (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫
        CategoryStruct.comp (Y := pullback f (𝟙 Y)) (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (pullback.fst f (𝟙 Y))) ≫
      Iso.hom (Iso.refl X))
    (CategoryStruct.comp (Y := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1) (𝒰.f i.2))
      (Iso.hom
        (asIso
          (pullback.map (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.1) (𝒰.f i.2)
            (𝟙 (𝒰.X i.1)) (𝟙 (𝒰.X i.2)) (pullback.fst f (𝟙 Y)) ⋯ ⋯)))
      (pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ pullback.diagonal f ≫ Iso.hom (Iso.refl (pullback.diagonalObj f)) = Iso.hom (Iso.refl X) ≫ pullback.diagonal f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
have :
  ∀
    (this :
      IsPullback (P := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1) (𝒰.f i.2)) (Y :=
        pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
        (pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f) (pullback.diagonal f)
        (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯)),
    Q (X :=
      pullback (Y := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
        (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))
      (pullback.snd (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))
⊢ Q (X :=
    pullback (Y := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))
    (pullback.snd (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))

Tactic:
have : IsPullback (pullback.fst _ _ ≫ 𝒰.f _) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f)
      (pullback.diagonal f) (pullback.map _ _ _ _ (𝒰.f _) (𝒰.f _) (𝟙 Y) (by simp) (by simp)) :=
    .of_iso (pullback_fst_map_snd_isPullback f (𝟙 _) (𝒰.f i.1 ≫ pullback.lift (𝟙 _) f)
      (𝒰.f i.2 ≫ pullback.lift (𝟙 _) f)) (asIso (pullback.map _ _ _ _ (𝟙 _) (𝟙 _)
      (pullback.fst _ _) (by simp) (by simp))) (.refl _) (pullback.congrHom (by simp) (by simp))
      (.refl _) (by simp) (by cat_disch) (by simp) (by cat_disch)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
this :
  IsPullback (P := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1) (𝒰.f i.2)) (Y :=
    pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
    (pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f) (pullback.diagonal f)
    (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯)
rw :
  Q (X := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1) (𝒰.f i.2)) (Y :=
    pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f)
⊢ Q (X :=
    pullback (Y := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))
    (pullback.snd (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))

Tactic:
rw [← Q.cancel_left_of_respectsIso this.isoPullback.hom, IsPullback.isoPullback_hom_snd]

Premises used: CategoryTheory.IsPullback.isoPullback, CategoryTheory.IsPullback.isoPullback_hom_snd, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
this :
  IsPullback (P := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1) (𝒰.f i.2)) (Y :=
    pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
    (pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f) (pullback.diagonal f)
    (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯)
⊢ Q (X := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1) (𝒰.f i.2)) (Y :=
    pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f)

Tactic:
h𝒰 _ _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_2 : IsAffine Y
h𝒰 :
  ∀ (i j : 𝒰.I₀),
    Q (X := pullback (𝒰.f i) (𝒰.f j)) (Y := pullback (𝒰.f i ≫ f) (𝒰.f j ≫ f)) (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : Scheme.OpenCover.{v, u} (pullback f f) := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
this :
  IsPullback (P := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1) (𝒰.f i.2)) (Y :=
    pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (Z := pullback.diagonalObj f)
    (pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f) (pullback.diagonal f)
    (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯)
⊢ Q (X := pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1) (𝒰.f i.2)) (Y :=
    pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f)) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f)

Tactic:
exact h𝒰 _ _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u_1)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hs' :
  ∀ (r : ↥s),
    Q.diagonal (X := (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme))
      (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1)))
⊢ Q.diagonal f

Tactic:
(diagonal_iff (targetAffineLocally Q)).mpr ?_

Premises used: Iff.mpr, AlgebraicGeometry.HasAffineProperty.diagonal_iff, AlgebraicGeometry.targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u_1)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hs' :
  ∀ (r : ↥s),
    Q.diagonal (X := (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme))
      (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1)))
refine : (targetAffineLocally Q).diagonal f
⊢ Q.diagonal f

Tactic:
refine (diagonal_iff (targetAffineLocally Q)).mpr ?_

Premises used: Iff.mpr, AlgebraicGeometry.HasAffineProperty.diagonal_iff, AlgebraicGeometry.targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u_1)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hs' :
  ∀ (r : ↥s),
    Q.diagonal (X := (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme))
      (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1)))
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun (f : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)) ↦ Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⋯
⊢ ∀ (i : 𝒰.I₀), IsAffine.{u_1} (𝒰.X i)

Tactic:
have (i : _) : IsAffine (𝒰.X i) := (isAffineOpen_top Y).basicOpen i.1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u_1)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hs' :
  ∀ (r : ↥s),
    Q.diagonal (X := (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme))
      (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1)))
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun (f : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)) ↦ Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⋯
this : ∀ (i : 𝒰.I₀), IsAffine.{u_1} (𝒰.X i)
⊢ (targetAffineLocally Q).diagonal f

Tactic:
diagonal_of_openCover_diagonal (targetAffineLocally Q) f 𝒰 ?_

Premises used: AlgebraicGeometry.targetAffineLocally, AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u_1)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hs' :
  ∀ (r : ↥s),
    Q.diagonal (X := (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme))
      (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1)))
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun (f : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)) ↦ Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⋯
this : ∀ (i : 𝒰.I₀), IsAffine.{u_1} (𝒰.X i)
refine :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    Q.diagonal (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
⊢ (targetAffineLocally Q).diagonal f

Tactic:
refine diagonal_of_openCover_diagonal (targetAffineLocally Q) f 𝒰 ?_

Premises used: AlgebraicGeometry.targetAffineLocally, AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u_1)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hs' :
  ∀ (r : ↥s),
    Q.diagonal (X := (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme))
      (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1)))
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun (f : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)) ↦ Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⋯
this : ∀ (i : 𝒰.I₀), IsAffine.{u_1} (𝒰.X i)
i : 𝒰.toPreZeroHypercover.1
⊢ Y.basicOpen (↑i : (↑Γ(Y, ⊤) : Type u_1)) = Scheme.Hom.opensRange (𝒰.f i)

Tactic:
simp [𝒰]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
Q : AffineTargetMorphismProperty
inst : Q.IsLocal
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u_1)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hs' :
  ∀ (r : ↥s),
    Q.diagonal (X := (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme))
      (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1)))
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun (f : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)) ↦ Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⋯
this : ∀ (i : 𝒰.I₀), IsAffine.{u_1} (𝒰.X i)
i : 𝒰.toPreZeroHypercover.1
⊢ Q.diagonal (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)

Tactic:
exact (Q.diagonal.arrow_mk_iso_iff
      (morphismRestrictEq _ (by simp [𝒰]) ≪≫ morphismRestrictOpensRange _ _)).mp (hs' i)

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictOpensRange, AlgebraicGeometry.morphismRestrictEq, CategoryTheory.Iso.trans, Iff.mp, AlgebraicGeometry.AffineTargetMorphismProperty.diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y), P.diagonal f ↔ targetAffineLocally Q.diagonal f
⊢ P.diagonal = targetAffineLocally Q.diagonal

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
h : P.diagonal f → targetAffineLocally Q.diagonal f
h₁ : targetAffineLocally Q.diagonal f → P.diagonal f
⊢ P.diagonal f ↔ targetAffineLocally Q.diagonal f

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ P.diagonal f → targetAffineLocally Q.diagonal f

Tactic:
fun H U ↦ HasAffineProperty.diagonal_of_diagonal_of_isPullback P
        (isPullback_morphismRestrict f U).flip H

Premises used: AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullback, AlgebraicGeometry.targetAffineLocally, CategoryTheory.IsPullback.flip, AlgebraicGeometry.isPullback_morphismRestrict, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ P.diagonal f → targetAffineLocally Q.diagonal f

Tactic:
exact fun H U ↦ HasAffineProperty.diagonal_of_diagonal_of_isPullback P
        (isPullback_morphismRestrict f U).flip H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ targetAffineLocally Q.diagonal f → P.diagonal f

Tactic:
fun H ↦ HasAffineProperty.diagonal_of_openCover_diagonal P f Y.affineCover
        (fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) H)

Premises used: AlgebraicGeometry.of_targetAffineLocally_of_isPullback, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover_diagonal, CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ targetAffineLocally Q.diagonal f → P.diagonal f

Tactic:
exact fun H ↦ HasAffineProperty.diagonal_of_openCover_diagonal P f Y.affineCover
        (fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) H)

Premises used: AlgebraicGeometry.of_targetAffineLocally_of_isPullback, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover_diagonal, CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
⊢ IsZariskiLocalAtTarget.{u_1} P.diagonal

Tactic:
letI := HasAffineProperty.of_isZariskiLocalAtTarget P
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
U : X.Opens
⊢ (U.ι ≫ f) ≫ 𝟙 Y = U.ι ≫ f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
⊢ IsZariskiLocalAtSource.{u_1} P.diagonal

Tactic:
IsZariskiLocalAtSource.mk' (fun {X Y} f U hf ↦ ?_) (fun {X Y} f {ι} U hU hf ↦ ?_)

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.mk'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
refine_1 : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) (hf : P.diagonal f), P.diagonal (U.ι ≫ f)
refine_2 :
  ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) {ι : Type u_1} (U : ι → X.Opens) (hU : iSup U = ⊤)
    (hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)), P.diagonal f
⊢ IsZariskiLocalAtSource.{u_1} P.diagonal

Tactic:
refine IsZariskiLocalAtSource.mk' (fun {X Y} f U hf ↦ ?_) (fun {X Y} f {ι} U hU hf ↦ ?_)

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.mk'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
refine_1 : P (Y := pullback.diagonalObj (U.ι ≫ f)) (pullback.diagonal (U.ι ≫ f))
⊢ P.diagonal (U.ι ≫ f)

Tactic:
change P _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
refine_1 : P (pullback.diagonal (U.ι ≫ f) ≫ g f U)
⊢ P (Y := pullback.diagonalObj (U.ι ≫ f)) (pullback.diagonal (U.ι ≫ f))

Tactic:
apply P.of_postcomp (W' := @IsOpenImmersion) (pullback.diagonal (U.ι ≫ f)) (g f U) inferInstance

Premises used: inferInstance, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.MorphismProperty.of_postcomp, CategoryTheory.Limits.pullback.diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
refine_1 : P (Y := pullback f f) (U.ι ≫ pullback.diagonal f)
⊢ P (pullback.diagonal (U.ι ≫ f) ≫ g f U)

Tactic:
rw [← pullback.comp_diagonal]

Premises used: CategoryTheory.Limits.pullback.comp_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
refine_1 : P (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ P (Y := pullback f f) (U.ι ≫ pullback.diagonal f)

Tactic:
apply IsZariskiLocalAtSource.comp

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
hf

Premises used: CategoryTheory.MorphismProperty.diagonal