-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
/-- If `P` is a morphism property affine locally defined by `affineAnd Q`, `P` is stable under
composition if `Q` is. -/
lemma HasAffineProperty.affineAnd_isStableUnderComposition {P : MorphismProperty Scheme.{u}}
    (hA : HasAffineProperty P (affineAnd Q)) (hQ : RingHom.StableUnderComposition Q) :
    P.IsStableUnderComposition where
  comp_mem {X Y Z} f g hf hg

Proof state:
case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this✝ : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
          P f → P g → HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P (f ∣_ g ⁻¹ᵁ ↑U ≫ g ∣_ ↑U)

Tactic:
exact this hA hQ _ _ (IsLocalAtTarget.restrict hf _) (IsLocalAtTarget.restrict hg _) hA U.2

Result:
no goals

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
⊢ P (f ≫ g)

Tactic:
wlog hZ : IsAffine Z

Result:
case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this✝ : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
          P f → P g → HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
⊢ P (f ≫ g)

Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hZ : IsAffine Z
⊢ P (f ≫ g)

Proof state:
case intro.intro
Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hZ : IsAffine Z
hY : IsAffine Y
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) (f ≫ g)

Tactic:
exact ⟨hX, hQ _ _ hg hf⟩

Result:
no goals

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
⊢ P (f ≫ g)

Tactic:
haveI := hA

Result:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
⊢ P (f ≫ g)

Proof state:
Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hZ : IsAffine Z
⊢ P (f ≫ g)

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hg

Result:
Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
this : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hZ : IsAffine Z
hg : affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) g
⊢ P (f ≫ g)

Proof state:
case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this✝ : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
          P f → P g → HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
⊢ P (f ≫ g)

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

Result:
case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this✝ : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
          P f → P g → HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
⊢ ∀ (i : ↑Z.affineOpens), P ((f ≫ g) ∣_ ↑i)