-- Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean
/-- If `P` respects isos, then `stalkwise P` is local at the source. -/
lemma stalkwise_isLocalAtSource_of_respectsIso (hP : RingHom.RespectsIso P) :
    IsLocalAtSource (stalkwise P)

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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] => P) ((U i).ι ≫ f)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ iSup U

Tactic:
rw [hU]

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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] => P) ((U i).ι ≫ f)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ⊤

Proof state:
case of_sSup_eq_top
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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] => P) ((U i).ι ≫ f)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f

Tactic:
intro X Y f ι U hU hf x

Result:
case of_sSup_eq_top
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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] => P) ((U i).ι ≫ f)
x : ↑↑X.toPresheafedSpace
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Proof state:
case restrict
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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens),
    stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f →
      stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (U.ι ≫ f)

Tactic:
intro X Y f U hf x

Result:
case restrict
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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
x : ↑↑(↑U).toPresheafedSpace
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (U.ι ≫ 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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] => P) ((U i).ι ≫ f)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ⊤

Tactic:
trivial

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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
⊢ IsLocalAtSource (stalkwise fun {R S} [CommRing R] [CommRing S] => P)

Tactic:
apply IsLocalAtSource.mk'

Result:
case restrict
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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens),
    stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f →
      stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (U.ι ≫ f)

case of_sSup_eq_top
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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] => P) ((U i).ι ≫ f)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f

Proof state:
case of_sSup_eq_top
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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] => P) ((U i).ι ≫ f)
x : ↑↑X.toPresheafedSpace
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
have hy : x ∈ iSup U := by rw [hU]; trivial

Result:
case of_sSup_eq_top
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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] => P) ((U i).ι ≫ f)
x : ↑↑X.toPresheafedSpace
hy : x ∈ iSup U
⊢ P (CommRingCat.Hom.hom (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
⊢ IsLocalAtSource (stalkwise fun {R S} [CommRing R] [CommRing S] => P)

Tactic:
letI := stalkwise_respectsIso hP

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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
⊢ IsLocalAtSource (stalkwise fun {R S} [CommRing R] [CommRing S] => P)

Proof state:
case of_sSup_eq_top.intro
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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] => P) ((U i).ι ≫ f)
x : ↑↑X.toPresheafedSpace
hy : x ∈ iSup U
i : ι
hi : x ∈ U i
⊢ P ((CommRingCat.Hom.hom (Scheme.Hom.stalkMap (U i).ι ⟨x, hi⟩)).comp (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))

Tactic:
simpa [Scheme.stalkMap_comp] using hf i ⟨x, hi⟩

Result:
no goals