awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
this : IsAffine.{u_1} (↑(e.hom ⁻¹ᵁ U) : Scheme)
⊢ P ((f ≫ e.hom) ∣_ U)
have hpostcomp : P (X := (↑((Opens.map f.base).obj ((Opens.map e.hom.base).obj U)) : Scheme)) (f ∣_ e.hom ⁻¹ᵁ U)
Tactic: rw [morphismRestrict_comp, P.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
⊢ P = targetAffineLocally (AffineTargetMorphismProperty.of P)
have h : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y), P f ↔ targetAffineLocally (AffineTargetMorphismProperty.of P) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ targetAffineLocally (AffineTargetMorphismProperty.of P) f
have h : P f → targetAffineLocally (AffineTargetMorphismProperty.of P) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
h : P f → targetAffineLocally (AffineTargetMorphismProperty.of P) f
⊢ P f ↔ targetAffineLocally (AffineTargetMorphismProperty.of P) f
have h₁ : targetAffineLocally (AffineTargetMorphismProperty.of P) f → P f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : P f
⊢ targetAffineLocally (AffineTargetMorphismProperty.of P) f
have h : ∀ (U : Y.Opens) (hU : U ∈ Y.affineOpens),
  AffineTargetMorphismProperty.of P (X :=
    (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme))
    (f ∣_ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens))
Tactic: ⟨U, hU⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ P.RespectsIso
have rw : (targetAffineLocally Q).RespectsIso
Tactic: rw [eq_targetAffineLocally P]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))
this : Q.IsLocal := ⋯
⊢ P f
have rw : targetAffineLocally Q f
Tactic: rw [eq_targetAffineLocally P]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U_1 : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U_1 i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U_1 i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U_1 i) : Y.Opens))
this : Q.IsLocal := ⋯
U : (↑Y.affineOpens : Type u)
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
h : Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
⊢ Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen r) : Y.Opens)) : Scheme)) (f ∣_ (↑(Y.affineBasicOpen r) : Y.Opens))
have basicOpen : ∀
  (this :
    Q (X :=
      (↑((f ∣_ (↑U : Y.Opens)) ⁻¹ᵁ
            (↑(↑U : Y.Opens) : Scheme).basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (↑U : Y.Opens).topIso.inv :
                  (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                r)) :
        Scheme))
      (f ∣_ (↑U : Y.Opens) ∣_
        (↑(↑U : Y.Opens) : Scheme).basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (↑U : Y.Opens).topIso.inv :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
            r))),
  Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen r) : Y.Opens)) : Scheme)) (f ∣_ (↑(Y.affineBasicOpen r) : Y.Opens))
Tactic: have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U_1 : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U_1 i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U_1 i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U_1 i) : Y.Opens))
this : Q.IsLocal := ⋯
U : (↑Y.affineOpens : Type u)
s : Finset (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, (↑U : Y.Opens)) : Type u))) ⊤
H :
  ∀ (f_1 : ↥s),
    Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens)) : Scheme))
      (f ∣_ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens))
⊢ Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
have openCover : ∀
  (r :
    ↥(Finset.image
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (↑U : Y.Opens).topIso.inv) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
        s)),
  Q (X :=
    (↑((f ∣_ (↑U : Y.Opens)) ⁻¹ᵁ
          (↑(↑U : Y.Opens) : Scheme).basicOpen (↑r : (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))) :
      Scheme))
    (f ∣_ (↑U : Y.Opens) ∣_ (↑(↑U : Y.Opens) : Scheme).basicOpen (↑r : (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)))
Tactic: apply AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _
      (s.image (Scheme.Opens.topIso _).inv) (by simp [← Ideal.map_span, hs, Ideal.map_top])
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))
this : Q.IsLocal := ⋯
V : (↑Y.affineOpens : Type u)
⊢ Q (X := (↑(f ⁻¹ᵁ (↑V : Y.Opens)) : Scheme)) (f ∣_ (↑V : Y.Opens))
have basicOpen : ∀ (U : (↑Y.affineOpens : Type u)) (r : (↑Γ(Y, (↑U : Y.Opens)) : Type u))
  (h : Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))),
  Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen r) : Y.Opens)) : Scheme)) (f ∣_ (↑(Y.affineBasicOpen r) : Y.Opens))
