awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
h :
  Eq.{u_1 + 1} (α := Submonoid (↑Γ(X, U) : Type u_1)) (nonZeroDivisors (↑Γ(X, U) : Type u_1))
    (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥))
⊢ nonZeroDivisors (↑Γ(X, U) : Type u_1) =
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) ⋯)).asIdeal.primeCompl

Tactic:
rw [hU.primeIdealOf_genericPoint, genericPoint_eq_bot_of_affine]

Premises used: AlgebraicGeometry.genericPoint_eq_bot_of_affine, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
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
⊢ Eq.{u_1 + 1} (α := Submonoid (↑Γ(X, U) : Type u_1)) (nonZeroDivisors (↑Γ(X, U) : Type u_1))
    (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
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:
mem_nonZeroDivisors_iff_ne_zero

Premises used: Set.Mem, setOf, Set.singleton, mem_nonZeroDivisors_iff_ne_zero, Not
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
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:
exact mem_nonZeroDivisors_iff_ne_zero

Premises used: mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
x : ↥X
⊢ IsAffine.{u_1} (X.affineCover.X x)

Tactic:
AlgebraicGeometry.isAffine_Spec _

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.isAffine_Spec
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
x : ↥X
⊢ IsFractionRing.{u_1, u_1} (↑(X.presheaf.stalk x) : Type u_1) (↑X.functionField : Type u_1)

Tactic:
let U : X.Opens := (X.affineCover.f ((X.affineCover.idx x))).opensRange
  have hU : IsAffineOpen U := isAffineOpen_opensRange (X.affineCover.f _)
  let x : U := ⟨x, X.affineCover.covers x⟩
  have : Nonempty U := ⟨x⟩
  let M := (hU.primeIdealOf x).asIdeal.primeCompl
  have := hU.isLocalization_stalk x
  have := functionField_isFractionRing_of_isAffineOpen X U hU
  -- Porting note: the following two lines were not needed.
  let _hA := Presheaf.algebra_section_stalk X.presheaf x
  have := functionField_isScalarTower X U x
  .isFractionRing_of_isDomain_of_isLocalization M ↑(Presheaf.stalk X.presheaf x)
    (Scheme.functionField X)

Premises used: AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen, CategoryTheory.PreZeroHypercover.f, CommRingCat.carrier, AlgebraicGeometry.functionField_isScalarTower, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.Scheme.Cover.covers, TopCat.Presheaf.algebra_section_stalk, Nonempty.intro, TopCat.Presheaf.stalk, Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, IsFractionRing.isFractionRing_of_isDomain_of_isLocalization, AlgebraicGeometry.Scheme.functionField, AlgebraicGeometry.IsAffineOpen.primeIdealOf, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Ideal.primeCompl, AlgebraicGeometry.Scheme.Cover.idx, Subtype.val, AlgebraicGeometry.Scheme.affineCover, PrimeSpectrum.asIdeal, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
x : ↥X
⊢ IsDomain.{u_1} (↑(X.presheaf.stalk x) : Type u_1)

Tactic:
Function.Injective.isDomain _ (IsFractionRing.injective (X.presheaf.stalk x) (X.functionField))

Premises used: CommRingCat.carrier, IsFractionRing.injective, Function.Injective.isDomain, TopCat.Presheaf.stalk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.functionField, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
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))
⊢ X.toΓSpecFun ⁻¹' (↑(basicOpen r) : Set (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))) =
    (↑(X.toRingedSpace.basicOpen r) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
x : (↑X.toTopCat : Type u)
h :
  x ∈ X.toΓSpecFun ⁻¹' (↑(basicOpen r) : Set (PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u))) ↔
    x ∈ (↑(X.toRingedSpace.basicOpen r) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : 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:
dsimp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
x : (↑X.toTopCat : Type u)
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))
⊢ Membership.mem (γ := Opens (PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u))) (basicOpen r) (X.toΓSpecFun x) ↔
    x ∈ X.toRingedSpace.basicOpen r

Tactic:
rw [X.toRingedSpace.mem_top_basicOpen]

Premises used: AlgebraicGeometry.RingedSpace.mem_top_basicOpen, AlgebraicGeometry.LocallyRingedSpace.toRingedSpace
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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) ↔
    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:
notMem_prime_iff_unit_in_stalk ..

Premises used: AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, Set.Mem, setOf, Not
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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) ↔
    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:
exact notMem_prime_iff_unit_in_stalk ..

Premises used: AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
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)
⊢ Continuous X.toΓSpecFun

Tactic:
rw [isTopologicalBasis_basic_opens.continuous_iff]

Premises used: PrimeSpectrum.isTopologicalBasis_basic_opens, TopologicalSpace.IsTopologicalBasis.continuous_iff
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
rw : IsOpen (↑(X.toRingedSpace.basicOpen r) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))
⊢ IsOpen
    (X.toΓSpecFun ⁻¹'
      (fun (r : (↑(Γ.obj (op X)) : Type u)) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (↑(Γ.obj (op X)) : Type u)))) r)

Tactic:
rw [X.toΓSpec_preimage_basicOpen_eq r]

Premises used: AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
⊢ IsOpen (↑(X.toRingedSpace.basicOpen r) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))

Tactic:
(X.toRingedSpace.basicOpen r).2

Premises used: AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, AlgebraicGeometry.RingedSpace.basicOpen, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
⊢ IsOpen (↑(X.toRingedSpace.basicOpen r) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))

Tactic:
exact (X.toRingedSpace.basicOpen r).2

Premises used: AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, AlgebraicGeometry.RingedSpace.basicOpen, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
⊢ X.toΓSpecMapBasicOpen r = X.toRingedSpace.basicOpen r

Tactic:
Opens.ext (X.toΓSpec_preimage_basicOpen_eq r)

Premises used: TopologicalSpace.Opens.ext, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
⊢ IsUnit (M := (↑(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))

Tactic:
(X.presheaf.map <| (eqToHom <| X.toΓSpecMapBasicOpen_eq r).op).hom.isUnit_map
      (X.toRingedSpace.isUnit_res_basicOpen r)

Premises used: CommRingCat.Hom.hom, Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, RingHom.isUnit_map, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
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 ⋯))) :
          (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))
⊢ 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))

Tactic:
convert!
    (X.presheaf.map <| (eqToHom <| X.toΓSpecMapBasicOpen_eq r).op).hom.isUnit_map
      (X.toRingedSpace.isUnit_res_basicOpen r)

Premises used: CommRingCat.Hom.hom, Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, RingHom.isUnit_map, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
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 ⋯).op ≫ Quiver.Hom.op (eqToHom ⋯))) :
          (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))
⊢ 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))

Tactic:
rw [← CommRingCat.comp_apply, ← Functor.map_comp]

Premises used: CommRingCat.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.toRingedSpace.presheaf.map ((homOfLE ⋯).op ≫ Quiver.Hom.op (eqToHom ⋯))) :
          (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:
congr
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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))
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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

Tactic:
ConcreteCategory.ext_iff.trans ?_

Premises used: CategoryTheory.ConcreteCategory.ext_iff, Iff.trans
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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)
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
⊢ 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

Tactic:
refine ConcreteCategory.ext_iff.trans ?_

Premises used: CategoryTheory.ConcreteCategory.ext_iff, Iff.trans