awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this_1 : IsAffineHom f
this_2 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (Iso.op (eqToIso ⋯))) (Functor.mapIso V.presheaf (Iso.op (eqToIso ⋯)))
this_3 :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q (RingHom.comp (RingHom.fst S T) f) → Q (RingHom.comp (RingHom.snd S T) f) → Q f
this : Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.snd = Scheme.Hom.app g W
⊢ Q
    (RingHom.comp (RingHom.snd (↑Γ(U, f ⁻¹ᵁ W) : Type u) (↑Γ(V, g ⁻¹ᵁ W) : Type u))
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          Iso.hom
            (Limits.IsLimit.conePointUniqueUpToIso (Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W)))
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))))))
have h : RingHom.comp (RingHom.snd (↑Γ(U, f ⁻¹ᵁ W) : Type u) (↑Γ(V, g ⁻¹ᵁ W) : Type u))
    (CommRingCat.Hom.hom
      ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
        Iso.hom
          (Limits.IsLimit.conePointUniqueUpToIso (Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W)))
            (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))))) =
  CommRingCat.Hom.hom (Scheme.Hom.app g W)
Tactic: convert! (hg W hW).2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ P f
have refine : ∀ (i : 𝒰.I₀), P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (𝒰.f i)) : Scheme)) (f ∣_ Scheme.Hom.opensRange (𝒰.f i))
Tactic: refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange 𝒰) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
⊢ IsOpenCover.{u, u} (ι := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U))
have h : ∀ (x : ↥Y),
  x ∈ (↑(iSup (ι := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U))) : Set ↥Y) ↔
    x ∈ (↑⊤ : Set ↥Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
⊢ P f
have refine : ∀
  (i :
    (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U))
        sorry).I₀),
  P (X :=
    pullback f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) sorry).f
        i))
    (pullback.snd f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) sorry).f
        i))
Tactic: refine (P.iff_of_zeroHypercover_target
    (Y.openCoverOfIsOpenCover (s := Set.range U) Subtype.val (by ext; simp [← hU]))).mpr fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
i :
  (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U))
      ⋯).I₀
⊢ P (X :=
    pullback f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
        i))
    (pullback.snd f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
        i))