Tactic: induction V using of_affine_open_cover U hU with
  | basicOpen U r h =>
    have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r)).mp this
  | openCover U s hs H =>
    apply AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _
      (s.image (Scheme.Opens.topIso _).inv) (by simp [← Ideal.map_span, hs, Ideal.map_top])
    intro ⟨r, hr⟩
    obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)
  | hU i => exact hU' i
Cleared hypotheses: V
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))
this : Q.IsLocal := ⋯
V : (↑Y.affineOpens : Type u)
basicOpen :
  ∀ (U : (↑Y.affineOpens : Type u)) (r : (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (h : Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))),
    Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen r) : Y.Opens)) : Scheme)) (f ∣_ (↑(Y.affineBasicOpen r) : Y.Opens))
⊢ Q (X := (↑(f ⁻¹ᵁ (↑V : Y.Opens)) : Scheme)) (f ∣_ (↑V : Y.Opens))
have openCover : ∀ (U : (↑Y.affineOpens : Type u)) (s : Finset (↑Γ(Y, (↑U : Y.Opens)) : Type u))
  (hs : Eq (α := Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, (↑U : Y.Opens)) : Type u))) ⊤)
  (H :
    ∀ (f_1 : ↥s),
      Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens)) : Scheme))
        (f ∣_ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens))),
  Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
Tactic: induction V using of_affine_open_cover U hU with
  | basicOpen U r h =>
    have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r)).mp this
  | openCover U s hs H =>
    apply AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _
      (s.image (Scheme.Opens.topIso _).inv) (by simp [← Ideal.map_span, hs, Ideal.map_top])
    intro ⟨r, hr⟩
    obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)
  | hU i => exact hU' i
Cleared hypotheses: V
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))
this : Q.IsLocal := ⋯
⊢ targetAffineLocally Q f
have intro : ∀ (V : (↑Y.affineOpens : Type u)), Q (X := (↑(f ⁻¹ᵁ (↑V : Y.Opens)) : Scheme)) (f ∣_ (↑V : Y.Opens))
Tactic: classical
  intro V
  induction V using of_affine_open_cover U hU with
  | basicOpen U r h =>
    have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r)).mp this
  | openCover U s hs H =>
    apply AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _
      (s.image (Scheme.Opens.topIso _).inv) (by simp [← Ideal.map_span, hs, Ideal.map_top])
    intro ⟨r, hr⟩
    obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)
  | hU i => exact hU' i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
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)
this : Q.IsLocal := ⋯
⊢ P f ↔
    ∀ (i : 𝒰.toPreZeroHypercover.1),
      Q (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
have rw : (∀ (i : 𝒰.I₀),
    Q (X :=
      (↑(f ⁻¹ᵁ
            (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) sorry) : Y.Opens)) :
        Scheme))
      (f ∣_ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) sorry) : Y.Opens))) ↔
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    Q (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
Tactic: rw [iff_of_iSup_eq_top (P := P)
    (fun i ↦ ⟨_, isAffineOpen_opensRange _⟩) 𝒰.iSup_opensRange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
⊢ P f ↔ Q f
have rw : (∀
    (i :
      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
          (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).1),
    Q (X :=
      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
        i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)) f i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
            i ⟶
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).X
            i)) ↔
  Q f
Tactic: rw [iff_of_openCover (P := P) (Scheme.coverOfIsIso.{0} (𝟙 Y))]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
⊢ (∀
      (i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).1),
      Q (X :=
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
              (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
          i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)) f i :
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
              i ⟶
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).X
              i)) ↔
    Q f
have trans : (∀
    (i :
      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
          (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).1),
    Q (X :=
      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
        i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)) f i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
            i ⟶
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).X
            i)) ↔
  Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))
