-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
lemma targetAffineLocally_affineAnd_iff_affineLocally (hQ : RingHom.PropertyIsLocal Q)
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    targetAffineLocally (affineAnd Q) f ↔ IsAffineHom f ∧ affineLocally Q f

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f ↔
    IsAffineHom f ∧ affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f

Tactic:
haveI : HasRingHomProperty (affineLocally Q) Q := ⟨hQ, rfl⟩

Result:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f ↔
    IsAffineHom f ∧ affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f

Proof state:
Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
this✝ :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q
hf : IsAffineHom f
hY : IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
this : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
exact h ⊤ (isAffineOpen_top Y)

Result:
no goals

Proof state:
case mpr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q
hf : IsAffineHom f
h : affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f
U : Y.Opens
hU : IsAffineOpen U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
rw [affineLocally_iff_affineOpens_le] at h

Result:
case mpr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q
hf : IsAffineHom f
h :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : Y.Opens
hU : IsAffineOpen U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f ↔
    IsAffineHom f ∧ affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f

Tactic:
rw [targetAffineLocally_affineAnd_iff' hQ.respectsIso]

Result:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q
⊢ (IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    IsAffineHom f ∧ affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f

Proof state:
case mpr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q
hf : IsAffineHom f
h :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : Y.Opens
hU : IsAffineOpen U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯))

Tactic:
exact h ⟨U, hU⟩ ⟨f ⁻¹ᵁ U, hf.isAffine_preimage U hU⟩ (by simp)

Result:
no goals

Proof state:
case mp.inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
this✝ :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q
hf : IsAffineHom f
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
    (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q) →
      ∀ {X Y : Scheme} (f : X ⟶ Y),
        (HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q)
            fun {R S} [CommRing R] [CommRing S] => Q) →
          IsAffineHom f →
            IsAffine Y →
              (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
                affineLocally (fun {R S} [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
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) (f ∣_ ↑U)

Tactic:
have : IsAffine (f ⁻¹ᵁ U) := hf.isAffine_preimage U U.2

Result:
case mp.inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
this✝¹ :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q
hf : IsAffineHom f
this✝ :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
    (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q) →
      ∀ {X Y : Scheme} (f : X ⟶ Y),
        (HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q)
            fun {R S} [CommRing R] [CommRing S] => Q) →
          IsAffineHom f →
            IsAffine Y →
              (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
                affineLocally (fun {R S} [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
this : IsAffine ↑(f ⁻¹ᵁ ↑U)
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) (f ∣_ ↑U)