awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
R : Type u
inst : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens (↑(↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace : TopCat) : Type u))ᵒᵖ
erw :
  Eq (α :=
    CommRingCat.of R ⟶
      X.presheaf.obj
        (op
          (Functor.obj
            (Opens.map
              (PresheafedSpace.Hom.base
                (Hom.toHom
                  ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                      (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                        X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                    f))))
            (unop U))))
    (f.unop ≫
      CategoryTheory.Functor.map
        (Functor.obj
          (pushforward CommRingCat
            (PresheafedSpace.Hom.base
              (Hom.toHom
                ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                    (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                      X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                  f))))
          X.presheaf)
        (Quiver.Hom.op (homOfLE ⋯)))
    (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ Eq (α :=
    CommRingCat.of R ⟶
      X.presheaf.obj
        (op
          (Functor.obj
            (Opens.map
              (PresheafedSpace.Hom.base
                (Hom.toHom
                  ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                      (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                        X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                    f))))
            (unop U))))
    (Quiver.Hom.unop
        (Γ.rightOp.map
            ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                  X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
              f) ≫
          locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))) ≫
      CategoryTheory.Functor.map
        (Functor.obj
          (pushforward CommRingCat
            (PresheafedSpace.Hom.base
              (Hom.toHom
                ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                    (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                      X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                  f))))
          X.presheaf)
        (Quiver.Hom.op (homOfLE ⋯)))
    (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
erw [← Adjunction.homEquiv_counit, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CategoryTheory.Adjunction.homEquiv_counit
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
R : Type u
inst : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens (↑(↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace : TopCat) : Type u))ᵒᵖ
⊢ Eq (α :=
    CommRingCat.of R ⟶
      X.presheaf.obj
        (op
          (Functor.obj
            (Opens.map
              (PresheafedSpace.Hom.base
                (Hom.toHom
                  ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                      (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                        X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                    f))))
            (unop U))))
    (f.unop ≫
      CategoryTheory.Functor.map
        (Functor.obj
          (pushforward CommRingCat
            (PresheafedSpace.Hom.base
              (Hom.toHom
                ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                    (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                      X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                  f))))
          X.presheaf)
        (Quiver.Hom.op (homOfLE ⋯)))
    (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
R : Type u_1
inst : CommRing R
f g : X ⟶ Spec (CommRingCat.of R)
h :
  Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫ Scheme.Γ.map f.op =
    Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫ Scheme.Γ.map g.op
⊢ f = g

Tactic:
(ΓSpec.adjunction.homEquiv X (.op <| .of R)).symm.injective <| Opposite.unop_injective h

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.ΓSpec.adjunction, Opposite.op, CommRingCat.of, Opposite.unop_injective, CategoryTheory.Adjunction.homEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
R : CommRingCatᵒᵖ
f : op (Scheme.Γ.obj (op X)) ⟶ R
⊢ Eq (α := X ⟶ Scheme.Spec.obj R)
    ((adjunction.homEquiv X R : (a : Scheme.Γ.rightOp.obj X ⟶ R) → X ⟶ Scheme.Spec.obj R) f : X ⟶ Scheme.Spec.obj R)
    ({
        toLRSHom' :=
          (locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace R :
              (a : Γ.rightOp.obj X.toLocallyRingedSpace ⟶ R) → X.toLocallyRingedSpace ⟶ Spec.toLocallyRingedSpace.obj R)
            f } :
      X.Hom (Scheme.Spec.obj R))

Tactic:
rfl

Premises used: AlgebraicGeometry.LocallyRingedSpace.comp, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
R : CommRingCatᵒᵖ
f : X ⟶ Scheme.Spec.obj R
⊢ Eq (α := Scheme.Γ.rightOp.obj X ⟶ R)
    (((adjunction.homEquiv X R).symm : (a : X ⟶ Scheme.Spec.obj R) → Scheme.Γ.rightOp.obj X ⟶ R) f :
      Scheme.Γ.rightOp.obj X ⟶ R)
    ((Equiv.symm (locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace R) :
          (a : X.toLocallyRingedSpace ⟶ Spec.toLocallyRingedSpace.obj R) → Γ.rightOp.obj X.toLocallyRingedSpace ⟶ R)
        (Scheme.Hom.toLRSHom f) :
      Γ.rightOp.obj X.toLocallyRingedSpace ⟶ R)

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.op, AlgebraicGeometry.Spec.locallyRingedSpaceObj, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCatᵒᵖ
⊢ adjunction.counit.app R = locallyRingedSpaceAdjunction.counit.app R

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCatᵒᵖ
⊢ adjunction.counit.app R = Quiver.Hom.op (Iso.inv (Scheme.ΓSpecIso (unop R)))

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.op, AlgebraicGeometry.toSpecΓ, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
⊢ adjunction.unit.app X = X.toSpecΓ

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.toSpecΓ, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
⊢ IsIso locallyRingedSpaceAdjunction.counit

Tactic:
(NatIso.op SpecΓIdentity).isIso_inv

Premises used: CategoryTheory.Functor.op, Set.Mem, Quiver.Hom.op, CategoryTheory.Functor.comp, Quiver.Hom.unop, CategoryTheory.Functor.id, CategoryTheory.Iso.isIso_inv, CategoryTheory.NatTrans.op, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity, CategoryTheory.NatIso.op
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
inst : ∀ (X : CommRingCatᵒᵖ), IsIso (adjunction.counit.app X)
⊢ IsIso adjunction.counit

Tactic:
apply +allowSynthFailures NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCatᵒᵖ
inst :
  IsIso.{u_1, u_1 + 1} (X := (Scheme.Spec ⋙ Scheme.Γ.rightOp).obj R)
    (Quiver.Hom.op (Iso.inv (Scheme.ΓSpecIso (unop R))))
⊢ IsIso (adjunction.counit.app R)

Tactic:
rw [adjunction_counit_app]

Premises used: AlgebraicGeometry.ΓSpec.adjunction_counit_app
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCatᵒᵖ
⊢ IsIso.{u_1, u_1 + 1} (X := (Scheme.Spec ⋙ Scheme.Γ.rightOp).obj R)
    (Quiver.Hom.op (Iso.inv (Scheme.ΓSpecIso (unop R))))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
x : ↥X
⊢ Eq (α := ↥(Spec Γ(X, ⊤))) (X.toSpecΓ x : ↥(Spec Γ(X, ⊤)))
    ((Spec.map (X.presheaf.Γgerm x)) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) :
      ↥(Spec (X.presheaf.obj (op ⊤))))

Tactic:
rfl

Premises used: AlgebraicGeometry.LocallyRingedSpace.toΓSpecFun, rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ f ≫ Y.toSpecΓ = X.toSpecΓ ≫ Spec.map (Hom.appTop f)

Tactic:
ΓSpec.adjunction.unit.naturality f

Premises used: AlgebraicGeometry.Spec, Quiver.Hom.unop, CategoryTheory.Adjunction.unit, AlgebraicGeometry.ΓSpec.adjunction, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
⊢ Γ.rightOp.map (ΓSpec.adjunction.unit.app X) ≫ ΓSpec.adjunction.counit.app (Γ.rightOp.obj X) = 𝟙 (Γ.rightOp.obj X)

Tactic:
have := ΓSpec.adjunction.left_triangle_components X
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op ≫ Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤))) = 𝟙 (op Γ(X, ⊤))
⊢ (Hom.appTop X.toSpecΓ).op = 𝟙 (op Γ(X, ⊤)) ≫ inv (Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤))))

