awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
this :
  Eq (α := Γ((AffineScheme.of X).obj, ⊤) ⟶ Γ((pullback (AffineScheme.ofHom f) (AffineScheme.ofHom g)).obj, ⊤))
    (CategoryStruct.comp (Y :=
      Opposite.unop
        (pullback (X := Opposite.op Γ((AffineScheme.of X).obj, ⊤)) (Y := Opposite.op Γ((AffineScheme.of Y).obj, ⊤))
          (Z := Opposite.op Γ((AffineScheme.of S).obj, ⊤))
          (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f))))
          (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g))))))
      (Quiver.Hom.unop
        (pullback.fst (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f))))
          (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g))))))
      (Quiver.Hom.unop
        (Iso.hom
          (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f)
            (AffineScheme.ofHom g)))))
    (Scheme.Hom.appTop (InducedCategory.Hom.hom (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))))
rw :
  P (R := (↑Γ(X, ⊤) : Type u)) (S :=
    (↑(pushout (X := Γ((AffineScheme.of S).obj, ⊤)) (Y := Γ((AffineScheme.of X).obj, ⊤)) (Z :=
          Γ((AffineScheme.of Y).obj, ⊤)) (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f)))
          (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g)))) :
      Type u))
    (CommRingCat.Hom.hom
      (pushout.inl (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f)))
        (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g)))))
⊢ P (R := (↑Γ(X, ⊤) : Type u)) (S :=
    (↑Γ(AffineScheme.forgetToScheme.obj (pullback (AffineScheme.ofHom f) (AffineScheme.ofHom g)), ⊤) : Type u))
    (CommRingCat.Hom.hom
      (Scheme.Hom.appTop (InducedCategory.Hom.hom (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)))))

Tactic:
rw [← this, CommRingCat.hom_comp, hP'.cancel_right_isIso, ← pushoutIsoUnopPullback_inl_hom,
    CommRingCat.hom_comp, hP'.cancel_right_isIso]

Premises used: RingHom.RespectsIso.cancel_right_isIso, CommRingCat.hom_comp, CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
this :
  Eq (α := Γ((AffineScheme.of X).obj, ⊤) ⟶ Γ((pullback (AffineScheme.ofHom f) (AffineScheme.ofHom g)).obj, ⊤))
    (CategoryStruct.comp (Y :=
      Opposite.unop
        (pullback (X := Opposite.op Γ((AffineScheme.of X).obj, ⊤)) (Y := Opposite.op Γ((AffineScheme.of Y).obj, ⊤))
          (Z := Opposite.op Γ((AffineScheme.of S).obj, ⊤))
          (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f))))
          (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g))))))
      (Quiver.Hom.unop
        (pullback.fst (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f))))
          (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g))))))
      (Quiver.Hom.unop
        (Iso.hom
          (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f)
            (AffineScheme.ofHom g)))))
    (Scheme.Hom.appTop (InducedCategory.Hom.hom (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))))
⊢ P (R := (↑Γ(X, ⊤) : Type u)) (S :=
    (↑(pushout (X := Γ((AffineScheme.of S).obj, ⊤)) (Y := Γ((AffineScheme.of X).obj, ⊤)) (Z :=
          Γ((AffineScheme.of Y).obj, ⊤)) (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f)))
          (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g)))) :
      Type u))
    (CommRingCat.Hom.hom
      (pushout.inl (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f)))
        (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g)))))

Tactic:
hP.pushout_inl hP' _ _ H

Premises used: RingHom.IsStableUnderBaseChange.pushout_inl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
this :
  Eq (α := Γ((AffineScheme.of X).obj, ⊤) ⟶ Γ((pullback (AffineScheme.ofHom f) (AffineScheme.ofHom g)).obj, ⊤))
    (CategoryStruct.comp (Y :=
      Opposite.unop
        (pullback (X := Opposite.op Γ((AffineScheme.of X).obj, ⊤)) (Y := Opposite.op Γ((AffineScheme.of Y).obj, ⊤))
          (Z := Opposite.op Γ((AffineScheme.of S).obj, ⊤))
          (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f))))
          (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g))))))
      (Quiver.Hom.unop
        (pullback.fst (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f))))
          (Quiver.Hom.op (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g))))))
      (Quiver.Hom.unop
        (Iso.hom
          (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f)
            (AffineScheme.ofHom g)))))
    (Scheme.Hom.appTop (InducedCategory.Hom.hom (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))))
