awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
⊢ Eq (α := Set ↥Y) (Set.image (α := ↥X) (⇑f) Set.univ) (Set.univ ∩ Set.range (ι := ↥X) ⇑f)
have h : Eq (α := Set ↥Y) (Set.image (α := ↥X) (⇑f) Set.univ) (Set.range (ι := ↥X) ⇑f)
Tactic: rw [Set.univ_inter, Set.image_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
h : Eq (α := Set ↥Y) (Set.image (α := ↥X) (⇑f) Set.univ) (Set.range (ι := ↥X) ⇑f)
⊢ Eq (α := Set ↥Y) (Set.image (α := ↥X) (⇑f) Set.univ) (Set.univ ∩ Set.range (ι := ↥X) ⇑f)
have h₁ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥X) ⇑f)
Tactic: rw [Set.univ_inter, Set.image_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
inst : IrreducibleSpace.{u_1} ↥X
x : ↥X
⊢ Algebra (↑(X.presheaf.stalk x) : Type u_1) (↑X.functionField : Type u_1)
have i : (↑(X.presheaf.stalk x) : Type u_1) →+* (↑X.functionField : Type u_1)
Tactic: apply RingHom.toAlgebra
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
inst : IrreducibleSpace.{u_1} ↥X
U : X.Opens
x : ↥U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ IsScalarTower.{u_1, u_1, u_1} (↑Γ(X, U) : Type u_1) (↑(X.presheaf.stalk (↑x : ↥X)) : Type u_1)
    (↑X.functionField : Type u_1)
have h : Eq.{u_1 + 1} (α := (↑Γ(X, U) : Type u_1) →+* (↑X.functionField : Type u_1))
  (algebraMap (↑Γ(X, U) : Type u_1) (↑X.functionField : Type u_1))
  (@RingHom.comp _ (↑(X.presheaf.stalk (↑x : ↥X)) : Type u_1) _ _ Semiring.toNonAssocSemiring _
    (algebraMap (↑(X.presheaf.stalk (↑x : ↥X)) : Type u_1) (↑X.functionField : Type u_1))
    (algebraMap (↑Γ(X, U) : Type u_1) (↑(X.presheaf.stalk (↑x : ↥X)) : Type u_1)))
Tactic: apply IsScalarTower.of_algebraMap_eq'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
inst : IrreducibleSpace.{u_1} ↥X
U : X.Opens
x : ↥U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ Eq (α := (↑Γ(X, U) : Type u_1) →+* (↑X.functionField : Type u_1)) (CommRingCat.Hom.hom (X.germToFunctionField U))
    (RingHom.comp (CommRingCat.Hom.hom (X.presheaf.stalkSpecializes ⋯))
      (CommRingCat.Hom.hom (X.presheaf.germ U (↑x : ↥X) ⋯)))
have h : Eq (α := (↑(X.presheaf.obj (op U)) : Type u_1) →+* (↑X.functionField : Type u_1))
  (CommRingCat.Hom.hom (X.germToFunctionField U))
  (CommRingCat.Hom.hom (X.presheaf.germ U (↑x : ↥X) sorry ≫ X.presheaf.stalkSpecializes sorry))
Tactic: change _ = (X.presheaf.germ U x x.2 ≫ _).hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
inst : IrreducibleSpace.{u_1} ↥X
U : X.Opens
x : ↥U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ Eq (α := (↑(X.presheaf.obj (op U)) : Type u_1) →+* (↑X.functionField : Type u_1))
    (CommRingCat.Hom.hom (X.germToFunctionField U))
    (CommRingCat.Hom.hom (X.presheaf.germ U (↑x : ↥X) ⋯ ≫ X.presheaf.stalkSpecializes ⋯))
have h : Eq (α := (↑(X.presheaf.obj (op U)) : Type u_1) →+* (↑X.functionField : Type u_1))
  (CommRingCat.Hom.hom (X.germToFunctionField U)) (CommRingCat.Hom.hom (X.presheaf.germ U (genericPoint ↥X) sorry))
Tactic: rw [X.presheaf.germ_stalkSpecializes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
⊢ (↑R : Type u) →+* (↑(Spec R).functionField : Type u)
have f : R.Hom (Spec R).functionField
Tactic: apply CommRingCat.Hom.hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
R : CommRingCat
inst : IsDomain.{u_1} (↑R : Type u_1)
⊢ Eq.{u_1 + 1} (α := ↥(Spec R)) (genericPoint ↥(Spec R)) ⊥
have apply : IsGenericPoint.{u_1} (α := ↥(Spec R)) ⊥ Set.univ
Tactic: apply (genericPoint_spec (Spec R)).eq
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
R : CommRingCat
inst : IsDomain.{u_1} (↑R : Type u_1)
⊢ Eq (α := Set ↥(Spec R)) (closure {⊥}) Set.univ
have rw : Eq (α := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus (↑(PrimeSpectrum.asIdeal ⊥) : Set (↑R : Type u_1))) Set.univ
Tactic: rw [← PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, PrimeSpectrum.vanishingIdeal_singleton]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
R : CommRingCat
inst : IsDomain.{u_1} (↑R : Type u_1)
⊢ Eq (α := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus (↑(PrimeSpectrum.asIdeal ⊥) : Set (↑R : Type u_1))) Set.univ
have rw : Eq (α := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus (↑(PrimeSpectrum.asIdeal ⊥) : Set (↑R : Type u_1)))
  (PrimeSpectrum.zeroLocus {0})
Tactic: rw [← PrimeSpectrum.zeroLocus_singleton_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
⊢ IsFractionRing.{u, u} (↑R : Type u) (↑(Spec R).functionField : Type u)
have a : IsFractionRing.{u, u} (↑R : Type u) (↑(Spec R).functionField : Type u) ↔
  IsLocalization.AtPrime.{u, u} (R := (↑R : Type u))
    (↑(Presheaf.stalk (X := PrimeSpectrum.Top (↑R : Type u)) (Sheaf.presheaf (Spec.structureSheaf (↑R : Type u)))
          (genericPoint ↥(Spec R))) :
      Type u)
    (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R)))
Tactic: convert! StructureSheaf.IsLocalization.to_stalk R (genericPoint (Spec R))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
⊢ IsLocalization.{u, u} (R := (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) (↑(Spec R).functionField : Type u) ↔
    IsLocalization.{u, u} (R := (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R))))
      (↑(Presheaf.stalk (X := PrimeSpectrum.Top (↑R : Type u)) (Sheaf.presheaf (Spec.structureSheaf (↑R : Type u)))
            (genericPoint ↥(Spec R))) :
        Type u)