Tactic:
rw [← IsIso.eq_comp_inv] at this

Premises used: CategoryTheory.IsIso.eq_comp_inv
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op = 𝟙 (op Γ(X, ⊤)) ≫ inv (Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤))))
⊢ (Hom.appTop X.toSpecΓ).op = inv (Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤))))

Tactic:
simp only [Category.id_comp] at this

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op = inv (Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤))))
rw : (Hom.appTop X.toSpecΓ).op = Quiver.Hom.op (Iso.hom (ΓSpecIso Γ(X, ⊤)))
rw₁ :
  Eq.{u + 1} (α := op Γ(X, ⊤) ⟶ op Γ(Spec Γ(X, ⊤), ⊤)) (inv (Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤)))))
    (Quiver.Hom.op (Iso.hom (ΓSpecIso Γ(X, ⊤))))
rw₂ :
  Eq.{u + 1} (α := op Γ(X, ⊤) ⟶ op Γ(Spec Γ(X, ⊤), ⊤)) (Quiver.Hom.op (inv (Iso.inv (ΓSpecIso Γ(X, ⊤)))))
    (Quiver.Hom.op (Iso.hom (ΓSpecIso Γ(X, ⊤))))
rw₃ rw₄ :
  Eq.{u + 1} (α := op Γ(X, ⊤) ⟶ op Γ(Spec Γ(X, ⊤), ⊤)) (Quiver.Hom.op (Iso.hom (ΓSpecIso Γ(X, ⊤))))
    (Quiver.Hom.op (Iso.hom (ΓSpecIso Γ(X, ⊤))))
