awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H_1 : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
U : (↑X.affineOpens : Type u)
s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u)
hs : Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ⊤
H :
  ∀ (f_1 : ↥s),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S :=
      (↑Γ(X, (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom
        (Scheme.Hom.appLE f ⊤ (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens) ⋯))
r : (↑(↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) ⋯))

Tactic:
H r

Premises used: setOf, AlgebraicGeometry.RingedSpace.basicOpen, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H_1 : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
U : (↑X.affineOpens : Type u)
s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u)
hs : Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ⊤
H :
  ∀ (f_1 : ↥s),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S :=
      (↑Γ(X, (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom
        (Scheme.Hom.appLE f ⊤ (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens) ⋯))
r : (↑(↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) ⋯))

Tactic:
exact H r
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
i : 𝒰.I₀
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))

Tactic:
specialize H i
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S :=
    (↑Γ((↑(↑(S i) : X.Opens) : Scheme), (IsOpenImmersion.isoOfRangeEq (𝒰.f i) (↑(S i) : X.Opens).ι ⋯).inv ⁻¹ᵁ ⊤) :
      Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ((↑(S i) : X.Opens).ι ''ᵁ ⊤) ⋯))

Tactic:
rw [← (isLocal_ringHomProperty P).respectsIso.cancel_right_isIso _
      ((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (S i).1.ι
      Subtype.range_coe.symm).inv.app _), ← CommRingCat.hom_comp, ← Scheme.Hom.comp_appTop,
      IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, Scheme.Hom.comp_appTop,
      Scheme.Opens.ι_appTop, Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map] at H

Premises used: CategoryTheory.PreZeroHypercover.f, RingHom.RespectsIso.cancel_right_isIso, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, AlgebraicGeometry.Scheme.Hom.appTop, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, CommRingCat.hom_comp, Subtype.range_coe, AlgebraicGeometry.Scheme.Opens.ι_appTop, AlgebraicGeometry.Scheme.Hom.app, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Hom.comp_appTop, Eq.symm, Subtype.val, AlgebraicGeometry.Scheme.Hom.appLE_map, CategoryTheory.Iso.inv, RingHom.PropertyIsLocal.respectsIso, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
i : 𝒰.I₀
H :
  Q (R := (↑Γ(Y, ⊤) : Type u)) (S :=
    (↑Γ((↑(↑(S i) : X.Opens) : Scheme), (IsOpenImmersion.isoOfRangeEq (𝒰.f i) (↑(S i) : X.Opens).ι ⋯).inv ⁻¹ᵁ ⊤) :
      Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ((↑(S i) : X.Opens).ι ''ᵁ ⊤) ⋯))
⊢ (↑(S i) : X.Opens).ι ''ᵁ ⊤ = (↑(S i) : X.Opens)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
i : 𝒰.I₀
H :
  Q (R := (↑Γ(Y, ⊤) : Type u)) (S :=
    (↑Γ((↑(↑(S i) : X.Opens) : Scheme), (IsOpenImmersion.isoOfRangeEq (𝒰.f i) (↑(S i) : X.Opens).ι ⋯).inv ⁻¹ᵁ ⊤) :
      Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ((↑(S i) : X.Opens).ι ''ᵁ ⊤) ⋯))
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(S i) : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(S i) : X.Opens) ⋯))

Tactic:
exact (f.appLE_congr _ rfl (by simp) (fun f => Q f.hom)).mp H

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Hom.appLE_congr, Iff.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
⊢ P f ↔ ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))

Tactic:
⟨fun H i ↦ appTop P _ (comp_of_isOpenImmersion P (𝒰.f i) f H), of_source_openCover 𝒰⟩

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.HasRingHomProperty.comp_of_isOpenImmersion, AlgebraicGeometry.HasRingHomProperty.appTop, Iff.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.HasRingHomProperty.of_source_openCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine X
inst_2 : IsAffine Y
rw :
  (∀
      (i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 X))).I₀),
      Q
        (CommRingCat.Hom.hom
          (Scheme.Hom.appTop
            ((Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 X))).f
                i ≫
              f)))) ↔
    Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ P f ↔ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
