-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
/-- If `P` respects isos, also `affineAnd P` respects isomorphisms. -/
lemma affineAnd_respectsIso (hP : RingHom.RespectsIso Q) :
    (affineAnd Q).toProperty.RespectsIso

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

Tactic:
refine RespectsIso.mk _ ?_ ?_

Result:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z),
    (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty (e.hom ≫ f)

case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y),
    (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty (f ≫ e.hom)

Proof state:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
hZ : IsAffine Y
hf : affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f
⊢ (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty (f ≫ e.hom)

Tactic:
simpa [AffineTargetMorphismProperty.toProperty, isAffine_of_isIso e.inv, hP.cancel_left_isIso]

Result:
no goals

Proof state:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z),
    (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty (e.hom ≫ f)

Tactic:
intro X Y Z e f ⟨hZ, ⟨hY, hf⟩⟩

Result:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
hZ : IsAffine Z
hY : IsAffine Y
hf : (fun {R S} [CommRing R] [CommRing S] => Q) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty (e.hom ≫ f)

Proof state:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
hZ : IsAffine Z
hY : IsAffine Y
hf : (fun {R S} [CommRing R] [CommRing S] => Q) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty (e.hom ≫ f)

Tactic:
simpa [hP.cancel_right_isIso, isAffine_of_isIso e.hom]

Result:
no goals

Proof state:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y),
    (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty (f ≫ e.hom)

Tactic:
intro X Y Z e f ⟨hZ, hf⟩

Result:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
hZ : IsAffine Y
hf : affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f
⊢ (affineAnd fun {R S} [CommRing R] [CommRing S] => Q).toProperty (f ≫ e.hom)