-- 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
this :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q
hf : IsAffineHom f
⊢ (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f

Tactic:
constructor

Result:
case mp
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
⊢ (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
    affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f

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
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f →
    ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

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
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f →
    ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
intro h U hU

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 : 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))

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))
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f

Tactic:
have : IsAffine X := isAffine_of_isAffineHom f

Result:
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
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f

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))
⊢ ∀ (i : ↑Y.affineOpens), affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) (f ∣_ ↑i)

Tactic:
intro U

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
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) (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
⊢ IsAffineHom f →
    ((∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
      affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f)

Tactic:
intro hf

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
hf : IsAffineHom f
⊢ (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f