rw [iff_of_source_openCover (P := P) (Scheme.coverOfIsIso.{u} (𝟙 _))]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine X
inst_2 : IsAffine Y
⊢ (∀
      (i :
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 X))).I₀),
      Q
        (CommRingCat.Hom.hom
          (Scheme.Hom.appTop
            ((Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 X))).f
                i ≫
              f)))) ↔
    Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
simp +instances
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
R S : CommRingCat
φ : R ⟶ S
⊢ RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
have H := (isLocal_ringHomProperty P).respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ))) ↔ Q (CommRingCat.Hom.hom φ)
rw₁ :
  Q ((CommRingCat.Hom.hom (Scheme.ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ)))) ↔
    Q (CommRingCat.Hom.hom φ)
rw₂ : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ) ≫ (Scheme.ΓSpecIso S).hom)) ↔ Q (CommRingCat.Hom.hom φ)
rw₃ : Q (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).hom ≫ φ)) ↔ Q (CommRingCat.Hom.hom φ)
rw₄ : Q ((CommRingCat.Hom.hom φ).comp (CommRingCat.Hom.hom (Scheme.ΓSpecIso R).hom)) ↔ Q (CommRingCat.Hom.hom φ)
rw₅ rw₆ : Q (CommRingCat.Hom.hom φ) ↔ Q (CommRingCat.Hom.hom φ)
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)

Tactic:
rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,
    ← CommRingCat.hom_comp, Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]

Premises used: RingHom.RespectsIso.cancel_right_isIso, AlgebraicGeometry.Scheme.ΓSpecIso, CommRingCat.hom_comp, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, RingHom.RespectsIso.cancel_left_isIso, CategoryTheory.Iso.hom, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H :
  ∀ (i : ι),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(U i) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(U i) : X.Opens) ⋯))
have :
  ∀
    (this :
      ∀ (i : (X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).I₀),
        IsAffine.{u} ((X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).X i)),
    P f
⊢ P f

Tactic:
have (i : _) : IsAffine ((X.openCoverOfIsOpenCover _ hU).X i) := (U i).2
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H :
  ∀ (i : ι),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(U i) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(U i) : X.Opens) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).I₀),
    IsAffine.{u} ((X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).X i)
refine :
  ∀ (i : (X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).I₀),
    Q
      (CommRingCat.Hom.hom
        (Scheme.Hom.appTop ((X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).f i ≫ f)))
⊢ P f

Tactic:
refine of_source_openCover (X.openCoverOfIsOpenCover _ hU) fun i ↦ ?_

Premises used: AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, AlgebraicGeometry.HasRingHomProperty.of_source_openCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H :
  ∀ (i : ι),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(U i) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(U i) : X.Opens) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).I₀),
    IsAffine.{u} ((X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).X i)
i : (X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).I₀
⊢ (↑(U i) : X.Opens) = (↑(U i) : X.Opens).ι ''ᵁ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H :
  ∀ (i : ι),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(U i) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(U i) : X.Opens) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).I₀),
    IsAffine.{u} ((X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).X i)
i : (X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).I₀
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).f i ≫ f)))

Tactic:
simpa [Scheme.Hom.app_eq_appLE] using (f.appLE_congr _ rfl (by simp) (fun f => Q f.hom)).mp (H i)

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Hom.appLE_congr, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, Iff.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
⊢ P f ↔
    ∀ (i : ι),
      Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(U i) : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(U i) : X.Opens) ⋯))

Tactic:
⟨fun H _ ↦ appLE P f H ⟨_, isAffineOpen_top _⟩ _ le_top, of_iSup_eq_top U hU⟩

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.HasRingHomProperty.of_iSup_eq_top, AlgebraicGeometry.HasRingHomProperty.appLE, Subtype.mk, le_top, Iff.intro, Top.top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover),
    sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
      ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)
⊢ IsZariskiLocalAtSource P