Tactic: trans Q (pullback.snd f (𝟙 _))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
trans :
  (∀
      (i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).1),
      Q (X :=
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
              (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
          i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)) f i :
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
              i ⟶
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).X
              i)) ↔
    Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))
⊢ (∀
      (i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).1),
      Q (X :=
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
              (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
          i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)) f i :
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
              i ⟶
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).X
              i)) ↔
    Q f
have trans₁ : Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y)) ↔ Q f
Tactic: trans Q (pullback.snd f (𝟙 _))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
⊢ Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y)) ↔ Q f
have rw : Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y) ≫ 𝟙 Y) ↔ Q f
Tactic: rw [← Category.comp_id (pullback.snd _ _), ← pullback.condition,
    Q.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
rw : Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y) ≫ 𝟙 Y) ↔ Q f
⊢ Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y)) ↔ Q f
have rw₁ : Q (X := pullback f (𝟙 Y)) (pullback.fst f (𝟙 Y) ≫ f) ↔ Q f
Tactic: rw [← Category.comp_id (pullback.snd _ _), ← pullback.condition,
    Q.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
rw : Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y) ≫ 𝟙 Y) ↔ Q f
rw₁ : Q (X := pullback f (𝟙 Y)) (pullback.fst f (𝟙 Y) ≫ f) ↔ Q f
⊢ Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y)) ↔ Q f
have rw₂ : Q f ↔ Q f
Tactic: rw [← Category.comp_id (pullback.snd _ _), ← pullback.condition,
    Q.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ IsZariskiLocalAtTarget P
have restrict : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
Tactic: apply IsZariskiLocalAtTarget.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
restrict : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
⊢ IsZariskiLocalAtTarget P
have of_sSup_eq_top : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Y.Opens),
  iSup U = ⊤ → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
Tactic: apply IsZariskiLocalAtTarget.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
have restrict : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : Y.Opens), targetAffineLocally Q f → targetAffineLocally Q (f ∣_ U)
Tactic: rw [eq_targetAffineLocally P]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
H : targetAffineLocally Q f
V : (↑(↑U : Scheme).affineOpens : Type u_1)
⊢ Q (X := (↑((f ∣_ U) ⁻¹ᵁ (↑V : (↑U : Scheme).Opens)) : Scheme)) (f ∣_ U ∣_ (↑V : (↑U : Scheme).Opens))
have restrict : Q (X := (↑(f ⁻¹ᵁ U.ι ''ᵁ (↑V : (↑U : Scheme).Opens)) : Scheme)) (f ∣_ U.ι ''ᵁ (↑V : (↑U : Scheme).Opens))
Tactic: rw [Q.arrow_mk_iso_iff (morphismRestrictRestrict f _ _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
⊢ P f
have of_sSup_eq_top : ∀ (i : 𝒰.affineRefinement.openCover.toPreZeroHypercover.1),
  Q (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰.affineRefinement.openCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).X i ⟶ 𝒰.affineRefinement.openCover.X i)
Tactic: apply of_openCover 𝒰.affineRefinement.openCover
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
    ((fun (i : 𝒰.I₀) ↦
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
          PreZeroHypercover (𝒰.X i)))
      i)
⊢ P (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
have refine : U i = Scheme.Hom.opensRange (𝒰.f i)
Tactic: refine (P.arrow_mk_iso_iff
        (morphismRestrictEq _ ?_ ≪≫ morphismRestrictOpensRange f (𝒰.f i))).mp (H i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
this : Q.IsLocal := ⋯
⊢ P (X := pullback f g) (pullback.fst f g)
have rw : ∀ (i : X.affineCover.toPreZeroHypercover.1),
  Q (X :=
    PreZeroHypercover.X (S := pullback f g)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
      i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i :
      PreZeroHypercover.X (S := pullback f g)
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
          i ⟶
        X.affineCover.X i)
Tactic: rw [iff_of_openCover (P := P) X.affineCover]