have a : IsLocalization.{u, u} (R := (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) (↑(Spec R).functionField : Type u) =
  IsLocalization.{u, u} (R := (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R))))
    (↑(Presheaf.stalk (X := PrimeSpectrum.Top (↑R : Type u)) (Sheaf.presheaf (Spec.structureSheaf (↑R : Type u)))
          (genericPoint ↥(Spec R))) :
      Type u)
Tactic: apply Eq.to_iff
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
⊢ IsLocalization.{u, u} (R := (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) (↑(Spec R).functionField : Type u) =
    IsLocalization.{u, u} (R := (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R))))
      (↑(Presheaf.stalk (X := PrimeSpectrum.Top (↑R : Type u)) (Sheaf.presheaf (Spec.structureSheaf (↑R : Type u)))
            (genericPoint ↥(Spec R))) :
        Type u)
have a : Eq.{u + 1} (α := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u))
  (Ideal.primeCompl (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R))))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
⊢ Eq.{u + 1} (α := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u))
    (Ideal.primeCompl (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R))))
have a : Eq.{u + 1} (α := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥))
Tactic: rw [genericPoint_eq_bot_of_affine]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
⊢ Eq.{u + 1} (α := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥))
have a : ∀ (x : (↑R : Type u)),
  Membership.mem (γ := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) x ↔
    Membership.mem (γ := Submonoid (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ Eq (α := PrimeSpectrum (↑Γ(X, U) : Type u_1))
    (hU.isoSpec.hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) ⋯) : ↥(Spec Γ(X, U)))
    (genericPoint ↥(Spec Γ(X, U)) : ↥(Spec Γ(X, U)))
