awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Y : Scheme
inst_1 : Subsingleton.{u + 1} ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
this :
  ∀ {Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (R : CommRingCat.{u}) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R)
    (hg : g ≫ f = 𝟙 Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsClosedImmersion g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
inst : Subsingleton.{u + 1} ↥(Spec Γ(Y, ⊤))
⊢ (Y.isoSpec.inv ≫ g) ≫ f ≫ Y.isoSpec.hom = 𝟙 (Spec Γ(Y, ⊤))

Tactic:
simp [reassoc_of% hg]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Y : Scheme
inst_1 : Subsingleton.{u + 1} ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
this :
  ∀ {Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (R : CommRingCat.{u}) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R)
    (hg : g ≫ f = 𝟙 Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsClosedImmersion g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
inst : Subsingleton.{u + 1} ↥(Spec Γ(Y, ⊤))
⊢ IsClosedImmersion (Y.isoSpec.inv ≫ g)

Tactic:
exact this R (f ≫ (Scheme.isoSpec Y).hom) ((Scheme.isoSpec Y).inv ≫ g)
      (by simp [reassoc_of% hg]) ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.isoSpec, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
hY : ∃ (S : CommRingCat.{u}), Y = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) [Subsingleton.{u + 1} ↥(Spec S)] (f : Spec R ⟶ Spec S) (g : Spec S ⟶ Spec R)
    (hg : g ≫ f = 𝟙 (Spec S)), IsClosedImmersion g
⊢ IsClosedImmersion g

Tactic:
obtain ⟨S, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
f : Spec R ⟶ Spec S
g : Spec S ⟶ Spec R
hg : g ≫ f = 𝟙 (Spec S)
obtain : ∀ (φ : S ⟶ R) (hg : g ≫ Spec.map φ = 𝟙 (Spec S)), IsClosedImmersion g
⊢ IsClosedImmersion g

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
g : Spec S ⟶ Spec R
φ : S ⟶ R
hg : g ≫ Spec.map φ = 𝟙 (Spec S)
obtain : ∀ (ψ : R ⟶ S) (hg : Spec.map ψ ≫ Spec.map φ = 𝟙 (Spec S)), IsClosedImmersion (Spec.map ψ)
⊢ IsClosedImmersion g

Tactic:
obtain ⟨ψ, rfl⟩ := Spec.map_surjective g

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : Spec.map ψ ≫ Spec.map φ = 𝟙 (Spec S)
⊢ φ ≫ ψ = 𝟙 S

Tactic:
rw [← Spec.map_comp, ← Spec.map_id, Spec.map_injective.eq_iff] at hg

Premises used: AlgebraicGeometry.Spec.map_injective, Function.Injective.eq_iff, AlgebraicGeometry.Spec.map_id, AlgebraicGeometry.Spec.map_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : φ ≫ ψ = 𝟙 S
h :
  Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) ψ) :
      (a : (↑R : Type u)) → (↑S : Type u))
⊢ IsClosedImmersion (Spec.map ψ)

Tactic:
apply IsClosedImmersion.spec_of_surjective

Premises used: AlgebraicGeometry.IsClosedImmersion.spec_of_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : φ ≫ ψ = 𝟙 S
h :
  Function.LeftInverse (α := (↑S : Type u)) (β := (↑R : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) ψ) :
      (a : (↑R : Type u)) → (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑S : Type u)) → (↑R : Type u))
⊢ Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) ψ) :
      (a : (↑R : Type u)) → (↑S : Type u))

Tactic:
apply Function.LeftInverse.surjective (g := φ)

Premises used: Function.LeftInverse.surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : φ ≫ ψ = 𝟙 S
⊢ Function.LeftInverse (α := (↑S : Type u)) (β := (↑R : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) ψ) :
      (a : (↑R : Type u)) → (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑S : Type u)) → (↑R : Type u))

Tactic:
fun x ↦ congr($hg.1 x)

Premises used: Function.LeftInverse, congrArg, id, DFunLike.coe, CommRingCat.Hom.hom'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : φ ≫ ψ = 𝟙 S
⊢ Function.LeftInverse (α := (↑S : Type u)) (β := (↑R : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) ψ) :
      (a : (↑R : Type u)) → (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑S : Type u)) → (↑R : Type u))

Tactic:
exact fun x ↦ congr($hg.1 x)

Premises used: congrArg, id, DFunLike.coe, CommRingCat.Hom.hom'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X_1 Y_1 Z X Y : Scheme
inst : Subsingleton.{u + 1} ↥X
f : Retract X Y
⊢ IsClosedImmersion f.i

Tactic:
isClosedImmersion_of_comp_eq_id _ _ f.retract

Premises used: CategoryTheory.Retract.retract, AlgebraicGeometry.isClosedImmersion_of_comp_eq_id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X_1 Y_1 Z X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
inst_1 : X.Over Y
f : Y ⟶ X
inst_2 : Scheme.Hom.IsOver f Y
⊢ f ≫ X ↘ Y = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
h₁ :
  ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z],
    (∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ Y) (f₂ : U₂ ⟶ Y) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
        [IsOpenImmersion f₁] [IsOpenImmersion f₂],
        P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)) →
      ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
        [IsOpenImmersion f₁] [IsOpenImmersion f₂],
        P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ e.hom ≫ f) (f₂ ≫ e.hom ≫ f)) (pullback.mapDesc f₁ f₂ (e.hom ≫ f))