⊢ Hom.appTop X.toSpecΓ = Iso.hom (ΓSpecIso Γ(X, ⊤))

Tactic:
rw [← Quiver.Hom.op_inj.eq_iff, this, ← op_inv, IsIso.Iso.inv_inv]

Premises used: Quiver.Hom.op_inj, Function.Injective.eq_iff, CategoryTheory.IsIso.Iso.inv_inv, CategoryTheory.op_inv
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
⊢ ΓSpec.adjunction.unit.app (Scheme.Spec.obj (op R)) ≫ Scheme.Spec.map (ΓSpec.adjunction.counit.app (op R)) =
    𝟙 (Scheme.Spec.obj (op R))

Tactic:
have := ΓSpec.adjunction.right_triangle_components (op R)
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
this : (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
rwa :
  ∀ (this : (Spec R).toSpecΓ = 𝟙 (Spec R) ≫ inv (Spec.map (Scheme.ΓSpecIso R).inv)),
    Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
rwa₁ :
  ∀ (this : (Spec R).toSpecΓ = inv (Spec.map (Scheme.ΓSpecIso R).inv)),
    Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
rwa₂ :
  ∀ (this : (Spec R).toSpecΓ = Spec.map (inv (Scheme.ΓSpecIso R).inv)),
    Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
rwa₃ :
  ∀ (this : (Spec R).toSpecΓ = Spec.map (Scheme.ΓSpecIso R).hom), Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
rwa₄ rwa₅ rwa₆ rwa₇ :
  ∀ (this : Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ), Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Tactic:
rwa [← IsIso.eq_comp_inv, Category.id_comp, ← Spec.map_inv, IsIso.Iso.inv_inv, eq_comm] at this

Premises used: eq_comm, CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.IsIso.Iso.inv_inv, AlgebraicGeometry.Spec.map_inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
rw : Spec.map (Scheme.ΓSpecIso R).inv ≫ Spec.map (Scheme.ΓSpecIso R).hom = 𝟙 (Spec Γ(Spec R, ⊤))
rw₁ : Spec.map ((Scheme.ΓSpecIso R).hom ≫ (Scheme.ΓSpecIso R).inv) = 𝟙 (Spec Γ(Spec R, ⊤))
rw₂ : Spec.map (𝟙 Γ(Spec R, ⊤)) = 𝟙 (Spec Γ(Spec R, ⊤))
rw₃ rw₄ : 𝟙 (Spec Γ(Spec R, ⊤)) = 𝟙 (Spec Γ(Spec R, ⊤))
⊢ Spec.map (Scheme.ΓSpecIso R).inv ≫ (Spec R).toSpecΓ = 𝟙 (Spec Γ(Spec R, ⊤))

Tactic:
rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.hom_inv_id, Spec.map_id]

Premises used: AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.Spec.map_id, CategoryTheory.Iso.hom_inv_id, AlgebraicGeometry.Spec.map_comp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
rw : Spec.map (Scheme.ΓSpecIso R).hom ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
rw₁ : Spec.map ((Scheme.ΓSpecIso R).inv ≫ (Scheme.ΓSpecIso R).hom) = 𝟙 (Spec R)
rw₂ : Spec.map (𝟙 R) = 𝟙 (Spec R)
rw₃ rw₄ : 𝟙 (Spec R) = 𝟙 (Spec R)
⊢ (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)

