-- 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:
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)

Tactic:
refine forall_congr' fun _ ↦ this _ ⟨_, rfl⟩

Result:
no goals

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
⊢ (∀ (i : Y.affineCover.1), P (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    ∀ (i : Y.affineCover.1), Q (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
refine forall_congr' fun _ ↦ this _ ⟨_, rfl⟩

Result:
no goals

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))
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
⊢ P f ↔ Q f

Tactic:
wlog hX : ∃ R, X = Spec R generalizing X

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
⊢ 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))
S : CommRingCat
X : Scheme
f : X ⟶ Spec S
hX : ∃ R, X = 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 = affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))

Tactic:
show P = Q

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))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))
⊢ P = Q

Proof state:
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 φ) ↔ P (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom φ)))

Tactic:
rfl

Result:
no goals

Proof state:
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 φ)

Tactic:
rw [HasRingHomProperty.Spec_iff (P := Q)]

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 φ) ↔ P (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom φ)))

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))
⊢ P = affineLocally fun {R S} [CommRing R] [CommRing S] f => P (Spec.map (CommRingCat.ofHom f))

Tactic:
have : HasRingHomProperty Q (fun f ↦ P (Spec.map (CommRingCat.ofHom f))) :=
  ⟨isLocal_ringHomProperty_of_isLocalAtSource_of_isLocalAtTarget P, rfl⟩

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))
this : HasRingHomProperty Q 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))