awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf :
  ∀ (U : (↑Y.affineOpens : Type u)),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
      Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
⊢ IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme)

Tactic:
obtain ⟨hfU, hf⟩ := hf ⟨U, hU⟩

Premises used: Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf :
  ∀ (U : (↑Y.affineOpens : Type u)),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
      Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
hfU : IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme)
⊢ Q (R := (↑Γ((↑(↑⟨U, hU⟩ : Y.Opens) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom
      (Scheme.Hom.app f ((↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤)))

Tactic:
obtain ⟨hfU, hf⟩ := hf ⟨U, hU⟩

Premises used: Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf_1 :
  ∀ (U : (↑Y.affineOpens : Type u)),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
      Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
hfU : IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme)
hf :
  Q (R := (↑Γ((↑(↑⟨U, hU⟩ : Y.Opens) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom
      (Scheme.Hom.app f ((↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤)))
right :
  ∀
    (hf :
      Q (R := (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤) : Type u))
        (CommRingCat.Hom.hom
          (Scheme.Hom.app f ((↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤)))),
    Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
have hf : Q (Scheme.Hom.app f (((⟨U, hU⟩ : Y.affineOpens) : Y.Opens).ι ''ᵁ ⊤)).hom := hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf_1 :
  ∀ (U : (↑Y.affineOpens : Type u)),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
      Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
hfU : IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme)
hf_2 :
  Q (R := (↑Γ((↑(↑⟨U, hU⟩ : Y.Opens) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom
      (Scheme.Hom.app f ((↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤)))
hf :
  Q (R := (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤) : Type u))
    (CommRingCat.Hom.hom
      (Scheme.Hom.app f ((↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤)))
right right₁ right₂ right₃ :
  ∀
    (hf :
      Q (R := (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Type u))
        (CommRingCat.Hom.hom
          (Scheme.Hom.app f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)))),
    Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
rwa [Scheme.Opens.ι_image_top] at hf

Premises used: AlgebraicGeometry.Scheme.Opens.ι_image_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
⊢ IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
    Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))

Tactic:
⟨(h U U.2).1, ?_⟩

Premises used: And.left, And.intro, Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
refine_2 :
  Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
⊢ IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
    Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))

Tactic:
refine ⟨(h U U.2).1, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
refine_2 :
  Q (R := (↑Γ(Y, (↑U : Y.Opens).ι ''ᵁ ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
⊢ Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))

Tactic:
change Q (Scheme.Hom.app f ((U : Y.Opens).ι ''ᵁ ⊤)).hom

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Hom.app, AlgebraicGeometry.Scheme.Opens.ι, Top.top, Subtype.val, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
refine_2 : Q (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f (↑U : Y.Opens)))
⊢ Q (R := (↑Γ(Y, (↑U : Y.Opens).ι ''ᵁ ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))

Tactic:
rw [Scheme.Opens.ι_image_top]

Premises used: AlgebraicGeometry.Scheme.Opens.ι_image_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
⊢ Q (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f (↑U : Y.Opens)))

Tactic:
(h U U.2).2

Premises used: And.right, Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
⊢ Q (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f (↑U : Y.Opens)))

Tactic:
exact (h U U.2).2

Premises used: And.right, Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
rw :
  (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
rw [targetAffineLocally_affineAnd_iff hQi, isAffineHom_iff]

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.isAffineHom_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
haveI : HasRingHomProperty (affineLocally Q) Q := ⟨hQ, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
rw :
  (IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    IsAffineHom f ∧ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    IsAffineHom f ∧ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
rw [targetAffineLocally_affineAnd_iff' hQ.respectsIso]

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_iff', RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
simp :
  IsAffineHom f →
    ((∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
      affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f)
⊢ (IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    IsAffineHom f ∧ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
simp only [and_congr_right_iff]

Premises used: and_congr_right_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
mp :
  (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
    affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
mpr :
  affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f →
    ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
mp :
  ∀
    (this :
      ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
        (hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y : Scheme.{u}}
        (f : X ⟶ Y)
        (this :
          HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
            fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
        (hf : IsAffineHom f) (hY : IsAffine Y),
        (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
          affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f)
    (hY : ¬IsAffine Y),
    (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
      affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
wlog :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
    (hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y : Scheme.{u}} (f : X ⟶ Y)
    (this :
      HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
        fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (hf : IsAffineHom f) (hY : IsAffine Y),
    (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
      affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
    affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
wlog hY : IsAffine Y

Premises used: AlgebraicGeometry.IsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this_1 :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
    (hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y : Scheme.{u}} (f : X ⟶ Y)
    (this :
      HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
        fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (hf : IsAffineHom f) (hY : IsAffine Y),
    (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
      affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
mp :
  ∀ (i : (↑Y.affineOpens : Type u)),
    affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme))
      (f ∣_ (↑i : Y.Opens))
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

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

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this_1 :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
    (hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y : Scheme.{u}} (f : X ⟶ Y)
    (this :
      HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
        fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (hf : IsAffineHom f) (hY : IsAffine Y),
    (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
      affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
⊢ IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)

Tactic:
have : IsAffine (f ⁻¹ᵁ U) := hf.isAffine_preimage U U.2
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this_1 :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this_2 :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
    (hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y : Scheme.{u}} (f : X ⟶ Y)
    (this :
      HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
        fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (hf : IsAffineHom f) (hY : IsAffine Y),
    (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
      affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
this : IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)
mp :
  Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
⊢ affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme))
    (f ∣_ (↑U : Y.Opens))

Tactic:
rw [HasRingHomProperty.iff_of_isAffine (P := affineLocally Q),
        morphismRestrict_appTop, CommRingCat.hom_comp, hQ.respectsIso.cancel_right_isIso]

Premises used: RingHom.RespectsIso.cancel_right_isIso, CommRingCat.hom_comp, AlgebraicGeometry.morphismRestrict_appTop, RingHom.PropertyIsLocal.respectsIso, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this_1 :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this_2 :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
    (hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y : Scheme.{u}} (f : X ⟶ Y)
    (this :
      HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
        fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (hf : IsAffineHom f) (hY : IsAffine Y),
    (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
      affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
this : IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)
mp : IsAffineOpen ((↑U : Y.Opens).ι ''ᵁ ⊤)
⊢ Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))

Tactic:
apply h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this_1 :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this_2 :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
    (hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y : Scheme.{u}} (f : X ⟶ Y)
    (this :
      HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
        fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (hf : IsAffineHom f) (hY : IsAffine Y),
    (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
      affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
this : IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)
mp : IsAffineOpen (↑U : Y.Opens)
⊢ IsAffineOpen ((↑U : Y.Opens).ι ''ᵁ ⊤)

Tactic:
rw [Scheme.Opens.ι_image_top]

Premises used: AlgebraicGeometry.Scheme.Opens.ι_image_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this_1 :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this_2 :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
    (hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y : Scheme.{u}} (f : X ⟶ Y)
    (this :
      HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
        fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (hf : IsAffineHom f) (hY : IsAffine Y),
    (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
      affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
this : IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)
⊢ IsAffineOpen (↑U : Y.Opens)

Tactic:
U.2

Premises used: Set.Mem, setOf, AlgebraicGeometry.IsAffineOpen, AlgebraicGeometry.Scheme.affineOpens, Subtype.property