have h₁ : PrimeSpectrum (↑Γ(X, U) : Type u_1) = ↥(Spec (X.presheaf.obj (op U))) →
  Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) sorry = genericPoint ↥(↑U : Scheme)
Tactic: convert!
    genericPoint_eq_of_isOpenImmersion
      (U.toScheme.isoSpec.hom ≫ Spec.map (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top).op))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
e_1 : PrimeSpectrum (↑Γ(X, U) : Type u_1) = ↥(Spec (X.presheaf.obj (op U)))
⊢ Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) ⋯ = genericPoint ↥(↑U : Scheme)
have h₁ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) sorry) : ↥X) = (↑(genericPoint ↥(↑U : Scheme)) : ↥X)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ IsLocalization.{u_1, u_1} (R := (↑Γ(X, U) : Type u_1)) (nonZeroDivisors (↑Γ(X, U) : Type u_1))
    (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u_1)
have h : nonZeroDivisors (↑Γ(X, U) : Type u_1) =
  (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) sorry)).asIdeal.primeCompl
Tactic: convert!
    hU.isLocalization_stalk
      ⟨genericPoint X,
        (((genericPoint_spec X).mem_open_set_iff U.isOpen).mpr (by simpa using ‹Nonempty U›))⟩
    using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ nonZeroDivisors (↑Γ(X, U) : Type u_1) =
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) ⋯)).asIdeal.primeCompl
have h : Eq.{u_1 + 1} (α := Submonoid (↑Γ(X, U) : Type u_1)) (nonZeroDivisors (↑Γ(X, U) : Type u_1))
  (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥))
Tactic: rw [hU.primeIdealOf_genericPoint, genericPoint_eq_bot_of_affine]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ Eq.{u_1 + 1} (α := Submonoid (↑Γ(X, U) : Type u_1)) (nonZeroDivisors (↑Γ(X, U) : Type u_1))
    (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥))
have h : ∀ (x : (↑Γ(X, U) : Type u_1)),
  Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (nonZeroDivisors (↑Γ(X, U) : Type u_1)) x ↔
    Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
⊢ X.toΓSpecFun ⁻¹' (↑(basicOpen r) : Set (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))) =
    (↑(X.toRingedSpace.basicOpen r) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))
have h : ∀ (x : (↑X.toTopCat : Type u)),
  x ∈ X.toΓSpecFun ⁻¹' (↑(basicOpen r) : Set (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))) ↔
    x ∈ (↑(X.toRingedSpace.basicOpen r) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
x : (↑X.toTopCat : Type u)
⊢ Membership.mem (γ := Opens (PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u))) (basicOpen r) (X.toΓSpecFun x) ↔
    x ∈ X.toRingedSpace.basicOpen r
have h : Membership.mem (γ := Opens (PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u))) (basicOpen r) (X.toΓSpecFun x) ↔
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.Γgerm x) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op ⊤)) : Type u)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
        r :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
Tactic: rw [X.toRingedSpace.mem_top_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
⊢ Continuous X.toΓSpecFun
have rw : ∀ (s : Set (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))),
  Membership.mem (γ := Set (Set (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))))
      (Set.range fun (r : (↑(Γ.obj (op X)) : Type u)) ↦
        (↑(basicOpen r) : Set (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))))
      s →
    IsOpen (X.toΓSpecFun ⁻¹' s)
Tactic: rw [isTopologicalBasis_basic_opens.continuous_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
⊢ IsOpen
    (X.toΓSpecFun ⁻¹'
      (fun (r : (↑(Γ.obj (op X)) : Type u)) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (↑(Γ.obj (op X)) : Type u)))) r)
