-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
/-- If `P` is stable under base change, so is `affineAnd P`. -/
lemma affineAnd_isStableUnderBaseChange (hQi : RingHom.RespectsIso Q)
    (hQb : RingHom.IsStableUnderBaseChange Q) :
    (affineAnd Q).IsStableUnderBaseChange

Proof state:
case H
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty.RespectsIso
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
hY : IsAffine Y
hg : (fun {R S} [CommRing R] [CommRing S] => Q) (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) (Limits.pullback.fst f g)

Tactic:
exact ⟨inferInstance, hQb.pullback_fst_appTop _ hQi f _ hg⟩

Result:
no goals

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty.RespectsIso
⊢ (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).IsStableUnderBaseChange

Tactic:
apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk

Result:
case H
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty.RespectsIso
⊢ ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) g →
      affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) (Limits.pullback.fst f g)

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q
⊢ (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).IsStableUnderBaseChange

Tactic:
haveI : (affineAnd Q).toProperty.RespectsIso := affineAnd_respectsIso hQi

Result:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty.RespectsIso
⊢ (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).IsStableUnderBaseChange

Proof state:
case H
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty.RespectsIso
⊢ ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) g →
      affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) (Limits.pullback.fst f g)

Tactic:
intro X Y S _ _ f g ⟨hY, hg⟩

Result:
case H
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty.RespectsIso
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
hY : IsAffine Y
hg : (fun {R S} [CommRing R] [CommRing S] => Q) (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) (Limits.pullback.fst f g)