have obtain : ∀ (i : ι),
  P (X :=
    pullback (Y :=
      (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) sorry).X
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) sorry))
      f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) sorry).f
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) sorry)))
    (pullback.snd f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) sorry).f
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) sorry)))
Tactic: obtain ⟨_, i, rfl⟩ := i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
i : ι
⊢ P (X :=
    pullback (Y :=
      (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).X
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯))
      f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯)))
    (pullback.snd f
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯)))
have refine : P (X :=
  (↑(f ⁻¹ᵁ
        Scheme.Hom.opensRange (X :=
          (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
                (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) sorry).X
            (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) sorry))
          ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
                (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) sorry).f
            (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) sorry))) :
    Scheme))
  (f ∣_
    Scheme.Hom.opensRange (X :=
      (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) sorry).X
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) sorry))
      ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) sorry).f
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) sorry)))
Tactic: refine (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
i : ι
⊢ P (X :=
    (↑(f ⁻¹ᵁ
          Scheme.Hom.opensRange (X :=
            (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
                  (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).X
              (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯))
            ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
                  (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
              (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯))) :
      Scheme))
    (f ∣_
      Scheme.Hom.opensRange (X :=
        (Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
              (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).X
          (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯))
        ((Y.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
              (Subtype.val (p := fun (x : Y.Opens) ↦ x ∈ Set.range U)) ⋯).f
          (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Set.range U) (U i) ⋯)))
have change : P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (U i).ι) : Scheme)) (f ∣_ Scheme.Hom.opensRange (U i).ι)
Tactic: change P (f ∣_ (U i).ι.opensRange)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
i : ι
⊢ P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (U i).ι) : Scheme)) (f ∣_ Scheme.Hom.opensRange (U i).ι)
have rw : P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
Tactic: rw [Scheme.Opens.opensRange_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} Y
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    P (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
⊢ P f
have apply : ∀ (i : 𝒰.I₀), P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (𝒰.f i)) : Scheme)) (f ∣_ Scheme.Hom.opensRange (𝒰.f i))
Tactic: apply of_iSup_eq_top (fun i ↦ (𝒰.f i).opensRange) 𝒰.iSup_opensRange
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst_1 : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range (ι := ↥X) ⇑f ⊆ (↑(⨆ (i : ι), U i) : Set ↥Y)
hf : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
g : X ⟶ (↑(⨆ (i : ι), U i) : Scheme) := IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯
⊢ P f
have rw : P (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f sorry ≫ Scheme.Opens.ι (⨆ (i : ι), U i))
Tactic: rw [← IsOpenImmersion.lift_fac (⨆ i, U i).ι f (by simpa using H)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst_1 : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range (ι := ↥X) ⇑f ⊆ (↑(⨆ (i : ι), U i) : Set ↥Y)
hf : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
g : X ⟶ (↑(⨆ (i : ι), U i) : Scheme) := IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯
⊢ P (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯ ≫ Scheme.Opens.ι (⨆ (i : ι), U i))
have hf₁ : P (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f sorry)
Tactic: apply MorphismProperty.RespectsRight.postcomp (Q := @IsOpenImmersion) _ inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst_1 : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range (ι := ↥X) ⇑f ⊆ (↑(⨆ (i : ι), U i) : Set ↥Y)
hf : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
g : X ⟶ (↑(⨆ (i : ι), U i) : Scheme) := IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯
⊢ P (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯)
have hf₁ : ∀ (i : ι),
  P (X :=
    (↑(IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f sorry ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) :
      Scheme))
    (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f sorry ∣_ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i)
Tactic: rw [iff_of_iSup_eq_top (P := P) (U := fun i : ι ↦ (⨆ i, U i).ι ⁻¹ᵁ U i)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst_1 : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range (ι := ↥X) ⇑f ⊆ (↑(⨆ (i : ι), U i) : Set ↥Y)
hf : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
g : X ⟶ (↑(⨆ (i : ι), U i) : Scheme) := IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯
hf₁ :
  ∀ (i : ι),
    P (X :=
      (↑(IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯ ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) :
        Scheme))
      (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯ ∣_ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i)
⊢ P (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯)
have hf₂ : Eq.{u + 1} (α := (↑(⨆ (i : ι), U i) : Scheme).Opens) (⨆ (i : ι), Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) ⊤
Tactic: rw [iff_of_iSup_eq_top (P := P) (U := fun i : ι ↦ (⨆ i, U i).ι ⁻¹ᵁ U i)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst_1 : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range (ι := ↥X) ⇑f ⊆ (↑(⨆ (i : ι), U i) : Set ↥Y)
hf : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
g : X ⟶ (↑(⨆ (i : ι), U i) : Scheme) := IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯
i : ι
⊢ g ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i = f ⁻¹ᵁ U i
have change : (g ≫ Scheme.Opens.ι (⨆ (i : ι), U i)) ⁻¹ᵁ U i = f ⁻¹ᵁ U i
Tactic: change (g ≫ (⨆ i, U i).ι) ⁻¹ᵁ U i = _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst_1 : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range (ι := ↥X) ⇑f ⊆ (↑(⨆ (i : ι), U i) : Set ↥Y)
hf : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
g : X ⟶ (↑(⨆ (i : ι), U i) : Scheme) := IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯
i : ι
⊢ P (X :=
    (↑(IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯ ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) :
      Scheme))
    (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯ ∣_ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i)
have hf₁ : ∀ (heq : g ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i = f ⁻¹ᵁ U i),
  P (X :=
    (↑(IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f sorry ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) :
      Scheme))
    (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f sorry ∣_ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i)
Tactic: have heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i := by
      change (g ≫ (⨆ i, U i).ι) ⁻¹ᵁ U i = _
      simp [g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst_1 : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range (ι := ↥X) ⇑f ⊆ (↑(⨆ (i : ι), U i) : Set ↥Y)
hf : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
g : X ⟶ (↑(⨆ (i : ι), U i) : Scheme) := IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯
i : ι
heq : g ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i = f ⁻¹ᵁ U i
e : Arrow.mk (X := (↑(g ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) : Scheme))
    (g ∣_ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) ≅
  Arrow.mk (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i) :=
  Arrow.isoMk (X.isoOfEq heq) (Scheme.Opens.isoOfLE ⋯) ⋯
⊢ P (X :=
    (↑(IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯ ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) :
      Scheme))
    (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯ ∣_ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i)
have hf₁ : P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
Tactic: rw [P.arrow_mk_iso_iff e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst_1 : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range (ι := ↥X) ⇑f ⊆ (↑(⨆ (i : ι), U i) : Set ↥Y)
hf : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
g : X ⟶ (↑(⨆ (i : ι), U i) : Scheme) := IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯
⊢ Eq.{u + 1} (α := (↑(⨆ (i : ι), U i) : Scheme).Opens) (⨆ (i : ι), Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) ⊤
have hf₁ : Eq.{u + 1} (α := Y.Opens)
  ((fun (x : (↑(⨆ (i : ι), U i) : Scheme).Opens) ↦ Scheme.Opens.ι (⨆ (i : ι), U i) ''ᵁ x)
    (⨆ (i : ι), Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i))
  ((fun (x : (↑(⨆ (i : ι), U i) : Scheme).Opens) ↦ Scheme.Opens.ι (⨆ (i : ι), U i) ''ᵁ x) ⊤)
Tactic: apply (⨆ i, U i).ι.image_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst_1 : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range (ι := ↥X) ⇑f ⊆ (↑(⨆ (i : ι), U i) : Set ↥Y)
hf : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
g : X ⟶ (↑(⨆ (i : ι), U i) : Scheme) := IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯
⊢ Eq.{u + 1} (α := Y.Opens) (Scheme.Opens.ι (⨆ (i : ι), U i) ''ᵁ ⨆ (i : ι), Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i)
    (Scheme.Opens.ι (⨆ (i : ι), U i) ''ᵁ ⊤)
have hf₁ : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), Scheme.Opens.ι (⨆ (i : ι), U i) ''ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i)
  (⨆ (i : ι), U i)
Tactic: rw [Scheme.Hom.image_iSup, Scheme.Hom.image_top_eq_opensRange, Scheme.Opens.opensRange_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥Y), ∃ (U : Y.Opens), x ∈ U ∧ P (f ∣_ U)
⊢ P f
have choose : ∀ (U : (x : ↥Y) → Y.Opens) (hxU : ∀ (x : ↥Y), x ∈ U x) (hU : ∀ (x : ↥Y), P (X := (↑(f ⁻¹ᵁ U x) : Scheme)) (f ∣_ U x)),
  P f
Tactic: choose U hxU hU using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
U : (x : ↥Y) → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), P (X := (↑(f ⁻¹ᵁ U x) : Scheme)) (f ∣_ U x)
⊢ P f
have refine : ∀ (x : ↥Y), Membership.mem (γ := Opens ↥Y) ⊤ x → x ∈ iSup U
Tactic: refine IsZariskiLocalAtTarget.of_iSup_eq_top U (top_le_iff.mp fun x _ ↦ ?_) hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
hX : ∀ (x : ↥X), ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ P ((f ⁻¹ᵁ U).ι ≫ f)
⊢ P f
have choose : ∀ (U : (x : ↥X) → Y.Opens) (h₁ : ∀ (x : ↥X), Membership.mem (α := ↥Y) (U x) (f x : ↥Y))
  (h₂ : ∀ (x : ↥X), P ((f ⁻¹ᵁ U x).ι ≫ f)), P f
Tactic: choose U h₁ h₂ using hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
U : (x : ↥X) → Y.Opens
h₁ : ∀ (x : ↥X), Membership.mem (α := ↥Y) (U x) (f x : ↥Y)
h₂ : ∀ (x : ↥X), P ((f ⁻¹ᵁ U x).ι ≫ f)
⊢ P f
have H : Set.range (ι := ↥X) ⇑f ⊆ (↑(⨆ (i : ↥X), U i) : Set ↥Y)
Tactic: apply IsZariskiLocalAtTarget.of_range_subset_iSup U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
U : (x : ↥X) → Y.Opens
h₁ : ∀ (x : ↥X), Membership.mem (α := ↥Y) (U x) (f x : ↥Y)
h₂ : ∀ (x : ↥X), P ((f ⁻¹ᵁ U x).ι ≫ f)
H : Set.range (ι := ↥X) ⇑f ⊆ (↑(⨆ (i : ↥X), U i) : Set ↥Y)
⊢ P f
have hf : ∀ (i : ↥X), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
Tactic: apply IsZariskiLocalAtTarget.of_range_subset_iSup U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
U : (x : ↥X) → Y.Opens
h₁ : ∀ (x : ↥X), Membership.mem (α := ↥Y) (U x) (f x : ↥Y)
h₂ : ∀ (x : ↥X), P ((f ⁻¹ᵁ U x).ι ≫ f)
x : ↥X
⊢ Membership.mem (α := ↥Y) (↑(⨆ (i : ↥X), U i) : Set ↥Y) (f x : ↥Y)
have H : ∃ (i : ↥X), Membership.mem (α := ↥Y) (U i) (f x : ↥Y)
Tactic: simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (X := X ⨿ Y) (Y := X' ⨿ Y') (coprod.map f g)
have refine : ∀ (i : (coprodOpenCover X' Y').toPreZeroHypercover.1),
  P (X :=
    PreZeroHypercover.X (S := X ⨿ Y)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (coprod.map f g) (coprodOpenCover X' Y')))
      i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) i :
      PreZeroHypercover.X (S := X ⨿ Y)
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (coprod.map f g) (coprodOpenCover X' Y')))
          i ⟶
        (coprodOpenCover X' Y').X i)
Tactic: refine IsZariskiLocalAtTarget.of_openCover (coprodOpenCover.{_, 0} _ _) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (Y := (coprodOpenCover X' Y').X (Sum.inl PUnit.unit))
    (CategoryStruct.comp (Y := pullback (X := X ⨿ Y) (Z := X' ⨿ Y') (coprod.map f g) coprod.inl) (Iso.hom ⋯.isoPullback)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) (Sum.inl PUnit.unit)))
have h : (coprodOpenCover X' Y').X (Sum.inl PUnit.unit) = X' →
  CategoryStruct.comp (Y := pullback (X := X ⨿ Y) (Z := X' ⨿ Y') (coprod.map f g) coprod.inl) (Iso.hom sorry.isoPullback)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) (Sum.inl PUnit.unit)) =
    f
Tactic: convert! hf