awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 : ι
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)) ⋯).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) ⋯)))
⊢ 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) ⋯)))

Tactic:
refine (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mp ?_

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictOpensRange, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 : ι
change : P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (U i).ι) : Scheme)) (f ∣_ Scheme.Hom.opensRange (U 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) ⋯)))

Tactic:
change P (f ∣_ (U i).ι.opensRange)

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 : ι
rw : P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
⊢ P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (U i).ι) : Scheme)) (f ∣_ Scheme.Hom.opensRange (U i).ι)

Tactic:
rw [Scheme.Opens.opensRange_ι]

Premises used: AlgebraicGeometry.Scheme.Opens.opensRange_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)

Tactic:
H i
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)

Tactic:
exact H i
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
⊢ P f ↔ ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)

Tactic:
⟨fun H _ ↦ restrict H _, of_iSup_eq_top U hU⟩

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_top, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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)
apply : ∀ (i : 𝒰.I₀), P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (𝒰.f i)) : Scheme)) (f ∣_ Scheme.Hom.opensRange (𝒰.f i))
⊢ P f

Tactic:
apply of_iSup_eq_top (fun i ↦ (𝒰.f i).opensRange) 𝒰.iSup_opensRange

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_top, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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)
⊢ ∀ (i : 𝒰.I₀), P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (𝒰.f i)) : Scheme)) (f ∣_ Scheme.Hom.opensRange (𝒰.f i))

Tactic:
fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (H i)

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictOpensRange, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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)
⊢ ∀ (i : 𝒰.I₀), P (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange (𝒰.f i)) : Scheme)) (f ∣_ Scheme.Hom.opensRange (𝒰.f i))

Tactic:
exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (H i)

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictOpensRange, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} Y
⊢ P f ↔
    ∀ (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)

Tactic:
⟨fun H _ ↦ of_isPullback (.of_hasPullback _ _) H, of_openCover _⟩

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, Iff.intro, CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.IsZariskiLocalAtTarget.of_openCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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)
⊢ Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f)
    (Set.range (ι := ↥(↑(⨆ (i : ι), U i) : Scheme)) ⇑(Scheme.Opens.ι (⨆ (i : ι), U i)))

Tactic:
simpa using H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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)
let : P f
⊢ P f

Tactic:
let g : X ⟶ (⨆ i, U i : Y.Opens) := IsOpenImmersion.lift (Scheme.Opens.ι _) f (by simpa using H)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 ⋯
⊢ Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f)
    (Set.range (ι := ↥(↑(⨆ (i : ι), U i) : Scheme)) ⇑(Scheme.Opens.ι (⨆ (i : ι), U i)))

Tactic:
simpa using H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 ⋯
rw : P (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯ ≫ Scheme.Opens.ι (⨆ (i : ι), U i))
⊢ P f

Tactic:
rw [← IsOpenImmersion.lift_fac (⨆ i, U i).ι f (by simpa using H)]

Premises used: iSup, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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₁ : P (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯)
⊢ P (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯ ≫ Scheme.Opens.ι (⨆ (i : ι), U i))

Tactic:
apply MorphismProperty.RespectsRight.postcomp (Q := @IsOpenImmersion) _ inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.RespectsRight.postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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)
hf₂ : Eq.{u + 1} (α := (↑(⨆ (i : ι), U i) : Scheme).Opens) (⨆ (i : ι), Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) ⊤
⊢ P (IsOpenImmersion.lift (Scheme.Opens.ι (⨆ (i : ι), U i)) f ⋯)

Tactic:
rw [iff_of_iSup_eq_top (P := P) (U := fun i : ι ↦ (⨆ i, U i).ι ⁻¹ᵁ U i)]

Premises used: iSup, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 : ι
change : (g ≫ Scheme.Opens.ι (⨆ (i : ι), U i)) ⁻¹ᵁ U i = f ⁻¹ᵁ U i
⊢ g ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i = f ⁻¹ᵁ U i

Tactic:
change (g ≫ (⨆ i, U i).ι) ⁻¹ᵁ U i = _

Premises used: iSup, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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

Tactic:
simp [g]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 : ι
hf₁ :
  ∀ (heq : g ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i = f ⁻¹ᵁ U 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 (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)

Tactic:
have heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i := by
      change (g ≫ (⨆ i, U i).ι) ⁻¹ᵁ U i = _
      simp [g]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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
⊢ (X.isoOfEq heq).hom ≫ (Arrow.mk (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)).hom =
    (Arrow.mk (X := (↑(g ⁻¹ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) : Scheme))
          (g ∣_ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i)).hom ≫
      (Scheme.Opens.isoOfLE ⋯).hom

Tactic:
simp [← CategoryTheory.cancel_mono (U i).ι, g]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 ⋯) ⋯
hf₁ : P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U 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)

Tactic:
rw [P.arrow_mk_iso_iff e]

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)

Tactic:
hf i
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)

Tactic:
exact hf i
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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₁ :
  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) ⊤)
⊢ Eq.{u + 1} (α := (↑(⨆ (i : ι), U i) : Scheme).Opens) (⨆ (i : ι), Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i) ⊤

Tactic:
apply (⨆ i, U i).ι.image_injective

Premises used: iSup, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Hom.image_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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₁ :
  Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), Scheme.Opens.ι (⨆ (i : ι), U i) ''ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i)
    (⨆ (i : ι), U i)
⊢ Eq.{u + 1} (α := Y.Opens) (Scheme.Opens.ι (⨆ (i : ι), U i) ''ᵁ ⨆ (i : ι), Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i)
    (Scheme.Opens.ι (⨆ (i : ι), U i) ''ᵁ ⊤)

Tactic:
rw [Scheme.Hom.image_iSup, Scheme.Hom.image_top_eq_opensRange, Scheme.Opens.opensRange_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, AlgebraicGeometry.Scheme.Opens.opensRange_ι, AlgebraicGeometry.Scheme.Hom.image_iSup
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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) (⨆ (i : ι), Scheme.Opens.ι (⨆ (i : ι), U i) ''ᵁ Scheme.Opens.ι (⨆ (i : ι), U i) ⁻¹ᵁ U i)
    (⨆ (i : ι), U i)

Tactic:
simp [Scheme.Hom.image_preimage_eq_opensRange_inf, le_iSup U]

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, le_iSup
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥Y), ∃ (U : Y.Opens), x ∈ U ∧ P (f ∣_ U)
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
⊢ P f

Tactic:
choose U hxU hU using H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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

Tactic:
IsZariskiLocalAtTarget.of_iSup_eq_top U (top_le_iff.mp fun x _ ↦ ?_) hU

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_top, top_le_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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)
refine : ∀ (x : ↥Y), Membership.mem (γ := Opens ↥Y) ⊤ x → x ∈ iSup U
⊢ P f

Tactic:
refine IsZariskiLocalAtTarget.of_iSup_eq_top U (top_le_iff.mp fun x _ ↦ ?_) hU

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_top, top_le_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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)
x : ↥Y
h : Membership.mem (γ := Opens ↥Y) ⊤ x
⊢ x ∈ iSup U

Tactic:
simpa using ⟨x, hxU x⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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)
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
⊢ P f

Tactic:
choose U h₁ h₂ using hX
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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)
hf : ∀ (i : ↥X), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
⊢ P f

Tactic:
apply IsZariskiLocalAtTarget.of_range_subset_iSup U

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_range_subset_iSup