-- 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
⊢ ∀ (i : ↑Z.affineOpens), P ((f ≫ g) ∣_ ↑i)

Tactic:
intro U

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
U : ↑Z.affineOpens
⊢ P ((f ≫ g) ∣_ ↑U)

Proof state:
case 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
hf : P f
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))
⊢ P (f ≫ g)

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

Result:
case 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
hf : affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ 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
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)

Tactic:
obtain ⟨hY, hg⟩ := hg

Result:
case 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
hf : P f
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))
⊢ 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
U : ↑Z.affineOpens
⊢ P ((f ≫ g) ∣_ ↑U)

Tactic:
rw [morphismRestrict_comp]

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
U : ↑Z.affineOpens
⊢ P (f ∣_ g ⁻¹ᵁ ↑U ≫ g ∣_ ↑U)

Proof state:
case 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
hf : affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P (f ≫ g)

Tactic:
obtain ⟨hX, hf⟩ := hf

Result:
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))
⊢ P (f ≫ g)