have rw : IsOpen (↑(X.toRingedSpace.basicOpen r) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))
Tactic: rw [X.toΓSpec_preimage_basicOpen_eq r]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
⊢ IsUnit (M := (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.toToΓSpecMapBasicOpen r) :
          (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
        r :
      (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
have h : Eq (α := (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.toToΓSpecMapBasicOpen r) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
      r :
    (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
  ((CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
        (a : (↑(X.presheaf.obj (op (X.toRingedSpace.basicOpen r))) : Type u)) →
          (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.toRingedSpace.presheaf.map (homOfLE sorry).op) :
            (a : (↑(X.toRingedSpace.presheaf.obj (op ⊤)) : Type u)) →
              (↑(X.toRingedSpace.presheaf.obj (op (X.toRingedSpace.basicOpen r))) : Type u))
          r :
        (↑(X.toRingedSpace.presheaf.obj (op (X.toRingedSpace.basicOpen r))) : Type u)) :
    (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
Tactic: convert!
    (X.presheaf.map <| (eqToHom <| X.toΓSpecMapBasicOpen_eq r).op).hom.isUnit_map
      (X.toRingedSpace.isUnit_res_basicOpen r)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
⊢ Eq (α := (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.toToΓSpecMapBasicOpen r) :
          (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
        r :
      (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑(X.presheaf.obj (op (X.toRingedSpace.basicOpen r))) : Type u)) →
            (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.toRingedSpace.presheaf.map (homOfLE ⋯).op) :
              (a : (↑(X.toRingedSpace.presheaf.obj (op ⊤)) : Type u)) →
                (↑(X.toRingedSpace.presheaf.obj (op (X.toRingedSpace.basicOpen r))) : Type u))
            r :
          (↑(X.toRingedSpace.presheaf.obj (op (X.toRingedSpace.basicOpen r))) : Type u)) :
      (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
have h : Eq (α := (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.toToΓSpecMapBasicOpen r) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
      r :
    (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.toRingedSpace.presheaf.map ((homOfLE sorry).op ≫ Quiver.Hom.op (eqToHom sorry))) :
        (a : (↑(X.toRingedSpace.presheaf.obj (op ⊤)) : Type u)) →
          (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
      r :
    (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
Tactic: rw [← CommRingCat.comp_apply, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (hypothesis)
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
f :
  Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
        (structureSheaf (↑(Γ.obj (op X)) : Type u)))
      (op (basicOpen r)) ⟶
    X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
⊢ CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)) : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r)))) ≫
        f =
      X.toToΓSpecMapBasicOpen r ↔
    f = X.toΓSpecCApp r
have loc_inst : IsLocalization.Away r
  (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
          (structureSheaf (↑(Γ.obj (op X)) : Type u)))
        (op (basicOpen r))) :
    Type u)
Tactic: have loc_inst := IsLocalization.to_basicOpen (Γ.obj (op X)) r
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
f :
  Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
        (structureSheaf (↑(Γ.obj (op X)) : Type u)))
      (op (basicOpen r)) ⟶
    X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst :
  IsLocalization.Away r
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
            (structureSheaf (↑(Γ.obj (op X)) : Type u)))
          (op (basicOpen r))) :
      Type u)
⊢ CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)) : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r)))) ≫
        f =
      X.toToΓSpecMapBasicOpen r ↔
    f = X.toΓSpecCApp r
have refine : ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X := CommRingCat.of (↑(Γ.obj (op X)) : Type u))
      (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)) : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r)))) ≫
        f) =
    ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) (X.toToΓSpecMapBasicOpen r) ↔
  f = X.toΓSpecCApp r
Tactic: refine ConcreteCategory.ext_iff.trans ?_