h₂ :
  ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y],
    (∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
        [IsOpenImmersion f₁] [IsOpenImmersion f₂],
        P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)) →
      ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
        [IsOpenImmersion f₁] [IsOpenImmersion f₂],
        P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f ≫ e.hom) (f₂ ≫ f ≫ e.hom)) (pullback.mapDesc f₁ f₂ (f ≫ e.hom))
⊢ (toProperty fun {X x : Scheme.{u_1}} (f : X ⟶ x) (x_1 : IsAffine x) ↦
      ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂]
        [IsOpenImmersion f₁] [IsOpenImmersion f₂],
        P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)).RespectsIso

Tactic:
apply AffineTargetMorphismProperty.respectsIso_mk

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst_1 : IsAffine Z
H :
  ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ Y) (f₂ : U₂ ⟶ Y) [inst : IsAffine U₁] [inst_6 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_2 : IsAffine U₁
inst_3 : IsAffine U₂
inst_4 : IsOpenImmersion f₁
inst_5 : IsOpenImmersion f₂
h₁ :
  P (X := pullback (f₁ ≫ e.hom) (f₂ ≫ e.hom)) (Y := pullback ((f₁ ≫ e.hom) ≫ f) ((f₂ ≫ e.hom) ≫ f))
    (pullback.mapDesc (f₁ ≫ e.hom) (f₂ ≫ e.hom) f)
⊢ P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ e.hom ≫ f) (f₂ ≫ e.hom ≫ f)) (pullback.mapDesc f₁ f₂ (e.hom ≫ f))

Tactic:
rw [pullback.mapDesc_comp, P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.cancel_right_of_respectsIso, CategoryTheory.Limits.pullback.mapDesc_comp, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst_1 : IsAffine Z
H :
  ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ Y) (f₂ : U₂ ⟶ Y) [inst : IsAffine U₁] [inst_6 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_2 : IsAffine U₁
inst_3 : IsAffine U₂
inst_4 : IsOpenImmersion f₁
inst_5 : IsOpenImmersion f₂
⊢ P (X := pullback (f₁ ≫ e.hom) (f₂ ≫ e.hom)) (Y := pullback ((f₁ ≫ e.hom) ≫ f) ((f₂ ≫ e.hom) ≫ f))
    (pullback.mapDesc (f₁ ≫ e.hom) (f₂ ≫ e.hom) f)

Tactic:
apply H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst_1 : IsAffine Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_6 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_2 : IsAffine U₁
inst_3 : IsAffine U₂
inst_4 : IsOpenImmersion f₁
inst_5 : IsOpenImmersion f₂
h₂ : P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)
⊢ P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f ≫ e.hom) (f₂ ≫ f ≫ e.hom)) (pullback.mapDesc f₁ f₂ (f ≫ e.hom))

Tactic:
rw [pullback.mapDesc_comp, P.cancel_right_of_respectsIso]

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.cancel_right_of_respectsIso, CategoryTheory.Limits.pullback.mapDesc_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst_1 : IsAffine Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_6 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_2 : IsAffine U₁
inst_3 : IsAffine U₂
inst_4 : IsOpenImmersion f₁
inst_5 : IsOpenImmersion f₂
⊢ P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)

Tactic:
apply H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : 𝒱.I₀
dsimp :
  IsAffine.{u}
    (pullback
      (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰' (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀))))
          i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀).1 ≫
        pullback.snd f (𝒰.f (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀))))
      (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰' (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀))))
          i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀).2 ≫
        pullback.snd f (𝒰.f (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' 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
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : 𝒱.I₀
⊢ IsAffine.{u}
    (pullback
      (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰' (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀))))
          i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀).1 ≫
        pullback.snd f (𝒰.f (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀))))
      (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰' (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀))))
          i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀).2 ≫
        pullback.snd f (𝒰.f (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' 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
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ ∀ (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:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
apply :
  ∀ (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)
⊢ P.diagonal f

Tactic:
apply of_openCover 𝒱

Premises used: AlgebraicGeometry.HasAffineProperty.of_openCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀
j k : (𝒰' i).I₀
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
(Q.cancel_left_of_respectsIso
          ((pullbackDiagonalMapIso _ _ ((𝒰' i).f j) ((𝒰' i).f k)).inv ≫
            pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) _ _)
          (pullback.snd _ _)).mp
      _

Premises used: CategoryTheory.Limits.pullbackDiagonalMapIso, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.map, CategoryTheory.CategoryStruct.comp, Iff.mp, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv, 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
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀
j k : (𝒰' i).I₀
⊢ pullback.diagonal f ≫ 𝟙 (pullback.diagonalObj f) = 𝟙 X ≫ pullback.diagonal f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀
j k : (𝒰' i).I₀
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀
j k : (𝒰' i).I₀
⊢ Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
    pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
      ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
    (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))

Tactic:
h𝒰' i j k