Tactic:
apply HasAffineProperty.isZariskiLocalAtSource

Premises used: AlgebraicGeometry.HasAffineProperty.isZariskiLocalAtSource
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
H :
  ∀ [inst : IsAffine Y] (𝒰 : X.OpenCover),
    sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
      ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)
⊢ ∀ [inst : IsAffine Y] (𝒰 : X.OpenCover),
    sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
      ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : X.OpenCover
H :
  (∀ (i : 𝒰.affineRefinement.openCover.I₀),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.affineRefinement.openCover.f i ≫ f)))) ↔
    ∀ (i : 𝒰.I₀)
      (i_1 : PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)),
      Q
        (CommRingCat.Hom.hom
          (Scheme.Hom.appTop
            (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover) i_1 ≫ 𝒰.f i ≫ f)))
⊢ sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)

Tactic:
simp_rw [← HasAffineProperty.iff_of_isAffine (P := P),
    iff_of_source_openCover 𝒰.affineRefinement.openCover,
    fun i ↦ iff_of_source_openCover (P := P) (f := 𝒰.f i ≫ f) (𝒰.X i).affineCover]

Premises used: CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.Scheme.OpenCover.affineRefinement, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, AlgebraicGeometry.Scheme.affineCover, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : X.OpenCover
⊢ (∀ (i : 𝒰.affineRefinement.openCover.I₀),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.affineRefinement.openCover.f i ≫ f)))) ↔
    ∀ (i : 𝒰.I₀)
      (i_1 : PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)),
      Q
        (CommRingCat.Hom.hom
          (Scheme.Hom.appTop
            (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover) i_1 ≫ 𝒰.f i ≫ f)))

Tactic:
simp [Scheme.OpenCover.affineRefinement, Sigma.forall]

Premises used: Sigma.forall, AlgebraicGeometry.Scheme.OpenCover.affineRefinement
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X : Scheme
rw : ∀ (i : (↑X.affineOpens : Type u)), P (X := (↑(𝟙 X ⁻¹ᵁ (↑i : X.Opens)) : Scheme)) (𝟙 X ∣_ (↑i : X.Opens))
⊢ P (𝟙 X)

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : (↑X.affineOpens : Type u)
have :
  ∀ (this : IsAffine.{u} (↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme)),
    P (X := (↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme)) (𝟙 X ∣_ (↑U : X.Opens))
⊢ P (X := (↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme)) (𝟙 X ∣_ (↑U : X.Opens))

Tactic:
have : IsAffine (𝟙 X ⁻¹ᵁ U.1) := U.2
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : (↑X.affineOpens : Type u)
this : IsAffine.{u} (↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme)
rw : Q (CommRingCat.Hom.hom (𝟙 Γ((↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme), ⊤)))
⊢ P (X := (↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme)) (𝟙 X ∣_ (↑U : X.Opens))

Tactic:
rw [morphismRestrict_id, iff_of_isAffine (P := P), Scheme.Hom.id_appTop]

Premises used: AlgebraicGeometry.Scheme.Hom.id_appTop, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, AlgebraicGeometry.morphismRestrict_id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : (↑X.affineOpens : Type u)
this : IsAffine.{u} (↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme)
⊢ Q (CommRingCat.Hom.hom (𝟙 Γ((↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme), ⊤)))

Tactic:
apply hP
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
⊢ RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))

Tactic:
have hP : RingHom.RespectsIso (fun f ↦ P (Spec.map (CommRingCat.ofHom f))) :=
    RingHom.toMorphismProperty_respectsIso_iff.mpr
      (inferInstanceAs (P.inverseImage Scheme.Spec).unop.RespectsIso)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
localizationAwayPreserves :
  RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
ofLocalizationSpanTarget :
  RingHom.OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
ofLocalizationSpan :
  RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
StableUnderCompositionWithLocalizationAwayTarget :
  RingHom.StableUnderCompositionWithLocalizationAwayTarget.{u}
    fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))

Tactic:
constructor