awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
exact hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
refine_2 : P (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ P.diagonal f

Tactic:
change P _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
⊢ P (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
IsZariskiLocalAtSource.of_iSup_eq_top U hU fun i ↦ ?_

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
refine_2 : ∀ (i : ι), P (Y := pullback.diagonalObj f) ((U i).ι ≫ pullback.diagonal f)
⊢ P (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
refine IsZariskiLocalAtSource.of_iSup_eq_top U hU fun i ↦ ?_

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
i : ι
refine_2 :
  P (Y := pullback.diagonalObj f)
    (CategoryStruct.comp (Y := pullback.diagonalObj ((U i).ι ≫ f)) (pullback.diagonal ((U i).ι ≫ f))
      (pullback.map ((U i).ι ≫ f) ((U i).ι ≫ f) f f (U i).ι (U i).ι (𝟙 Y) ⋯ ⋯))
⊢ P (Y := pullback.diagonalObj f) ((U i).ι ≫ pullback.diagonal f)

Tactic:
rw [pullback.comp_diagonal]

Premises used: CategoryTheory.Limits.pullback.comp_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
i : ι
⊢ P (Y := pullback.diagonalObj f)
    (CategoryStruct.comp (Y := pullback.diagonalObj ((U i).ι ≫ f)) (pullback.diagonal ((U i).ι ≫ f))
      (pullback.map ((U i).ι ≫ f) ((U i).ι ≫ f) f f (U i).ι (U i).ι (𝟙 Y) ⋯ ⋯))

Tactic:
RespectsRight.postcomp (P := P) (Q := @IsOpenImmersion) (g _ _) inferInstance _ (hf i)

Premises used: inferInstance, CategoryTheory.MorphismProperty.RespectsRight.postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : P.HasOfPostcompProperty IsOpenImmersion
inst_1 : P.RespectsRight IsOpenImmersion
inst_2 : IsZariskiLocalAtSource P
g : {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : X.Opens) ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
i : ι
⊢ P (Y := pullback.diagonalObj f)
    (CategoryStruct.comp (Y := pullback.diagonalObj ((U i).ι ≫ f)) (pullback.diagonal ((U i).ι ≫ f))
      (pullback.map ((U i).ι ≫ f) ((U i).ι ≫ f) f f (U i).ι (U i).ι (𝟙 Y) ⋯ ⋯))

Tactic:
exact RespectsRight.postcomp (P := P) (Q := @IsOpenImmersion) (g _ _) inferInstance _ (hf i)

Premises used: inferInstance, CategoryTheory.MorphismProperty.RespectsRight.postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P.universally f → P.universally (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ → (∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P.universally f
⊢ IsZariskiLocalAtTarget.{u} P.universally

Tactic:
apply IsZariskiLocalAtTarget.mk'

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.mk'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
⊢ ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P.universally f → P.universally (f ∣_ U)

Tactic:
fun {X Y} f U => P.universally.of_isPullback
      (isPullback_morphismRestrict f U).flip

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.IsPullback.flip, AlgebraicGeometry.isPullback_morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
⊢ ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P.universally f → P.universally (f ∣_ U)

Tactic:
exact fun {X Y} f U => P.universally.of_isPullback
      (isPullback_morphismRestrict f U).flip

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.IsPullback.flip, AlgebraicGeometry.isPullback_morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
of_sSup_eq_top : IsOpenCover (X := ↥Y') fun (i : ι) ↦ i₂ ⁻¹ᵁ U i
of_sSup_eq_top₁ : ∀ (i : ι), P (X := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i)
⊢ P f'

Tactic:
apply hP₂ _ (fun i ↦ i₂ ⁻¹ᵁ U i)

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
of_sSup_eq_top : ∀ (hU : ⊤ ≤ iSup U), LE.le.{u} (α := Opens ↥Y') ⊤ (⨆ (i : ι), i₂ ⁻¹ᵁ U i)
⊢ IsOpenCover (X := ↥Y') fun (i : ι) ↦ i₂ ⁻¹ᵁ U i

Tactic:
simp only [IsOpenCover, ← top_le_iff] at hU ⊢

Premises used: TopologicalSpace.IsOpenCover, top_le_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
hU : ⊤ ≤ iSup U
x : ↥Y'
⊢ Membership.mem (γ := Opens ↥Y') (⨆ (i : ι), i₂ ⁻¹ᵁ U i) x

Tactic:
simpa using @hU (i₂ x) trivial

Premises used: trivial
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ P (X := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i)

Tactic:
H _ ((X'.isoOfEq ?_).hom ≫ i₁ ∣_ _) (i₂ ∣_ _) _ ?_

Premises used: AlgebraicGeometry.Scheme.isoOfEq, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, AlgebraicGeometry.morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
of_sSup_eq_top : f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i = i₁ ⁻¹ᵁ f ⁻¹ᵁ U i
of_sSup_eq_top₁ :
  IsPullback (P := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i) (Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i)
    (i₂ ∣_ U i) (f ∣_ U i)
⊢ P (X := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i)

Tactic:
refine H _ ((X'.isoOfEq ?_).hom ≫ i₁ ∣_ _) (i₂ ∣_ _) _ ?_

Premises used: AlgebraicGeometry.Scheme.isoOfEq, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, AlgebraicGeometry.morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i = i₁ ⁻¹ᵁ f ⁻¹ᵁ U i

Tactic:
congr($(h.1.1) ⁻¹ᵁ U i)

Premises used: congrArg, id, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i = i₁ ⁻¹ᵁ f ⁻¹ᵁ U i

Tactic:
exact congr($(h.1.1) ⁻¹ᵁ U i)

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
of_sSup_eq_top :
  IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) ((Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ (f ⁻¹ᵁ U i).ι) (i₂ ∣_ U i ≫ (U i).ι) f
of_sSup_eq_top₁ :
  Eq (α := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme) ⟶ (↑(U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i ≫ i₂ ∣_ U i)
    ((Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ f ∣_ U i)
⊢ IsPullback (P := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i) (Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i)
    (i₂ ∣_ U i) (f ∣_ U i)

Tactic:
rw [← (isPullback_morphismRestrict f _).paste_vert_iff]

Premises used: CategoryTheory.IsPullback.paste_vert_iff, AlgebraicGeometry.isPullback_morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
of_sSup_eq_top : IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) ((f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i).ι ≫ i₁) ((i₂ ⁻¹ᵁ U i).ι ≫ i₂) f
⊢ IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) ((Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ (f ⁻¹ᵁ U i).ι) (i₂ ∣_ U i ≫ (U i).ι) f

Tactic:
simp only [Category.assoc, morphismRestrict_ι, Scheme.isoOfEq_hom_ι_assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.isoOfEq_hom_ι_assoc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) ((f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i).ι ≫ i₁) ((i₂ ⁻¹ᵁ U i).ι ≫ i₂) f

Tactic:
(isPullback_morphismRestrict f' (i₂ ⁻¹ᵁ U i)).paste_vert h

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.IsPullback.paste_vert, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) ((f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i).ι ≫ i₁) ((i₂ ⁻¹ᵁ U i).ι ≫ i₂) f

Tactic:
exact (isPullback_morphismRestrict f' (i₂ ⁻¹ᵁ U i)).paste_vert h

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.IsPullback.paste_vert, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
of_sSup_eq_top :
  (f' ∣_ i₂ ⁻¹ᵁ U i ≫ i₂ ∣_ U i) ≫ (U i).ι = ((Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ f ∣_ U i) ≫ (U i).ι
⊢ Eq (α := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme) ⟶ (↑(U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i ≫ i₂ ∣_ U i)
    ((Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ f ∣_ U i)

Tactic:
rw [← cancel_mono (Scheme.Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ (f' ∣_ i₂ ⁻¹ᵁ U i ≫ i₂ ∣_ U i) ≫ (U i).ι = ((Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ f ∣_ U i) ≫ (U i).ι

Tactic:
simp [morphismRestrict_ι_assoc, h.1.1]

Premises used: AlgebraicGeometry.morphismRestrict_ι_assoc, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
⊢ IsZariskiLocalAtSource.{u_1} P.universally

Tactic:
.mk_of_iff ?_

Premises used: CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
refine :
  ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X),
    P.universally f ↔ ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
⊢ IsZariskiLocalAtSource.{u_1} P.universally

Tactic:
refine .mk_of_iff ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
⊢ P.universally f ↔ ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)

Tactic:
⟨fun hf i ↦ ?_, fun hf ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
refine_1 : ∀ (hf : P.universally f) (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
refine_2 : ∀ (hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)), P.universally f
⊢ P.universally f ↔ ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)

Tactic:
refine ⟨fun hf i ↦ ?_, fun hf ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
refine_1 :
  ∀ {T : Scheme.{u_1}} (f_1 : T ⟶ Y) [inst : HasPullback f_1 (𝒰.f i ≫ f)],
    P (X := pullback f_1 (𝒰.f i ≫ f)) (pullback.fst f_1 (𝒰.f i ≫ f))
⊢ P.universally (𝒰.f i ≫ f)

Tactic:
apply MorphismProperty.universally_mk'

Premises used: CategoryTheory.MorphismProperty.universally_mk'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
refine_1 : ∀ [inst : HasPullback g (𝒰.f i ≫ f)], P (X := pullback g (𝒰.f i ≫ f)) (pullback.fst g (𝒰.f i ≫ f))
⊢ ∀ [inst : HasPullback g (𝒰.f i ≫ f)], P (X := pullback g (𝒰.f i ≫ f)) (pullback.fst g (𝒰.f i ≫ f))

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
inst_1 : HasPullback g (𝒰.f i ≫ f)
refine_1 :
  P (X := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
    (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ pullback.fst g f)
⊢ P (X := pullback g (𝒰.f i ≫ f)) (pullback.fst g (𝒰.f i ≫ f))

Tactic:
rw [← P.cancel_left_of_respectsIso (pullbackLeftPullbackSndIso g f _).hom,
      pullbackLeftPullbackSndIso_hom_fst]

Premises used: CategoryTheory.Limits.pullbackLeftPullbackSndIso, CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
inst_1 : HasPullback g (𝒰.f i ≫ f)
⊢ P (X := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
    (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ pullback.fst g f)

Tactic:
IsZariskiLocalAtSource.comp (hf _ _ _ (IsPullback.of_hasPullback ..)) _

Premises used: CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
inst_1 : HasPullback g (𝒰.f i ≫ f)
⊢ P (X := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
    (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ pullback.fst g f)

Tactic:
exact IsZariskiLocalAtSource.comp (hf _ _ _ (IsPullback.of_hasPullback ..)) _

Premises used: CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
refine_2 : ∀ {T : Scheme.{u_1}} (f_1 : T ⟶ Y) [inst : HasPullback f_1 f], P (X := pullback f_1 f) (pullback.fst f_1 f)
⊢ P.universally f

Tactic:
apply MorphismProperty.universally_mk'

Premises used: CategoryTheory.MorphismProperty.universally_mk'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
g : T ⟶ Y
refine_2 : ∀ [inst : HasPullback g f], P (X := pullback g f) (pullback.fst g f)
⊢ ∀ [inst : HasPullback g f], P (X := pullback g f) (pullback.fst g f)

Tactic:
_