-- Mathlib/RingTheory/RingHomProperties.lean
lemma toMorphismProperty_respectsIso_iff :
    RespectsIso P ↔ (toMorphismProperty P).RespectsIso

Proof state:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : CommRingCat
e : Y ≅ Z
f : X ⟶ Y
hf : toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) (f ≫ e.hom)

Tactic:
exact h.left f.hom e.commRingCatIsoToRingEquiv hf

Result:
no goals

Proof state:
case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    (fun {R S} [CommRing R] [CommRing S] => P) f → (fun {R S} [CommRing R] [CommRing S] => P) (e.toRingHom.comp f)

Tactic:
intro X Y Z _ _ _ f e hf

Result:
case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
X Y Z : Type u
inst✝² : CommRing X
inst✝¹ : CommRing Y
inst✝ : CommRing Z
f : X →+* Y
e : Y ≃+* Z
hf : P f
⊢ P (e.toRingHom.comp f)

Proof state:
case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
X Y Z : Type u
inst✝² : CommRing X
inst✝¹ : CommRing Y
inst✝ : CommRing Z
f : X →+* Y
e : Y ≃+* Z
hf : P f
⊢ P (e.toRingHom.comp f)

Tactic:
exact MorphismProperty.RespectsIso.postcomp (toMorphismProperty P)
  e.toCommRingCatIso.hom (CommRingCat.ofHom f) hf

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (RespectsIso fun {R S} [CommRing R] [CommRing S] => P) ↔
    (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso

Tactic:
refine ⟨fun h ↦ MorphismProperty.RespectsIso.mk _ ?_ ?_, fun h ↦ ⟨?_, ?_⟩⟩

Result:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
⊢ ∀ {X Y Z : CommRingCat} (e : X ≅ Y) (f : Y ⟶ Z),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) (e.hom ≫ f)

case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
⊢ ∀ {X Y Z : CommRingCat} (e : Y ≅ Z) (f : X ⟶ Y),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) (f ≫ e.hom)

case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    (fun {R S} [CommRing R] [CommRing S] => P) f → (fun {R S} [CommRing R] [CommRing S] => P) (e.toRingHom.comp f)

case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
    (fun {R S} [CommRing R] [CommRing S] => P) f → (fun {R S} [CommRing R] [CommRing S] => P) (f.comp e.toRingHom)

Proof state:
case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
    (fun {R S} [CommRing R] [CommRing S] => P) f → (fun {R S} [CommRing R] [CommRing S] => P) (f.comp e.toRingHom)

Tactic:
intro X Y Z _ _ _ f e

Result:
case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
X Y Z : Type u
inst✝² : CommRing X
inst✝¹ : CommRing Y
inst✝ : CommRing Z
f : Y →+* Z
e : X ≃+* Y
⊢ (fun {R S} [CommRing R] [CommRing S] => P) f → (fun {R S} [CommRing R] [CommRing S] => P) (f.comp e.toRingHom)

Proof state:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : CommRingCat
e : X ≅ Y
f : Y ⟶ Z
hf : toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) (e.hom ≫ f)

Tactic:
exact h.right f.hom e.commRingCatIsoToRingEquiv hf

Result:
no goals

Proof state:
case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
X Y Z : Type u
inst✝² : CommRing X
inst✝¹ : CommRing Y
inst✝ : CommRing Z
f : Y →+* Z
e : X ≃+* Y
⊢ (fun {R S} [CommRing R] [CommRing S] => P) f → (fun {R S} [CommRing R] [CommRing S] => P) (f.comp e.toRingHom)

Tactic:
exact MorphismProperty.RespectsIso.precomp (toMorphismProperty P)
  e.toCommRingCatIso.hom (CommRingCat.ofHom f)

Result:
no goals

Proof state:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
⊢ ∀ {X Y Z : CommRingCat} (e : X ≅ Y) (f : Y ⟶ Z),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) (e.hom ≫ f)

Tactic:
intro X Y Z e f hf

Result:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : CommRingCat
e : X ≅ Y
f : Y ⟶ Z
hf : toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) (e.hom ≫ f)

Proof state:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
⊢ ∀ {X Y Z : CommRingCat} (e : Y ≅ Z) (f : X ⟶ Y),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) (f ≫ e.hom)

Tactic:
intro X Y Z e f hf

Result:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : CommRingCat
e : Y ≅ Z
f : X ⟶ Y
hf : toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) (f ≫ e.hom)