-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
lemma of_isLocalAtSource_of_isLocalAtTarget [IsLocalAtTarget P] [IsLocalAtSource P] :
    HasRingHomProperty P (fun f ↦ P (Spec.map (CommRingCat.ofHom f))) where
  isLocal_ringHomProperty :=
    isLocal_ringHomProperty_of_isLocalAtSource_of_isLocalAtTarget P
  eq_affineLocally'

Proof state:
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
S : CommRingCat
X : Scheme
f : X ⟶ Spec S
hX : ∃ R, X = Spec R
⊢ P f ↔ Q f

Tactic:
obtain ⟨R, rfl⟩ := hX

Result:
case intro
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
S R : CommRingCat
f : Spec R ⟶ Spec S
⊢ P f ↔ Q f

Proof state:
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
⊢ P = affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))

Tactic:
let Q := affineLocally (fun f ↦ P (Spec.map (CommRingCat.ofHom f)))

Result:
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
⊢ P = affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))

Proof state:
case intro.inr
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this✝ : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
this : ∀ ⦃X : Scheme⦄ (f : X ⟶ Spec S), (∃ R, X = Spec R) → (P f ↔ Q f)
hX : ¬∃ R, X = Spec R
⊢ P f ↔ Q f

Tactic:
rw [IsLocalAtSource.iff_of_openCover (P := P) X.affineCover,
  IsLocalAtSource.iff_of_openCover (P := Q) X.affineCover]

Result:
case intro.inr
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this✝ : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
this : ∀ ⦃X : Scheme⦄ (f : X ⟶ Spec S), (∃ R, X = Spec R) → (P f ↔ Q f)
hX : ¬∃ R, X = Spec R
⊢ (∀ (i : X.affineCover.J), P (X.affineCover.map i ≫ f)) ↔ ∀ (i : X.affineCover.J), Q (X.affineCover.map i ≫ f)

Proof state:
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
X Y : Scheme
f : X ⟶ Y
hY : ∃ R, Y = Spec R
⊢ P f ↔ Q f

Tactic:
obtain ⟨S, rfl⟩ := hY

Result:
case intro
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
⊢ P f ↔ Q f

Proof state:
case h.inr
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this✝ : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
X Y : Scheme
f : X ⟶ Y
this : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), (∃ R, Y = Spec R) → (P f ↔ Q f)
hY : ¬∃ R, Y = Spec R
⊢ P f ↔ Q f

Tactic:
rw [IsLocalAtTarget.iff_of_openCover (P := P) Y.affineCover,
  IsLocalAtTarget.iff_of_openCover (P := Q) Y.affineCover]

Result:
case h.inr
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this✝ : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
X Y : Scheme
f : X ⟶ Y
this : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), (∃ R, Y = Spec R) → (P f ↔ Q f)
hY : ¬∃ R, Y = Spec R
⊢ (∀ (i : Y.affineCover.1), P (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    ∀ (i : Y.affineCover.1), Q (Scheme.Cover.pullbackHom Y.affineCover f i)

Proof state:
case h
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ Q f

Tactic:
wlog hY : ∃ R, Y = Spec R generalizing X Y

Result:
case h.inr
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this✝ : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
X Y : Scheme
f : X ⟶ Y
this : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), (∃ R, Y = Spec R) → (P f ↔ Q f)
hY : ¬∃ R, Y = Spec R
⊢ P f ↔ Q f

P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
X Y : Scheme
f : X ⟶ Y
hY : ∃ R, Y = Spec R
⊢ P f ↔ Q f

Proof state:
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
⊢ P = Q

Tactic:
ext X Y f

Result:
case h
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ Q f

Proof state:
case intro
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
S R : CommRingCat
f : Spec R ⟶ Spec S
⊢ P f ↔ Q f

Tactic:
obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f := ⟨_, Spec.map_preimage _⟩

Result:
case intro.intro
P : MorphismProperty Scheme
inst✝¹ : IsLocalAtTarget P
inst✝ : IsLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
S R : CommRingCat
φ : S ⟶ R
⊢ P (Spec.map φ) ↔ Q (Spec.map φ)