⊢ P (R := (↑Γ(X, ⊤) : Type u)) (S :=
    (↑(pushout (X := Γ((AffineScheme.of S).obj, ⊤)) (Y := Γ((AffineScheme.of X).obj, ⊤)) (Z :=
          Γ((AffineScheme.of Y).obj, ⊤)) (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f)))
          (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g)))) :
      Type u))
    (CommRingCat.Hom.hom
      (pushout.inl (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom f)))
        (Scheme.Hom.appTop (InducedCategory.Hom.hom (AffineScheme.ofHom g)))))

Tactic:
exact hP.pushout_inl hP' _ _ H

Premises used: RingHom.IsStableUnderBaseChange.pushout_inl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ {X Y Z : Scheme.{u}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z],
    sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)
h₃ :
  ∀ {X Y Z : Scheme.{u}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y],
    sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)
⊢ (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso

Tactic:
apply AffineTargetMorphismProperty.respectsIso_mk

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst : IsAffine Z
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
h₂ :
  ∀
    (this :
      IsIso (X := Γ(Y, e.hom ''ᵁ (↑U : X.Opens))) (Scheme.Hom.appLE e.hom (e.hom ''ᵁ (↑U : X.Opens)) (↑U : X.Opens) ⋯)),
    P (R := (↑Γ(Z, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ (↑U : X.Opens) ⋯))
⊢ P (R := (↑Γ(Z, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ (↑U : X.Opens) ⋯))

Tactic:
have : IsIso (e.hom.appLE (e.hom ''ᵁ U) U.1 (e.hom.preimage_image_eq _).ge) :=
      inferInstanceAs (IsIso (e.hom.app _ ≫
        X.presheaf.map (eqToHom (e.hom.preimage_image_eq _).symm).op))
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst : IsAffine Z
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
this : IsIso (X := Γ(Y, e.hom ''ᵁ (↑U : X.Opens))) (Scheme.Hom.appLE e.hom (e.hom ''ᵁ (↑U : X.Opens)) (↑U : X.Opens) ⋯)
h₂ :
  P (R := (↑Γ(Z, ⊤) : Type u)) (S := (↑Γ(Y, e.hom ''ᵁ (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (e.hom ''ᵁ (↑U : X.Opens)) ⋯))
⊢ P (R := (↑Γ(Z, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ (↑U : X.Opens) ⋯))

Tactic:
rw [← Scheme.Hom.appLE_comp_appLE _ _ ⊤ (e.hom ''ᵁ U) U.1 le_top (e.hom.preimage_image_eq _).ge,
      CommRingCat.hom_comp, h₁.cancel_right_isIso]

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, Eq.ge, RingHom.RespectsIso.cancel_right_isIso, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, CommRingCat.hom_comp, le_top, Top.top, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE, Subtype.val, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst : IsAffine Z
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
this : IsIso (X := Γ(Y, e.hom ''ᵁ (↑U : X.Opens))) (Scheme.Hom.appLE e.hom (e.hom ''ᵁ (↑U : X.Opens)) (↑U : X.Opens) ⋯)
⊢ P (R := (↑Γ(Z, ⊤) : Type u)) (S := (↑Γ(Y, e.hom ''ᵁ (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (e.hom ''ᵁ (↑U : X.Opens)) ⋯))

Tactic:
H ⟨_, U.prop.image_of_isOpenImmersion e.hom⟩

Premises used: AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, Subtype.mk, Subtype.prop, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst : IsAffine Z
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
this : IsIso (X := Γ(Y, e.hom ''ᵁ (↑U : X.Opens))) (Scheme.Hom.appLE e.hom (e.hom ''ᵁ (↑U : X.Opens)) (↑U : X.Opens) ⋯)
⊢ P (R := (↑Γ(Z, ⊤) : Type u)) (S := (↑Γ(Y, e.hom ''ᵁ (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (e.hom ''ᵁ (↑U : X.Opens)) ⋯))

Tactic:
exact H ⟨_, U.prop.image_of_isOpenImmersion e.hom⟩

Premises used: AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, Subtype.mk, Subtype.prop, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst : IsAffine Y
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
h₂ :
  P (R := (↑Γ(Y, e.hom ⁻¹ᵁ ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f (e.hom ⁻¹ᵁ ⊤) (↑U : X.Opens) ⋯))
⊢ P (R := (↑Γ(Z, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ e.hom) ⊤ (↑U : X.Opens) ⋯))

Tactic:
rw [Scheme.Hom.comp_appLE, CommRingCat.hom_comp, h₁.cancel_left_isIso]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_appLE, CommRingCat.hom_comp, RingHom.RespectsIso.cancel_left_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst : IsAffine Y
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
⊢ P (R := (↑Γ(Y, e.hom ⁻¹ᵁ ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f (e.hom ⁻¹ᵁ ⊤) (↑U : X.Opens) ⋯))

Tactic:
H U

Premises used: Set.Mem, Set.univ, setOf, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst : IsAffine Y
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
⊢ P (R := (↑Γ(Y, e.hom ⁻¹ᵁ ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f (e.hom ⁻¹ᵁ ⊤) (↑U : X.Opens) ⋯))

Tactic:
exact H U
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
⊢ (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso

Tactic:
letI := sourceAffineLocally_respectsIso P h
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
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
dsimp :
  (∀ (U_1 : (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u)),
      P (R := (↑Γ((↑U : Scheme), ⊤) : Type u)) (S :=
        (↑Γ((↑(f ⁻¹ᵁ U) : Scheme), (↑U_1 : (↑(f ⁻¹ᵁ U) : Scheme).Opens)) : Type u))
        (CommRingCat.Hom.hom (Hom.appLE (f ∣_ U) ⊤ (↑U_1 : (↑(f ⁻¹ᵁ U) : Scheme).Opens) ⋯))) ↔
    ∀ (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ U),
      P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) e))
⊢ sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ∣_ U) ↔
    ∀ (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ U),
      P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) e))

Tactic:
dsimp only [sourceAffineLocally]

Premises used: AlgebraicGeometry.sourceAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
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
simp :
  (∀ (U_1 : (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u)),
      P (R := (↑Γ((↑U : Scheme), ⊤) : Type u)) (S :=
        (↑Γ((↑(f ⁻¹ᵁ U) : Scheme), (↑U_1 : (↑(f ⁻¹ᵁ U) : Scheme).Opens)) : Type u))
        (CommRingCat.Hom.hom (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ (↑U_1 : (↑(f ⁻¹ᵁ U) : Scheme).Opens)) ⋯))) ↔
    ∀ (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ U),
      P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) e))
⊢ (∀ (U_1 : (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u)),
      P (R := (↑Γ((↑U : Scheme), ⊤) : Type u)) (S :=
        (↑Γ((↑(f ⁻¹ᵁ U) : Scheme), (↑U_1 : (↑(f ⁻¹ᵁ U) : Scheme).Opens)) : Type u))
        (CommRingCat.Hom.hom (Hom.appLE (f ∣_ U) ⊤ (↑U_1 : (↑(f ⁻¹ᵁ U) : Scheme).Opens) ⋯))) ↔
    ∀ (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ U),
      P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) e))

