awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
x : ↥X
H : ∃ (i : ↥X), Membership.mem (α := ↥Y) (U i) (f x : ↥Y)
⊢ Membership.mem (α := ↥Y) (↑(⨆ (i : ↥X), U i) : Set ↥Y) (f x : ↥Y)

Tactic:
simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe]

Premises used: TopologicalSpace.Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe
-- 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)
x : ↥X
⊢ ∃ (i : ↥X), Membership.mem (α := ↥Y) (U i) (f x : ↥Y)

Tactic:
⟨x, h₁ x⟩

Premises used: Exists.intro
-- 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)
x : ↥X
⊢ ∃ (i : ↥X), Membership.mem (α := ↥Y) (U i) (f x : ↥Y)

Tactic:
exact ⟨x, h₁ 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
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
⊢ P (f ∣_ U x ≫ (U x).ι)

Tactic:
simp [h₂]
-- 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)
x : ↥X
⊢ P (X := (↑(f ⁻¹ᵁ U x) : Scheme)) (f ∣_ U x)

Tactic:
exact P.of_postcomp (f ∣_ U x) (U x).ι (inferInstance : IsOpenImmersion _) (by simp [h₂])

Premises used: inferInstance, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.MorphismProperty.of_postcomp, AlgebraicGeometry.morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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)

Tactic:
IsZariskiLocalAtTarget.of_openCover (coprodOpenCover.{_, 0} _ _) ?_

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_openCover, AlgebraicGeometry.coprodOpenCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
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)
⊢ P (X := X ⨿ Y) (Y := X' ⨿ Y') (coprod.map f g)

Tactic:
refine IsZariskiLocalAtTarget.of_openCover (coprodOpenCover.{_, 0} _ _) ?_

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_openCover, AlgebraicGeometry.coprodOpenCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 f

Tactic:
hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
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 ⋯.isoPullback)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g)
          (Sum.inl PUnit.unit)) =
      f
⊢ 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)))

Tactic:
convert! hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
e_2 : (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 ⋯.isoPullback)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) (Sum.inl PUnit.unit)) =
    f

Tactic:
simp [Scheme.Cover.pullbackHom, coprodOpenCover]

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, AlgebraicGeometry.coprodOpenCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
inr :
  P (Y := (coprodOpenCover X' Y').X (Sum.inr PUnit.unit))
    (CategoryStruct.comp (Y := pullback (X := X ⨿ Y) (Z := X' ⨿ Y') (coprod.map f g) coprod.inr) (Iso.hom ⋯.isoPullback)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit)))
⊢ P (X :=
    PreZeroHypercover.X (S := X ⨿ Y)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (coprod.map f g) (coprodOpenCover X' Y')))
      (Sum.inr PUnit.unit))
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit) :
      PreZeroHypercover.X (S := X ⨿ Y)
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (coprod.map f g) (coprodOpenCover X' Y')))
          (Sum.inr PUnit.unit) ⟶
        (coprodOpenCover X' Y').X (Sum.inr PUnit.unit))

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso P
      (isPullback_inr_inr_coprodMap f g).flip.isoPullback.hom]

Premises used: CategoryTheory.IsPullback.isoPullback, CategoryTheory.IsPullback.flip, AlgebraicGeometry.isPullback_inr_inr_coprodMap, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
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 g

Tactic:
hg
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
h :
  (coprodOpenCover X' Y').X (Sum.inr PUnit.unit) = Y' →
    CategoryStruct.comp (Y := pullback (X := X ⨿ Y) (Z := X' ⨿ Y') (coprod.map f g) coprod.inr) (Iso.hom ⋯.isoPullback)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g)
          (Sum.inr PUnit.unit)) =
      g
⊢ P (Y := (coprodOpenCover X' Y').X (Sum.inr PUnit.unit))
    (CategoryStruct.comp (Y := pullback (X := X ⨿ Y) (Z := X' ⨿ Y') (coprod.map f g) coprod.inr) (Iso.hom ⋯.isoPullback)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit)))

Tactic:
convert! hg
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
e_2 : (coprodOpenCover X' Y').X (Sum.inr PUnit.unit) = Y'
⊢ CategoryStruct.comp (Y := pullback (X := X ⨿ Y) (Z := X' ⨿ Y') (coprod.map f g) coprod.inr) (Iso.hom ⋯.isoPullback)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit)) =
    g

