awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))
this : Q.IsLocal := ⋯
i : ι
⊢ Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))

Tactic:
exact hU' i
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))
this : Q.IsLocal := ⋯
V : (↑Y.affineOpens : Type u)
basicOpen :
  ∀ (U : (↑Y.affineOpens : Type u)) (r : (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (h : Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))),
    Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen r) : Y.Opens)) : Scheme)) (f ∣_ (↑(Y.affineBasicOpen r) : Y.Opens))
openCover :
  ∀ (U : (↑Y.affineOpens : Type u)) (s : Finset (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (hs : Eq (α := Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, (↑U : Y.Opens)) : Type u))) ⊤)
    (H :
      ∀ (f_1 : ↥s),
        Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens)) : Scheme))
          (f ∣_ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens))),
    Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
hU₁ : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))
⊢ Q (X := (↑(f ⁻¹ᵁ (↑V : Y.Opens)) : Scheme)) (f ∣_ (↑V : Y.Opens))

Tactic:
induction V using of_affine_open_cover U hU with
  | basicOpen U r h =>
    have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r)).mp this
  | openCover U s hs H =>
    apply AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _
      (s.image (Scheme.Opens.topIso _).inv) (by simp [← Ideal.map_span, hs, Ideal.map_top])
    intro ⟨r, hr⟩
    obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)
  | hU i => exact hU' i

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))
this : Q.IsLocal := ⋯
intro : ∀ (V : (↑Y.affineOpens : Type u)), Q (X := (↑(f ⁻¹ᵁ (↑V : Y.Opens)) : Scheme)) (f ∣_ (↑V : Y.Opens))
⊢ targetAffineLocally Q f

Tactic:
classical
  intro V
  induction V using of_affine_open_cover U hU with
  | basicOpen U r h =>
    have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r)).mp this
  | openCover U s hs H =>
    apply AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _
      (s.image (Scheme.Opens.topIso _).inv) (by simp [← Ideal.map_span, hs, Ideal.map_top])
    intro ⟨r, hr⟩
    obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)
  | hU i => exact hU' i

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U i) : Y.Opens)) ⊤
⊢ P f ↔ ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))

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

Premises used: AlgebraicGeometry.HasAffineProperty.of_iSup_eq_top, AlgebraicGeometry.HasAffineProperty.restrict, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
h𝒰 :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    Q (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
⊢ P f

Tactic:
letI := isLocal_affineProperty P
  of_iSup_eq_top
    (fun i ↦ ⟨_, isAffineOpen_opensRange (𝒰.f i)⟩) 𝒰.iSup_opensRange
    (fun i ↦ (Q.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (h𝒰 i))

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.HasAffineProperty.of_iSup_eq_top, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff, Subtype.mk, AlgebraicGeometry.morphismRestrictOpensRange, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
this : Q.IsLocal := ⋯
rw :
  (∀ (i : 𝒰.I₀),
      Q (X :=
        (↑(f ⁻¹ᵁ
              (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯) :
                Y.Opens)) :
          Scheme))
        (f ∣_
          (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯) : Y.Opens))) ↔
    ∀ (i : 𝒰.toPreZeroHypercover.1),
      Q (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
⊢ P f ↔
    ∀ (i : 𝒰.toPreZeroHypercover.1),
      Q (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)

Tactic:
rw [iff_of_iSup_eq_top (P := P)
    (fun i ↦ ⟨_, isAffineOpen_opensRange _⟩) 𝒰.iSup_opensRange]

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, Subtype.mk, AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
this : Q.IsLocal := ⋯
⊢ (∀ (i : 𝒰.I₀),
      Q (X :=
        (↑(f ⁻¹ᵁ
              (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯) :
                Y.Opens)) :
          Scheme))
        (f ∣_
          (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯) : Y.Opens))) ↔
    ∀ (i : 𝒰.toPreZeroHypercover.1),
      Q (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)

Tactic:
forall_congr' fun i ↦ Q.arrow_mk_iso_iff
    (morphismRestrictOpensRange f _)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictOpensRange, forall_congr', CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
this : Q.IsLocal := ⋯
⊢ (∀ (i : 𝒰.I₀),
      Q (X :=
        (↑(f ⁻¹ᵁ
              (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯) :
                Y.Opens)) :
          Scheme))
        (f ∣_
          (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯) : Y.Opens))) ↔
    ∀ (i : 𝒰.toPreZeroHypercover.1),
      Q (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)

Tactic:
exact forall_congr' fun i ↦ Q.arrow_mk_iso_iff
    (morphismRestrictOpensRange f _)

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictOpensRange, forall_congr'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
rw :
  (∀
      (i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).1),
      Q (X :=
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
              (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
          i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)) f i :
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
              i ⟶
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).X
              i)) ↔
    Q f
⊢ P f ↔ Q f

Tactic:
rw [iff_of_openCover (P := P) (Scheme.coverOfIsIso.{0} (𝟙 Y))]

Premises used: AlgebraicGeometry.Scheme.coverOfIsIso, AlgebraicGeometry.HasAffineProperty.iff_of_openCover, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
trans :
  (∀
      (i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).1),
      Q (X :=
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
              (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
          i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)) f i :
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
              i ⟶
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).X
              i)) ↔
    Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))
trans₁ : Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y)) ↔ Q f
⊢ (∀
      (i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).1),
      Q (X :=
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
              (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
          i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)) f i :
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
              i ⟶
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).X
              i)) ↔
    Q f

Tactic:
trans Q (pullback.snd f (𝟙 _))

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
⊢ (∀
      (i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).1),
      Q (X :=
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
              (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
          i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)) f i :
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
              i ⟶
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).X
              i)) ↔
    Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))