Tactic:
rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.inv_hom_id, Spec.map_id]

Premises used: CategoryTheory.Iso.inv_hom_id, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.Spec.map_id, AlgebraicGeometry.Spec.map_comp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
r : (↑Γ(X, ⊤) : Type u)
rw :
  X.basicOpen (U := X.toSpecΓ ⁻¹ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop X.toSpecΓ) :
          (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
              (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
            r :
          (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))) =
    X.basicOpen r
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r

Tactic:
rw [← basicOpen_eq_of_affine, Scheme.preimage_basicOpen, ← Scheme.Hom.appTop]

Premises used: AlgebraicGeometry.Scheme.Hom.appTop, AlgebraicGeometry.basicOpen_eq_of_affine, AlgebraicGeometry.Scheme.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
r : (↑Γ(X, ⊤) : Type u)
e_f :
  (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Hom.appTop X.toSpecΓ) :
        (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
            (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
          r :
        (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) =
    r
⊢ X.basicOpen (U := X.toSpecΓ ⁻¹ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop X.toSpecΓ) :
          (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
              (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
            r :
          (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))) =
    X.basicOpen r

Tactic:
congr
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
r : (↑Γ(X, ⊤) : Type u)
e_f :
  (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(Spec Γ(X, ⊤), ⊤)) (Iso.hom (ΓSpecIso Γ(X, ⊤))) :
        (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
            (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
          r :
        (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) =
    r
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Hom.appTop X.toSpecΓ) :
        (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
            (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
          r :
        (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) =
    r

Tactic:
rw [Scheme.toSpecΓ_appTop]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_appTop
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
r : (↑Γ(X, ⊤) : Type u)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(Spec Γ(X, ⊤), ⊤)) (Iso.hom (ΓSpecIso Γ(X, ⊤))) :
        (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
            (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
          r :
        (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) =
    r

Tactic:
Iso.inv_hom_id_apply (C := CommRingCat) _ _

Premises used: CategoryTheory.Iso.inv_hom_id_apply
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
r : (↑Γ(X, ⊤) : Type u)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(Spec Γ(X, ⊤), ⊤)) (Iso.hom (ΓSpecIso Γ(X, ⊤))) :
        (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
            (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
          r :
        (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) =
    r

Tactic:
exact Iso.inv_hom_id_apply (C := CommRingCat) _ _

Premises used: CategoryTheory.Iso.inv_hom_id_apply
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
simp :
  (Scheme.ΓSpecIso B).inv ≫ Scheme.Hom.app (Spec.map φ.op.unop) ⊤ ≫ Scheme.Hom.app (ΓSpec.adjunction.unit.app X) ⊤ = φ
⊢ (Scheme.ΓSpecIso B).inv ≫
      Scheme.Hom.appTop
        ((ΓSpec.adjunction.homEquiv X (op B) : (a : Scheme.Γ.rightOp.obj X ⟶ op B) → X ⟶ Scheme.Spec.obj (op B)) φ.op) =
    φ

Tactic:
simp only [Adjunction.homEquiv_apply, Scheme.Spec_map, Opens.map_top, Scheme.Hom.comp_app]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_app, CategoryTheory.Adjunction.homEquiv_apply, AlgebraicGeometry.Scheme.Spec_map, TopologicalSpace.Opens.map_top
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
⊢ (Scheme.ΓSpecIso B).inv ≫ Scheme.Hom.app (Spec.map φ.op.unop) ⊤ ≫ Scheme.Hom.app (ΓSpec.adjunction.unit.app X) ⊤ = φ

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
rw :
  (Scheme.ΓSpecIso B).inv ≫
      Scheme.Hom.appTop
        ((ΓSpec.adjunction.homEquiv X (op B) : (a : Scheme.Γ.rightOp.obj X ⟶ op B) → X ⟶ Scheme.Spec.obj (op B)) φ.op) =
    φ
rw₁ rw₂ : φ = φ
⊢ Scheme.Hom.appTop
      ((ΓSpec.adjunction.homEquiv X (op B) : (a : Scheme.Γ.rightOp.obj X ⟶ op B) → X ⟶ Scheme.Spec.obj (op B)) φ.op) =
    (Scheme.ΓSpecIso B).hom ≫ φ

Tactic:
rw [← Iso.inv_comp_eq, ΓSpecIso_inv_ΓSpec_adjunction_homEquiv]

Premises used: CategoryTheory.Iso.inv_comp_eq, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : Scheme
U : X.Opens
⊢ Iso.hom (Scheme.ΓSpecIso Γ(X, U)) =
    Scheme.Hom.appTop (Spec.map U.topIso.inv) ≫ Scheme.Hom.appTop (↑U : Scheme).toSpecΓ ≫ U.topIso.hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
⊢ Spec.toLocallyRingedSpace.Full

Tactic:
Spec.fullyFaithfulToLocallyRingedSpace.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, AlgebraicGeometry.Spec.fullyFaithfulToLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
⊢ Spec.toLocallyRingedSpace.Faithful

Tactic:
Spec.fullyFaithfulToLocallyRingedSpace.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, AlgebraicGeometry.Spec.fullyFaithfulToLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
⊢ Scheme.Spec.Full

Tactic:
Spec.fullyFaithful.full

Premises used: AlgebraicGeometry.Spec.fullyFaithful, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
⊢ Scheme.Spec.Faithful

Tactic:
Spec.fullyFaithful.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, AlgebraicGeometry.Spec.fullyFaithful
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R S : CommRingCat
φ ψ : R ⟶ S
rw : Scheme.Spec.map φ.op = Scheme.Spec.map ψ.op ↔ map φ = map ψ
⊢ map φ = map ψ ↔ φ = ψ

Tactic:
rw [iff_comm, ← Quiver.Hom.op_inj.eq_iff, ← Scheme.Spec.map_injective.eq_iff]

Premises used: Quiver.Hom.op_inj, Function.Injective.eq_iff, iff_comm, AlgebraicGeometry.Scheme.Spec, CategoryTheory.Functor.map_injective
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R S : CommRingCat
φ ψ : R ⟶ S
⊢ Scheme.Spec.map φ.op = Scheme.Spec.map ψ.op ↔ map φ = map ψ

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R S : CommRingCat
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R ⟶ S) map

Tactic:
fun _ _ ↦ Spec.map_inj.mp

Premises used: Iff.mp, Function.Injective, AlgebraicGeometry.Spec.map_inj
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
ϕ : R ⟶ R
⊢ map ϕ = 𝟙 (Spec R) ↔ ϕ = 𝟙 R

Tactic:
simp [← map_inj]

Premises used: AlgebraicGeometry.Spec.map_inj
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ map (preimage f) = f

Tactic:
Scheme.Spec.map_preimage f

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.Spec.map, AlgebraicGeometry.Scheme.Spec, AlgebraicGeometry.Spec.preimage, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R S : CommRingCat
f : Spec R ⟶ Spec S
⊢ map (fullyFaithful.preimage f).unop = f

Tactic:
Spec.fullyFaithful.map_preimage _

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.Spec.map, AlgebraicGeometry.Spec.fullyFaithful, CategoryTheory.Functor.FullyFaithful.map_preimage
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R S : CommRingCat
φ : R ⟶ S
⊢ preimage (map φ) = φ

Tactic:
Spec.map_injective (Spec.map_preimage (Spec.map φ))

Premises used: AlgebraicGeometry.Spec.map_injective, AlgebraicGeometry.Spec.map, AlgebraicGeometry.Spec.map_preimage
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
h : map (preimage f) = f
⊢ ∃ (a : R ⟶ S), map a = f

Tactic:
use Spec.preimage f

Premises used: AlgebraicGeometry.Spec.preimage
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ map (preimage f) = f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
⊢ map (preimage (𝟙 (Spec R))) = map (𝟙 R)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R S T : CommRingCat
f : Spec R ⟶ Spec S
g : Spec S ⟶ Spec T
⊢ map (preimage (f ≫ g)) = map (preimage g ≫ preimage f)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
⊢ Γ.IsRightAdjoint

Tactic:
ΓSpec.locallyRingedSpaceAdjunction.rightOp.isRightAdjoint

Premises used: AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction, CategoryTheory.Adjunction.rightOp, CategoryTheory.Adjunction.isRightAdjoint