Tactic:
simp [Scheme.Cover.pullbackHom, coprodOpenCover]

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, AlgebraicGeometry.coprodOpenCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
i : 𝒰.I₀
H : P f
rw : P ((Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)
⊢ P (𝒰.f i ≫ f)

Tactic:
rw [← IsOpenImmersion.isoOfRangeEq_hom_fac (𝒰.f i) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
      P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.Scheme.Opens.opensRange_ι, TopologicalSpace.Opens.carrier, congr_arg, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, Eq.symm, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
i : 𝒰.I₀
H : P f
⊢ P ((Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)

Tactic:
restrict _ _ H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
i : 𝒰.I₀
H : P f
⊢ P ((Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)

Tactic:
exact restrict _ _ H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f

Tactic:
of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange 𝒰) fun i ↦ ?_

Premises used: AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
refine : ∀ (i : 𝒰.I₀), P ((Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)
⊢ P f

Tactic:
refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange 𝒰) fun i ↦ ?_

Premises used: AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
rw : P (𝒰.f i ≫ f)
⊢ P ((Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)

Tactic:
rw [← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f i) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
      P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.Scheme.Opens.opensRange_ι, TopologicalSpace.Opens.carrier, congr_arg, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, Eq.symm, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)

Tactic:
h _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)

Tactic:
exact h _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
UX : Scheme
H : P f
i : UX ⟶ X
inst_1 : IsOpenImmersion i
⊢ P (i ≫ f)

Tactic:
(P.iff_of_zeroHypercover_source (X.affineCover.add i)).mp H .none

Premises used: AlgebraicGeometry.Scheme.Cover.add, CategoryTheory.MorphismProperty.iff_of_zeroHypercover_source, Option.none, Iff.mp, AlgebraicGeometry.Scheme.affineCover, Sum.elim
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
h :
  ∀ (x : ↥X),
    x ∈ (↑(iSup (ι := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))) : Set ↥X) ↔
      x ∈ (↑⊤ : Set ↥X)
⊢ IsOpenCover.{u, u} (ι := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
x : ↥X
⊢ x ∈ (↑(iSup (ι := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))) : Set ↥X) ↔
    x ∈ (↑⊤ : Set ↥X)

Tactic:
simp [← hU]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
refine :
  ∀
    (i :
      (X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
          (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U)) ⋯).I₀),
    P
      ((X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
              (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U)) ⋯).f
          i ≫
        f)
⊢ P f

Tactic:
refine (P.iff_of_zeroHypercover_source
    (X.openCoverOfIsOpenCover (s := Set.range U) Subtype.val (by ext; simp [← hU]))).mpr fun i ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, CategoryTheory.MorphismProperty.iff_of_zeroHypercover_source, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i :
  (X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
      ⋯).I₀
obtain :
  ∀ (i : ι),
    P (X :=
      (X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
            (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U)) ⋯).X
        (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ Set.range U) (U i) ⋯))
      ((X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u))
              (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U)) ⋯).f
          (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ Set.range U) (U i) ⋯) ≫
        f)
⊢ P
    ((X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
            ⋯).f
        i ≫
      f)

Tactic:
obtain ⟨_, i, rfl⟩ := i

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i : ι
⊢ P (X :=
    (X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
          ⋯).X
      (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ Set.range U) (U i) ⋯))
    ((X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
            ⋯).f
        (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ Set.range U) (U i) ⋯) ≫
      f)

Tactic:
H i

Premises used: Set.Mem, AlgebraicGeometry.Scheme.restrict, AlgebraicGeometry.Scheme.Opens.toScheme
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i : ι
⊢ P (X :=
    (X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
          ⋯).X
      (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ Set.range U) (U i) ⋯))
    ((X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
            ⋯).f
        (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ Set.range U) (U i) ⋯) ≫
      f)

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

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

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.of_iSup_eq_top, Iff.intro, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f

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

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.IsZariskiLocalAtSource.of_iSup_eq_top, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
refine :
  ∀ (i : 𝒰.I₀),
    P (X := (↑((fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)) i) : Scheme))
      (Scheme.Opens.ι ((fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)) i) ≫ f)
⊢ P f

Tactic:
refine of_iSup_eq_top (fun i ↦ (𝒰.f i).opensRange) 𝒰.iSup_opensRange fun i ↦ ?_

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.IsZariskiLocalAtSource.of_iSup_eq_top, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
rw : P (𝒰.f i ≫ f)
⊢ P (X := (↑((fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)) i) : Scheme))
    (Scheme.Opens.ι ((fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)) i) ≫ f)

Tactic:
rw [← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f i) (Scheme.Opens.ι _)
    (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
    P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.Scheme.Opens.opensRange_ι, TopologicalSpace.Opens.carrier, congr_arg, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, Eq.symm, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)

Tactic:
H i
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)

Tactic:
exact H i
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
⊢ P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)

Tactic:
⟨fun H _ ↦ comp H _, of_openCover _⟩

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsZariskiLocalAtSource.of_openCover, Iff.intro, AlgebraicGeometry.IsZariskiLocalAtSource.comp, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : P.ContainsIdentities
inst_2 : IsOpenImmersion f
⊢ P f

Tactic:
Category.comp_id f ▸ comp (P.id_mem Y) f

Premises used: Eq.rec, CategoryTheory.Category.comp_id, CategoryTheory.MorphismProperty.id_mem, AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
i : 𝒰.I₀
hf : P f
apply : P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i) ≫ 𝒰.f i)
⊢ P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))

Tactic:
apply hP _ (𝒰.f i)

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
i : 𝒰.I₀
hf : P f
rw : P (X := pullback f (𝒰.f i)) (pullback.fst f (𝒰.f i) ≫ f)
⊢ P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i) ≫ 𝒰.f i)

Tactic:
rw [← pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition