-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
theorem sourceAffineLocally_morphismRestrict {X Y : Scheme.{u}} (f : X ⟶ Y)
    (U : Y.Opens) (hU : IsAffineOpen U) :
    @sourceAffineLocally P _ _ (f ∣_ U) hU ↔
      ∀ (V : X.affineOpens) (e : V.1 ≤ f ⁻¹ᵁ U), P (f.appLE U V e).hom

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
⊢ (∀ (U_1 : ↑(↑(f ⁻¹ᵁ U)).affineOpens), P (CommRingCat.Hom.hom (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑U_1) ⋯))) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) e))

Tactic:
rw [(affineOpensRestrict (f ⁻¹ᵁ U)).forall_congr_left, Subtype.forall]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
⊢ (∀ (a : ↑X.affineOpens) (b : ↑a ≤ f ⁻¹ᵁ U),
      P
        (CommRingCat.Hom.hom
          (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨a, b⟩)) ⋯))) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) e))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) (f ∣_ U) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) e))

Tactic:
dsimp only [sourceAffineLocally]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
⊢ (∀ (U_1 : ↑(↑(f ⁻¹ᵁ U)).affineOpens), P (CommRingCat.Hom.hom (Hom.appLE (f ∣_ U) ⊤ ↑U_1 ⋯))) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) e))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : ↑X.affineOpens
h : ↑V ≤ f ⁻¹ᵁ U
⊢ P (CommRingCat.Hom.hom (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨V, h⟩)) ⋯)) ↔
    P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) h))

Tactic:
have := (affineOpensRestrict (f ⁻¹ᵁ U)).apply_symm_apply ⟨V, h⟩

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : ↑X.affineOpens
h : ↑V ≤ f ⁻¹ᵁ U
this : (affineOpensRestrict (f ⁻¹ᵁ U)) ((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨V, h⟩) = ⟨V, h⟩
⊢ P (CommRingCat.Hom.hom (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨V, h⟩)) ⋯)) ↔
    P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) h))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
⊢ (∀ (U_1 : ↑(↑(f ⁻¹ᵁ U)).affineOpens), P (CommRingCat.Hom.hom (Hom.appLE (f ∣_ U) ⊤ ↑U_1 ⋯))) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) e))

Tactic:
simp only [morphismRestrict_appLE]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
⊢ (∀ (U_1 : ↑(↑(f ⁻¹ᵁ U)).affineOpens), P (CommRingCat.Hom.hom (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑U_1) ⋯))) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) e))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : ↑X.affineOpens
h : ↑V ≤ f ⁻¹ᵁ U
this : (affineOpensRestrict (f ⁻¹ᵁ U)) ((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨V, h⟩) = ⟨V, h⟩
⊢ P (CommRingCat.Hom.hom (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨V, h⟩)) ⋯)) ↔
    P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) h))

Tactic:
exact f.appLE_congr _ (Opens.ι_image_top _) congr($(this).1.1) (fun f => P f.hom)

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
⊢ (∀ (a : ↑X.affineOpens) (b : ↑a ≤ f ⁻¹ᵁ U),
      P
        (CommRingCat.Hom.hom
          (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨a, b⟩)) ⋯))) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) e))

Tactic:
refine forall₂_congr fun V h ↦ ?_

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : ↑X.affineOpens
h : ↑V ≤ f ⁻¹ᵁ U
⊢ P (CommRingCat.Hom.hom (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨V, h⟩)) ⋯)) ↔
    P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) h))