awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ IsLocalization (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)
have inst : IsCompact.{u} (X := ↥X) (Opens.carrier ⊤)
Tactic: refine isLocalization_basicOpen_of_qcqs ?_ ?_ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
inst_2 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
inst : IsCompact.{u} (X := ↥X) (Opens.carrier ⊤)
⊢ IsLocalization (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)
have inst₁ : IsQuasiSeparated.{u} (α := ↥X) (Opens.carrier ⊤)
Tactic: refine isLocalization_basicOpen_of_qcqs ?_ ?_ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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))
⊢ P (S := (↑Γ(pullback f g, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))
have erw : P (R := (↑Γ(X, ⊤) : Type u)) (S := (↑Γ(pullback f g, ⊤) : Type u))
  (CommRingCat.Hom.hom
      (Scheme.Hom.appTop
        (CategoryStruct.comp (Y :=
          AffineScheme.forgetToScheme.obj
            (pullback (X := AffineScheme.of X) (Y := AffineScheme.of Y) (Z := AffineScheme.of S) (AffineScheme.ofHom f)
              (AffineScheme.ofHom g)))
          (Iso.inv (PreservesPullback.iso AffineScheme.forgetToScheme (AffineScheme.ofHom f) (AffineScheme.ofHom g)))
          (AffineScheme.forgetToScheme.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))))) :
    (↑Γ(X, ⊤) : Type u) →+* (↑Γ(pullback f g, ⊤) : Type u))
Tactic: erw [← PreservesPullback.iso_inv_fst AffineScheme.forgetToScheme (AffineScheme.ofHom f)
      (AffineScheme.ofHom g)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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))
⊢ P (R := (↑Γ(X, ⊤) : Type u)) (S := (↑Γ(pullback f g, ⊤) : Type u))
    (CommRingCat.Hom.hom
        (Scheme.Hom.appTop
          (CategoryStruct.comp (Y :=
            AffineScheme.forgetToScheme.obj
              (pullback (X := AffineScheme.of X) (Y := AffineScheme.of Y) (Z := AffineScheme.of S)
                (AffineScheme.ofHom f) (AffineScheme.ofHom g)))
            (Iso.inv (PreservesPullback.iso AffineScheme.forgetToScheme (AffineScheme.ofHom f) (AffineScheme.ofHom g)))
            (AffineScheme.forgetToScheme.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))))) :
      (↑Γ(X, ⊤) : Type u) →+* (↑Γ(pullback f g, ⊤) : Type u))
have rw : 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 [Scheme.Hom.comp_appTop, CommRingCat.hom_comp, hP'.cancel_right_isIso,
    AffineScheme.forgetToScheme_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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))
⊢ 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)))))
have have : ∀
  (this :
    Eq (α :=
      Opposite.unop (AffineScheme.Γ.rightOp.obj (AffineScheme.of X)) ⟶
        Opposite.unop
          (AffineScheme.Γ.rightOp.obj
            (pullback (X := AffineScheme.of X) (Y := AffineScheme.of Y) (Z := AffineScheme.of S) (AffineScheme.ofHom f)
              (AffineScheme.ofHom g))))
      (Quiver.Hom.unop
        (CategoryStruct.comp (Y :=
          pullback (X := AffineScheme.Γ.rightOp.obj (AffineScheme.of X)) (Y :=
            AffineScheme.Γ.rightOp.obj (AffineScheme.of Y)) (Z := AffineScheme.Γ.rightOp.obj (AffineScheme.of S))
            (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom f)) (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom g)))
          (Iso.hom (PreservesPullback.iso AffineScheme.Γ.rightOp (AffineScheme.ofHom f) (AffineScheme.ofHom g)))
          (pullback.fst (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom f))
            (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom g)))))
      (Quiver.Hom.unop (AffineScheme.Γ.rightOp.map (pullback.fst (AffineScheme.ofHom f) (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: have := congr_arg Quiver.Hom.unop
      (PreservesPullback.iso_hom_fst AffineScheme.Γ.rightOp (AffineScheme.ofHom f)
        (AffineScheme.ofHom g))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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 :=
    (↑Γ(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)))))
have 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)))))
Tactic: rw [← this, CommRingCat.hom_comp, hP'.cancel_right_isIso, ← pushoutIsoUnopPullback_inl_hom,
    CommRingCat.hom_comp, hP'.cancel_right_isIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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
⊢ (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso
have 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)
Tactic: apply AffineTargetMorphismProperty.respectsIso_mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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)
⊢ (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso
have 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)
Tactic: apply AffineTargetMorphismProperty.respectsIso_mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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)
⊢ P (R := (↑Γ(Z, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ (↑U : X.Opens) ⋯))
have h₂ : ∀
  (this :
    IsIso (X := Γ(Y, e.hom ''ᵁ (↑U : X.Opens))) (Scheme.Hom.appLE e.hom (e.hom ''ᵁ (↑U : X.Opens)) (↑U : X.Opens) sorry)),
  P (R := (↑Γ(Z, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ (↑U : X.Opens) sorry))
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))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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 := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ (↑U : X.Opens) ⋯))
have 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)) sorry))
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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 := (↑Γ(Z, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ e.hom) ⊤ (↑U : X.Opens) ⋯))
have 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) sorry))
Tactic: rw [Scheme.Hom.comp_appLE, CommRingCat.hom_comp, h₁.cancel_left_isIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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
⊢ 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))
have 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) sorry))) ↔
  ∀ (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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
⊢ (∀ (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))
have 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)) sorry))) ↔
  ∀ (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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
⊢ (∀ (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))
have 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))
          sorry))) ↔
  ∀ (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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))
have 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))
          sorry)) ↔
    P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) h))
Tactic: refine forall₂_congr fun V h ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
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
⊢ 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))
have this : 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⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
⊢ AffineTargetMorphismProperty.IsLocal.{u} (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P)
have respectsIso : (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
respectsIso : (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso
⊢ AffineTargetMorphismProperty.IsLocal.{u} (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P)
have to_basicOpen : ∀ {X Y : Scheme.{u}} [inst : IsAffine Y] (f : X ⟶ Y) (r : (↑Γ(Y, ⊤) : Type u)),
  sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
    sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme))
      (f ∣_ Y.basicOpen r)
Tactic: constructor