awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
h𝒰 :
  ∀ (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)
⊢ P.diagonal f

Tactic:
diagonal_of_openCover P f 𝒰 (fun _ ↦ Scheme.affineCover _)
    (fun _ _ _ ↦ h𝒰 _ _ _)

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.affineCover, AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y U V : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsAffine U
inst_2 : IsOpenImmersion g
iV : V ⟶ X
f' : V ⟶ U
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
rw : Q.diagonal (X := pullback f g) (pullback.snd f g)
⊢ Q.diagonal f'

Tactic:
rw [← Q.diagonal.cancel_left_of_respectsIso h.isoPullback.inv,
    h.isoPullback_inv_snd]

Premises used: CategoryTheory.IsPullback.isoPullback_inv_snd, CategoryTheory.IsPullback.isoPullback, AlgebraicGeometry.AffineTargetMorphismProperty.diagonal, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y U_1 V_1 : Scheme
f : X ⟶ Y
g : U_1 ⟶ Y
inst_1 : IsAffine U_1
inst_2 : IsOpenImmersion g
iV : V_1 ⟶ X
f' : V_1 ⟶ U_1
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
rw :
  Q (X :=
    pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯))
    (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
    (CategoryStruct.comp (Y := pullback f₁ f₂)
        (Iso.hom (pullbackDiagonalMapIso f g f₁ f₂) :
          pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
              (pullback.diagonal f)
              (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
                (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
            pullback f₁ f₂)
        (pullback.mapDesc f₁ f₂ (pullback.snd f g) :
          pullback f₁ f₂ ⟶ pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) :
      pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
          (pullback.diagonal f)
          (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
            (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
        pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
⊢ Q (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
    (pullback.mapDesc f₁ f₂ (pullback.snd f g))

Tactic:
rw [← Q.cancel_left_of_respectsIso (pullbackDiagonalMapIso f _ f₁ f₂).hom]

Premises used: CategoryTheory.Limits.pullbackDiagonalMapIso, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y U_1 V_1 : Scheme
f : X ⟶ Y
g : U_1 ⟶ Y
inst_1 : IsAffine U_1
inst_2 : IsOpenImmersion g
iV : V_1 ⟶ X
f' : V_1 ⟶ U_1
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ Q (X :=
    pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯))
    (pullback.snd (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯))

Tactic:
HasAffineProperty.of_isPullback (P := P) (.of_hasPullback _ _) H

Premises used: AlgebraicGeometry.HasAffineProperty.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y U_1 V_1 : Scheme
f : X ⟶ Y
g : U_1 ⟶ Y
inst_1 : IsAffine U_1
inst_2 : IsOpenImmersion g
iV : V_1 ⟶ X
f' : V_1 ⟶ U_1
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
e_1 :
  pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯) =
    pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯)
e_2 :
  pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) = pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)
⊢ Eq (α :=
    pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
        (pullback.diagonal f)
        (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
          (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
      U)
    (CategoryStruct.comp (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
        (CategoryStruct.comp (Y := pullback f₁ f₂)
          (Iso.hom (pullbackDiagonalMapIso f g f₁ f₂) :
            pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
                (pullback.diagonal f)
                (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
                  (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
              pullback f₁ f₂)
          (pullback.mapDesc f₁ f₂ (pullback.snd f g) :
            pullback f₁ f₂ ⟶ pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)))
        (pullback.fst (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) :
      pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
          (pullback.diagonal f)
          (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
            (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
        U)
    (pullback.snd (pullback.diagonal f)
          (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
            (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ≫
        pullback.fst (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) :
      pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
          (pullback.diagonal f)
          (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
            (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
        U)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y U_1 V_1 : Scheme
f : X ⟶ Y
g : U_1 ⟶ Y
inst_1 : IsAffine U_1
inst_2 : IsOpenImmersion g
iV : V_1 ⟶ X
f' : V_1 ⟶ U_1
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
e_1 :
  pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯) =
    pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯)
e_2 :
  pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) = pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)
⊢ Eq (α :=
    pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
        (pullback.diagonal f)
        (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
          (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
      V)
    (CategoryStruct.comp (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
        (CategoryStruct.comp (Y := pullback f₁ f₂)
          (Iso.hom (pullbackDiagonalMapIso f g f₁ f₂) :
            pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
                (pullback.diagonal f)
                (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
                  (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
              pullback f₁ f₂)
          (pullback.mapDesc f₁ f₂ (pullback.snd f g) :
            pullback f₁ f₂ ⟶ pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)))
        (pullback.snd (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) :
      pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
          (pullback.diagonal f)
          (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
            (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
        V)
    (pullback.snd (pullback.diagonal f)
          (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
            (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ≫
        pullback.snd (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) :
      pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
          (pullback.diagonal f)
          (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
            (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
        V)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y U_1 V_1 : Scheme
f : X ⟶ Y
g : U_1 ⟶ Y
inst_1 : IsAffine U_1
inst_2 : IsOpenImmersion g
iV : V_1 ⟶ X
f' : V_1 ⟶ U_1
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ IsAffine.{u} (pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y U_1 V_1 : Scheme
f : X ⟶ Y
g : U_1 ⟶ Y
inst_1 : IsAffine U_1
inst_2 : IsOpenImmersion g
iV : V_1 ⟶ X
f' : V_1 ⟶ U_1
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ IsOpenImmersion (X := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Y := pullback.diagonalObj f)
    (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g) g
      ⋯ ⋯)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
⊢ Q.diagonal f ↔ P.diagonal f

Tactic:
⟨fun hf ↦ ?_, diagonal_of_diagonal_of_isPullback P .of_id_fst⟩

Premises used: CategoryTheory.IsPullback.of_id_fst, AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullback, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
refine : ∀ (hf : Q.diagonal f), P.diagonal f
⊢ Q.diagonal f ↔ P.diagonal f

Tactic:
refine ⟨fun hf ↦ ?_, diagonal_of_diagonal_of_isPullback P .of_id_fst⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
hf : Q.diagonal f
⊢ Q.diagonal (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))

Tactic:
rw [← Q.diagonal.cancel_left_of_respectsIso
    (pullback.fst (f := f) (g := 𝟙 Y)), pullback.condition, Category.comp_id] at hf

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.fst, AlgebraicGeometry.AffineTargetMorphismProperty.diagonal, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
hf : Q.diagonal (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) (pullback f (𝟙 Y)) :=
  Scheme.Cover.pushforwardIso (P := IsOpenImmersion) X.affineCover (inv (pullback.fst f (𝟙 Y)))
i : 𝒰.I₀
dsimp :
  IsAffine.{u}
    (X.affineCover.X
      (Sigma.snd (β := fun (i : PUnit.{u + 1}) ↦ X.affineCover.I₀)
        ((Equiv.trans (Equiv.symm (Equiv.punitProd X.affineCover.I₀))
              (Equiv.symm (Equiv.sigmaEquivProd PUnit.{u + 1} X.affineCover.I₀)) :
            (a : X.affineCover.I₀) → (_ : PUnit.{u + 1}) × X.affineCover.I₀)
          i)))
⊢ IsAffine.{u} (𝒰.X i)

Tactic:
dsimp [𝒰]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
hf : Q.diagonal (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) (pullback f (𝟙 Y)) :=
  Scheme.Cover.pushforwardIso (P := IsOpenImmersion) X.affineCover (inv (pullback.fst f (𝟙 Y)))
i : 𝒰.I₀
⊢ IsAffine.{u}
    (X.affineCover.X
      (Sigma.snd (β := fun (i : PUnit.{u + 1}) ↦ X.affineCover.I₀)
        ((Equiv.trans (Equiv.symm (Equiv.punitProd X.affineCover.I₀))
              (Equiv.symm (Equiv.sigmaEquivProd PUnit.{u + 1} X.affineCover.I₀)) :
            (a : X.affineCover.I₀) → (_ : PUnit.{u + 1}) × X.affineCover.I₀)
          i)))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
hf : Q.diagonal (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) (pullback f (𝟙 Y)) :=
  Scheme.Cover.pushforwardIso (P := IsOpenImmersion) X.affineCover (inv (pullback.fst f (𝟙 Y)))
⊢ ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)

Tactic:
have (i : _) : IsAffine (𝒰.X i) := by dsimp [𝒰]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this_1 : Q.IsLocal := ⋯
hf : Q.diagonal (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) (pullback f (𝟙 Y)) :=
  Scheme.Cover.pushforwardIso (P := IsOpenImmersion) X.affineCover (inv (pullback.fst f (𝟙 Y)))
this : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
⊢ P.diagonal f

Tactic:
HasAffineProperty.diagonal_of_openCover.{u, u, u} P f (Scheme.coverOfIsIso (𝟙 _))
    (fun _ ↦ 𝒰) (fun _ _ _ ↦ hf _ _)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.coverOfIsIso, CategoryTheory.CategoryStruct.id, AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover, 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
inst_1 : IsAffine Y
this_1 : Q.IsLocal := ⋯
hf : Q.diagonal (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) (pullback f (𝟙 Y)) :=
  Scheme.Cover.pushforwardIso (P := IsOpenImmersion) X.affineCover (inv (pullback.fst f (𝟙 Y)))
this : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
⊢ P.diagonal f

Tactic:
exact HasAffineProperty.diagonal_of_openCover.{u, u, u} P f (Scheme.coverOfIsIso (𝟙 _))
    (fun _ ↦ 𝒰) (fun _ _ _ ↦ hf _ _)
-- 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)
rw : (targetAffineLocally Q).diagonal f
⊢ Q.diagonal f

Tactic:
rw [HasAffineProperty.diagonal_iff (targetAffineLocally Q)]

Premises used: AlgebraicGeometry.HasAffineProperty.diagonal_iff, AlgebraicGeometry.targetAffineLocally
-- 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
i : 𝒱.I₀
dsimp : IsAffine.{u} (pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f))
⊢ IsAffine.{u} (𝒱.X i)

Tactic:
dsimp [𝒱]
-- 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
i : 𝒱.I₀
⊢ IsAffine.{u} (pullback (X := 𝒰.X i.1) (Y := 𝒰.X i.2) (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f))

Tactic:
infer_instance
-- 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
⊢ ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)

Tactic:
have i1 : ∀ i, IsAffine (𝒱.X i) := fun i => by dsimp [𝒱]; infer_instance
-- 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)
⊢ (targetAffineLocally Q).diagonal f

Tactic:
HasAffineProperty.of_openCover (P := targetAffineLocally Q) 𝒱 fun i ↦ ?_

Premises used: CategoryTheory.MorphismProperty.diagonal, AlgebraicGeometry.HasAffineProperty.of_openCover, AlgebraicGeometry.targetAffineLocally
-- 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)
refine :
  ∀ (i : 𝒱.toPreZeroHypercover.1),
    Q (X := (Precoverage.ZeroHypercover.pullback₁ (pullback.diagonal f) 𝒱).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒱 (pullback.diagonal f) i :
        (Precoverage.ZeroHypercover.pullback₁ (pullback.diagonal f) 𝒱).X i ⟶ 𝒱.X i)
⊢ (targetAffineLocally Q).diagonal f

Tactic:
refine HasAffineProperty.of_openCover (P := targetAffineLocally Q) 𝒱 fun i ↦ ?_

Premises used: AlgebraicGeometry.HasAffineProperty.of_openCover
-- 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) ((𝒰.f i.1 ≫ 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) ((𝒰.f i.2 ≫ 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
⊢ CategoryStruct.comp (Y := pullback f (𝟙 Y)) (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (pullback.fst f (𝟙 Y)) =
    𝟙 (𝒰.X i.1) ≫ 𝒰.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
⊢ CategoryStruct.comp (Y := pullback f (𝟙 Y)) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) (pullback.fst f (𝟙 Y)) =
    𝟙 (𝒰.X i.2) ≫ 𝒰.f i.2

Tactic:
simp