-- Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean
/-- If `P` respects isos, then `stalkwise P` respects isos. -/
lemma stalkwise_respectsIso (hP : RingHom.RespectsIso P) :
    (stalkwise P).RespectsIso where
  precomp {X Y Z} e (he : IsIso e) f hf

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (f ≫ e)

Tactic:
simp only [stalkwise, Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ ∀ (x : ↑↑X.toPresheafedSpace), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ≫ e) x))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
x : ↑↑X.toPresheafedSpace
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((ConcreteCategory.hom e.base) x) ≫ Scheme.Hom.stalkMap e x))

Tactic:
exact (RingHom.RespectsIso.cancel_right_isIso hP _ _).mpr <| hf (e.base x)

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
x : ↑↑X.toPresheafedSpace
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (e ≫ f) x))

Tactic:
rw [Scheme.stalkMap_comp]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
x : ↑↑X.toPresheafedSpace
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((ConcreteCategory.hom e.base) x) ≫ Scheme.Hom.stalkMap e x))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
x : ↑↑X.toPresheafedSpace
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap e ((ConcreteCategory.hom f.base) x) ≫ Scheme.Hom.stalkMap f x))

Tactic:
exact (RingHom.RespectsIso.cancel_left_isIso hP _ _).mpr <| hf x

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ ∀ (x : ↑↑X.toPresheafedSpace), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ≫ e) x))

Tactic:
intro x

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
x : ↑↑X.toPresheafedSpace
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ≫ e) x))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (e ≫ f)

Tactic:
simp only [stalkwise, Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ ∀ (x : ↑↑X.toPresheafedSpace), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (e ≫ f) x))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
x : ↑↑X.toPresheafedSpace
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ≫ e) x))

Tactic:
rw [Scheme.stalkMap_comp]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
x : ↑↑X.toPresheafedSpace
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap e ((ConcreteCategory.hom f.base) x) ≫ Scheme.Hom.stalkMap f x))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ ∀ (x : ↑↑X.toPresheafedSpace), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (e ≫ f) x))

Tactic:
intro x

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
x : ↑↑X.toPresheafedSpace
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (e ≫ f) x))