-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
theorem sourceAffineLocally_respectsIso (h₁ : RingHom.RespectsIso P) :
    (sourceAffineLocally P).toProperty.RespectsIso

Proof state:
case h₁
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝ : IsAffine Z
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
this : IsIso (Scheme.Hom.appLE e.hom (e.hom ''ᵁ ↑U) ↑U ⋯)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ ↑U ⋯))

Tactic:
rw [← Scheme.appLE_comp_appLE _ _ ⊤ (e.hom ''ᵁ U) U.1 le_top (e.hom.preimage_image_eq _).ge,
  CommRingCat.hom_comp, h₁.cancel_right_isIso]

Result:
case h₁
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝ : IsAffine Z
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
this : IsIso (Scheme.Hom.appLE e.hom (e.hom ''ᵁ ↑U) ↑U ⋯)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (e.hom ''ᵁ ↑U) ⋯))

Proof state:
case h₂
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst✝ : IsAffine Y
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (e.hom ⁻¹ᵁ ⊤) ↑U ⋯))

Tactic:
exact H U

Result:
no goals

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

Tactic:
introv H U

Result:
case h₁
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝ : IsAffine Z
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ ↑U ⋯))

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

Tactic:
apply AffineTargetMorphismProperty.respectsIso_mk

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

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

Proof state:
case h₁
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝ : IsAffine Z
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ ↑U ⋯))

Tactic:
have : IsIso (e.hom.appLE (e.hom ''ᵁ U) U.1 (e.hom.preimage_image_eq _).ge) :=
  inferInstanceAs (IsIso (e.hom.app _ ≫
    X.presheaf.map (eqToHom (e.hom.preimage_image_eq _).symm).op))

Result:
case h₁
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝ : IsAffine Z
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
this : IsIso (Scheme.Hom.appLE e.hom (e.hom ''ᵁ ↑U) ↑U ⋯)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ ↑U ⋯))

Proof state:
case h₂
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst✝ : IsAffine Y
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ e.hom) ⊤ ↑U ⋯))

Tactic:
rw [Scheme.comp_appLE, CommRingCat.hom_comp, h₁.cancel_left_isIso]

Result:
case h₂
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst✝ : IsAffine Y
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (e.hom ⁻¹ᵁ ⊤) ↑U ⋯))

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

Tactic:
introv H U

Result:
case h₂
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst✝ : IsAffine Y
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ e.hom) ⊤ ↑U ⋯))

Proof state:
case h₁
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝ : IsAffine Z
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f
U : ↑X.affineOpens
this : IsIso (Scheme.Hom.appLE e.hom (e.hom ''ᵁ ↑U) ↑U ⋯)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (e.hom ''ᵁ ↑U) ⋯))

Tactic:
exact H ⟨_, U.prop.image_of_isOpenImmersion e.hom⟩

Result:
no goals