Tactic:
⟨fun H => H PUnit.unit, fun H _ => H⟩

Premises used: Iff.intro, PUnit.unit
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
⊢ (∀
      (i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).1),
      Q (X :=
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
              (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
          i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)) f i :
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Precoverage.ZeroHypercover.pullback₁ f (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y)))).X
              i ⟶
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 Y))).X
              i)) ↔
    Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y))

Tactic:
exact ⟨fun H => H PUnit.unit, fun H _ => H⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
this : Q.IsLocal := ⋯
rw : Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y) ≫ 𝟙 Y) ↔ Q f
rw₁ : Q (X := pullback f (𝟙 Y)) (pullback.fst f (𝟙 Y) ≫ f) ↔ Q f
rw₂ rw₃ : Q f ↔ Q f
⊢ Q (X := pullback f (𝟙 Y)) (pullback.snd f (𝟙 Y)) ↔ Q f

Tactic:
rw [← Category.comp_id (pullback.snd _ _), ← pullback.condition,
    Q.cancel_left_of_respectsIso]

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
restrict : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Y.Opens),
    iSup U = ⊤ → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
⊢ IsZariskiLocalAtTarget P

Tactic:
apply IsZariskiLocalAtTarget.mk'

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.mk'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
restrict : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : Y.Opens), targetAffineLocally Q f → targetAffineLocally Q (f ∣_ U)
⊢ ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)

Tactic:
rw [eq_targetAffineLocally P]

Premises used: AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
H : targetAffineLocally Q f
V : (↑(↑U : Scheme).affineOpens : Type u_1)
restrict : Q (X := (↑(f ⁻¹ᵁ U.ι ''ᵁ (↑V : (↑U : Scheme).Opens)) : Scheme)) (f ∣_ U.ι ''ᵁ (↑V : (↑U : Scheme).Opens))
⊢ Q (X := (↑((f ∣_ U) ⁻¹ᵁ (↑V : (↑U : Scheme).Opens)) : Scheme)) (f ∣_ U ∣_ (↑V : (↑U : Scheme).Opens))

Tactic:
rw [Q.arrow_mk_iso_iff (morphismRestrictRestrict f _ _)]

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictRestrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
H : targetAffineLocally Q f
V : (↑(↑U : Scheme).affineOpens : Type u_1)
⊢ Q (X := (↑(f ⁻¹ᵁ U.ι ''ᵁ (↑V : (↑U : Scheme).Opens)) : Scheme)) (f ∣_ U.ι ''ᵁ (↑V : (↑U : Scheme).Opens))

Tactic:
H ⟨_, V.2.image_of_isOpenImmersion (Y.ofRestrict _)⟩

Premises used: AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, Subtype.mk, AlgebraicGeometry.Scheme.ofRestrict, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
H : targetAffineLocally Q f
V : (↑(↑U : Scheme).affineOpens : Type u_1)
⊢ Q (X := (↑(f ⁻¹ᵁ U.ι ''ᵁ (↑V : (↑U : Scheme).Opens)) : Scheme)) (f ∣_ U.ι ''ᵁ (↑V : (↑U : Scheme).Opens))

Tactic:
exact H ⟨_, V.2.image_of_isOpenImmersion (Y.ofRestrict _)⟩

Premises used: AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, Subtype.mk, AlgebraicGeometry.Scheme.ofRestrict, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
of_sSup_eq_top : P f
⊢ P f

Tactic:
let 𝒰 := Y.openCoverOfIsOpenCover U hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
of_sSup_eq_top :
  ∀ (i : 𝒰.affineRefinement.openCover.toPreZeroHypercover.1),
    Q (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰.affineRefinement.openCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).X i ⟶ 𝒰.affineRefinement.openCover.X i)
⊢ P f

Tactic:
apply of_openCover 𝒰.affineRefinement.openCover

Premises used: AlgebraicGeometry.HasAffineProperty.of_openCover, AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.Scheme.OpenCover.affineRefinement
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
    ((fun (i : 𝒰.I₀) ↦
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
          PreZeroHypercover (𝒰.X i)))
      i)
⊢ P (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)

Tactic:
(P.arrow_mk_iso_iff
        (morphismRestrictEq _ ?_ ≪≫ morphismRestrictOpensRange f (𝒰.f i))).mp (H i)

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.limit, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictOpensRange, AlgebraicGeometry.morphismRestrictEq, CategoryTheory.Iso.trans, Iff.mp, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
    ((fun (i : 𝒰.I₀) ↦
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
          PreZeroHypercover (𝒰.X i)))
      i)
refine : U i = Scheme.Hom.opensRange (𝒰.f i)
⊢ P (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)

Tactic:
refine (P.arrow_mk_iso_iff
        (morphismRestrictEq _ ?_ ≪≫ morphismRestrictOpensRange f (𝒰.f i))).mp (H i)

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.morphismRestrictOpensRange, AlgebraicGeometry.morphismRestrictEq, CategoryTheory.Iso.trans, Iff.mp, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
    ((fun (i : 𝒰.I₀) ↦
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
          PreZeroHypercover (𝒰.X i)))
      i)
⊢ U i = Scheme.Hom.opensRange (𝒰.f i)

Tactic:
(Scheme.Opens.opensRange_ι _).symm

Premises used: AlgebraicGeometry.Scheme.Opens.opensRange_ι, AlgebraicGeometry.Scheme.restrict, AlgebraicGeometry.Scheme.ofRestrict, AlgebraicGeometry.Scheme.Opens.ι, Eq.symm, AlgebraicGeometry.Scheme.Opens.toScheme