Tactic:
simp only [morphismRestrict_appLE]

Premises used: AlgebraicGeometry.morphismRestrict_appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
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
rw :
  (∀ (a : (↑X.affineOpens : Type u)) (b : (↑a : X.Opens) ≤ f ⁻¹ᵁ U),
      P (R := (↑Γ((↑U : Scheme), ⊤) : Type u)) (S :=
        (↑Γ((↑(f ⁻¹ᵁ U) : Scheme),
              (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                      (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                        (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                    (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) a b)) :
                (↑(f ⁻¹ᵁ U) : Scheme).Opens)) :
          Type u))
        (CommRingCat.Hom.hom
          (Hom.appLE f (U.ι ''ᵁ ⊤)
            ((f ⁻¹ᵁ U).ι ''ᵁ
              (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                      (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                        (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                    (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) a b)) :
                (↑(f ⁻¹ᵁ U) : Scheme).Opens))
            ⋯))) ↔
    ∀ (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ U),
      P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) e))
⊢ (∀ (U_1 : (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u)),
      P (R := (↑Γ((↑U : Scheme), ⊤) : Type u)) (S :=
        (↑Γ((↑(f ⁻¹ᵁ U) : Scheme), (↑U_1 : (↑(f ⁻¹ᵁ U) : Scheme).Opens)) : Type u))
        (CommRingCat.Hom.hom (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ (↑U_1 : (↑(f ⁻¹ᵁ U) : Scheme).Opens)) ⋯))) ↔
    ∀ (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ U),
      P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) e))

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

Premises used: AlgebraicGeometry.affineOpensRestrict, Equiv.forall_congr_left, Subtype.forall, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
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 : Type u)) (b : (↑a : X.Opens) ≤ f ⁻¹ᵁ U),
      P (R := (↑Γ((↑U : Scheme), ⊤) : Type u)) (S :=
        (↑Γ((↑(f ⁻¹ᵁ U) : Scheme),
              (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                      (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                        (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                    (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) a b)) :
                (↑(f ⁻¹ᵁ U) : Scheme).Opens)) :
          Type u))
        (CommRingCat.Hom.hom
          (Hom.appLE f (U.ι ''ᵁ ⊤)
            ((f ⁻¹ᵁ U).ι ''ᵁ
              (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                      (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                        (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                    (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) a b)) :
                (↑(f ⁻¹ᵁ U) : Scheme).Opens))
            ⋯))) ↔
    ∀ (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ U),
      P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) e))

Tactic:
forall₂_congr fun V h ↦ ?_

Premises used: Set.Mem, forall₂_congr
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
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
refine :
  ∀ (V : (↑X.affineOpens : Type u)) (h : (↑V : X.Opens) ≤ f ⁻¹ᵁ U),
    P (R := (↑Γ((↑U : Scheme), ⊤) : Type u)) (S :=
        (↑Γ((↑(f ⁻¹ᵁ U) : Scheme),
              (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                      (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                        (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                    (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) V h)) :
                (↑(f ⁻¹ᵁ U) : Scheme).Opens)) :
          Type u))
        (CommRingCat.Hom.hom
          (Hom.appLE f (U.ι ''ᵁ ⊤)
            ((f ⁻¹ᵁ U).ι ''ᵁ
              (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                      (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                        (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                    (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) V h)) :
                (↑(f ⁻¹ᵁ U) : Scheme).Opens))
            ⋯)) ↔
      P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) h))
⊢ (∀ (a : (↑X.affineOpens : Type u)) (b : (↑a : X.Opens) ≤ f ⁻¹ᵁ U),
      P (R := (↑Γ((↑U : Scheme), ⊤) : Type u)) (S :=
        (↑Γ((↑(f ⁻¹ᵁ U) : Scheme),
              (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                      (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                        (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                    (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) a b)) :
                (↑(f ⁻¹ᵁ U) : Scheme).Opens)) :
          Type u))
        (CommRingCat.Hom.hom
          (Hom.appLE f (U.ι ''ᵁ ⊤)
            ((f ⁻¹ᵁ U).ι ''ᵁ
              (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                      (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                        (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                    (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) a b)) :
                (↑(f ⁻¹ᵁ U) : Scheme).Opens))
            ⋯))) ↔
    ∀ (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ U),
      P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) e))

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

Premises used: forall₂_congr
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
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 : Type u)
h : (↑V : X.Opens) ≤ f ⁻¹ᵁ U
⊢ Eq (α := { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })
    ((affineOpensRestrict (f ⁻¹ᵁ U) :
          (a : (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u)) →
            { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })
        (((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
            (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
              (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
          (Subtype.mk (p := fun (V : (↑X.affineOpens : Type u)) ↦ (↑V : X.Opens) ≤ f ⁻¹ᵁ U) V h)) :
      { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })
    (Subtype.mk (p := fun (V : (↑X.affineOpens : Type u)) ↦ (↑V : X.Opens) ≤ f ⁻¹ᵁ U) V h :
      { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })

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