awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R : CommRingCat
p : PrimeSpectrum (↑R : Type u_1)
⊢ Eq (α :=
    (↑(↑(Spec.locallyRingedSpaceObj (unop (op (Functor.obj (𝟭 CommRingCat) R)))).toPresheafedSpace : TopCat) :
      Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (PresheafedSpace.Hom.base
                (Hom.toHom (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec) ≫
              (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base) :
          (a :
              (↑(↑((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toPresheafedSpace : TopCat) :
                Type u_1)) →
            (↑(↑(Spec.locallyRingedSpaceObj (unop (op ((𝟭 CommRingCat).obj R)))).toPresheafedSpace : TopCat) :
              Type u_1))
        p :
      (↑(↑(Spec.locallyRingedSpaceObj (unop (op (Functor.obj (𝟭 CommRingCat) R)))).toPresheafedSpace : TopCat) :
        Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (Hom.toHom (𝟙 (Functor.obj (𝟭 LocallyRingedSpace) (Spec.toLocallyRingedSpace.obj (op R))))).base :
          (a :
              (↑(↑((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toPresheafedSpace : TopCat) :
                Type u_1)) →
            (↑(↑(Spec.locallyRingedSpaceObj (unop (op ((𝟭 CommRingCat).obj R)))).toPresheafedSpace : TopCat) :
              Type u_1))
        p :
      (↑(↑(Spec.locallyRingedSpaceObj (unop (op (Functor.obj (𝟭 CommRingCat) R)))).toPresheafedSpace : TopCat) :
        Type u_1))
have w : (TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
      (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
        PrimeSpectrum (↑R : Type u_1))
    (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
          C((↑(Spec.topObj R) : Type u_1),
            (↑(Spec.topObj
                  (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                    (ObjectProperty.FullSubcategory.obj (P :=
                      Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                      (structureSheaf (↑R : Type u_1)))
                    (op ⊤))) :
              Type u_1))) :
        (a : PrimeSpectrum (↑R : Type u_1)) →
          PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
      p) =
  p
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R : CommRingCat
p : PrimeSpectrum (↑R : Type u_1)
⊢ (TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
        (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
          PrimeSpectrum (↑R : Type u_1))
      (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
            C((↑(Spec.topObj R) : Type u_1),
              (↑(Spec.topObj
                    (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                        (structureSheaf (↑R : Type u_1)))
                      (op ⊤))) :
                Type u_1))) :
          (a : PrimeSpectrum (↑R : Type u_1)) →
            PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
        p) =
    p
have w : ∀ (x : (↑R : Type u_1)),
  Membership.mem (γ := Ideal (↑R : Type u_1))
      (asIdeal
        ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
            (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
              PrimeSpectrum (↑R : Type u_1))
          (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
                C((↑(Spec.topObj R) : Type u_1),
                  (↑(Spec.topObj
                        (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                          (ObjectProperty.FullSubcategory.obj (P :=
                            Presheaf.IsSheaf
                              (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                            (structureSheaf (↑R : Type u_1)))
                          (op ⊤))) :
                    Type u_1))) :
              (a : PrimeSpectrum (↑R : Type u_1)) →
                PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
            p)))
      x ↔
    x ∈ p.asIdeal
Tactic: refine PrimeSpectrum.ext (Ideal.ext fun x => ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R : CommRingCat
p : PrimeSpectrum (↑R : Type u_1)
x : (↑R : Type u_1)
⊢ Membership.mem (γ := Ideal (↑R : Type u_1))
      (asIdeal
        ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
            (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
              PrimeSpectrum (↑R : Type u_1))
          (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
                C((↑(Spec.topObj R) : Type u_1),
                  (↑(Spec.topObj
                        (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                          (ObjectProperty.FullSubcategory.obj (P :=
                            Presheaf.IsSheaf
                              (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                            (structureSheaf (↑R : Type u_1)))
                          (op ⊤))) :
                    Type u_1))) :
              (a : PrimeSpectrum (↑R : Type u_1)) →
                PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
            p)))
      x ↔
    x ∈ p.asIdeal
have w : Membership.mem (γ := Ideal (↑R : Type u_1))
    (asIdeal
      ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
          (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
            PrimeSpectrum (↑R : Type u_1))
        (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
              C((↑(Spec.topObj R) : Type u_1),
                (↑(Spec.topObj
                      (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                        (ObjectProperty.FullSubcategory.obj (P :=
                          Presheaf.IsSheaf
                            (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                          (structureSheaf (↑R : Type u_1)))
                        (op ⊤))) :
                  Type u_1))) :
            (a : PrimeSpectrum (↑R : Type u_1)) →
              PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
          p)))
    x ↔
  Membership.mem (α := (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1)) (γ :=
    Ideal (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1))
    (IsLocalRing.maximalIdeal (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1))
    ((algebraMap (↑R : Type u_1) (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1) :
          (a : (↑R : Type u_1)) → (↑((structureSheaf (↑R : Type u_1)).presheaf.stalk p) : Type u_1))
        x :
      (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1))
Tactic: rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff ((structureSheaf R).presheaf.stalk p)
        p.asIdeal x]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
⊢ Γ.rightOp.map (identityToΓSpec.app X) ≫ (NatIso.op SpecΓIdentity).inv.app (Γ.rightOp.obj X) = 𝟙 (Γ.rightOp.obj X)
have simp : Quiver.Hom.op ((identityToΓSpec.app X).c.app (op ⊤)) ≫ Quiver.Hom.op (toSpecΓ (X.presheaf.obj (op ⊤))) =
  𝟙 (op (X.presheaf.obj (op ⊤)))
Tactic: simp only [Functor.id_obj, Functor.rightOp_obj, Γ_obj, Functor.comp_obj,
      Spec.toLocallyRingedSpace_obj, Spec.locallyRingedSpaceObj_toSheafedSpace,
      Spec.sheafedSpaceObj_carrier, Spec.sheafedSpaceObj_presheaf, Functor.rightOp_map, Γ_map,
      Quiver.Hom.unop_op, NatIso.op_inv, NatTrans.op_app, SpecΓIdentity_inv_app]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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 ⟶
      Functor.obj
        (Functor.obj
          (pushforward CommRingCat
            (PresheafedSpace.Hom.base
              (Hom.toHom
                ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                    (a : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)) →
                      X ⟶ Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R)))
                  f))))
          X.presheaf)
        U)
    (CommRingCat.ofHom
        (algebraMap R
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf
                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(unop (op (CommRingCat.of R))) : Type u)) : Type u)))
              (structureSheafInType (↑(unop (op (CommRingCat.of R))) : Type u)
                (↑(unop (op (CommRingCat.of R))) : Type u)))
            U)) ≫
      NatTrans.app
        (PresheafedSpace.Hom.c
          (Hom.toHom
            ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                (a : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)) →
                  X ⟶ Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R)))
              f)))
        U)
    (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
have dsimp : 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))))
  (CommRingCat.ofHom
      (algebraMap R
        (Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u))) (structureSheafInType R R))
          U)) ≫
    NatTrans.app
      (PresheafedSpace.Hom.c
        (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)))
      U)
  (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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))))
    (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 ⋯)))
have 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 sorry)))
  (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: erw [← Adjunction.homEquiv_counit, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
⊢ IsIso adjunction.counit
have inst : ∀ (X : CommRingCatᵒᵖ), IsIso (adjunction.counit.app X)
Tactic: apply +allowSynthFailures NatIso.isIso_of_isIso_app
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R : CommRingCatᵒᵖ
⊢ IsIso (adjunction.counit.app R)
have inst : IsIso.{u_1, u_1 + 1} (X := (Scheme.Spec ⋙ Scheme.Γ.rightOp).obj R) (Quiver.Hom.op (Iso.inv (Scheme.ΓSpecIso (unop R))))
Tactic: rw [adjunction_counit_app]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (hypothesis)
Goal:
X : Scheme
⊢ Hom.appTop X.toSpecΓ = Iso.hom (ΓSpecIso Γ(X, ⊤))
have this : Γ.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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (hypothesis)
Goal:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op ≫ Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤))) = 𝟙 (op Γ(X, ⊤))
⊢ Hom.appTop X.toSpecΓ = Iso.hom (ΓSpecIso Γ(X, ⊤))
have this₁ : (Hom.appTop X.toSpecΓ).op = 𝟙 (op Γ(X, ⊤)) ≫ inv (Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤))))
Tactic: rw [← IsIso.eq_comp_inv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (hypothesis)
Goal:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op = 𝟙 (op Γ(X, ⊤)) ≫ inv (Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤))))
⊢ Hom.appTop X.toSpecΓ = Iso.hom (ΓSpecIso Γ(X, ⊤))
have this₁ : (Hom.appTop X.toSpecΓ).op = inv (Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤))))
Tactic: simp only [Category.id_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op = inv (Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤))))
⊢ Hom.appTop X.toSpecΓ = Iso.hom (ΓSpecIso Γ(X, ⊤))
have rw : (Hom.appTop X.toSpecΓ).op = Quiver.Hom.op (Iso.hom (ΓSpecIso Γ(X, ⊤)))
Tactic: rw [← Quiver.Hom.op_inj.eq_iff, this, ← op_inv, IsIso.Iso.inv_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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, ⊤)))
⊢ Hom.appTop X.toSpecΓ = Iso.hom (ΓSpecIso Γ(X, ⊤))
have rw₁ : Eq.{u + 1} (α := op Γ(X, ⊤) ⟶ op Γ(Spec Γ(X, ⊤), ⊤)) (inv (Quiver.Hom.op (Iso.inv (ΓSpecIso Γ(X, ⊤)))))
  (Quiver.Hom.op (Iso.hom (ΓSpecIso Γ(X, ⊤))))
Tactic: rw [← Quiver.Hom.op_inj.eq_iff, this, ← op_inv, IsIso.Iso.inv_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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, ⊤))))
⊢ Hom.appTop X.toSpecΓ = Iso.hom (ΓSpecIso Γ(X, ⊤))
have rw₂ : Eq.{u + 1} (α := op Γ(X, ⊤) ⟶ op Γ(Spec Γ(X, ⊤), ⊤)) (Quiver.Hom.op (inv (Iso.inv (ΓSpecIso Γ(X, ⊤)))))
  (Quiver.Hom.op (Iso.hom (ΓSpecIso Γ(X, ⊤))))
Tactic: rw [← Quiver.Hom.op_inj.eq_iff, this, ← op_inv, IsIso.Iso.inv_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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, ⊤))))
⊢ Hom.appTop X.toSpecΓ = Iso.hom (ΓSpecIso Γ(X, ⊤))
have rw₃ : Eq.{u + 1} (α := op Γ(X, ⊤) ⟶ op Γ(Spec Γ(X, ⊤), ⊤)) (Quiver.Hom.op (Iso.hom (ΓSpecIso Γ(X, ⊤))))
  (Quiver.Hom.op (Iso.hom (ΓSpecIso Γ(X, ⊤))))
Tactic: rw [← Quiver.Hom.op_inj.eq_iff, this, ← op_inv, IsIso.Iso.inv_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (hypothesis)
Goal:
R : CommRingCat
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
have this : Γ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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R : CommRingCat
this : (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
have rwa : ∀ (this : (Spec R).toSpecΓ = 𝟙 (Spec R) ≫ inv (Spec.map (Scheme.ΓSpecIso R).inv)),
  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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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Γ
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
have rwa₁ : ∀ (this : (Spec R).toSpecΓ = inv (Spec.map (Scheme.ΓSpecIso R).inv)),
  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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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Γ
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
have rwa₂ : ∀ (this : (Spec R).toSpecΓ = Spec.map (inv (Scheme.ΓSpecIso R).inv)),
  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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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Γ
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
have rwa₃ : ∀ (this : (Spec R).toSpecΓ = Spec.map (Scheme.ΓSpecIso R).hom), 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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Γ
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
have rwa₄ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R : CommRingCat
⊢ Spec.map (Scheme.ΓSpecIso R).inv ≫ (Spec R).toSpecΓ = 𝟙 (Spec Γ(Spec R, ⊤))
have rw : Spec.map (Scheme.ΓSpecIso R).inv ≫ Spec.map (Scheme.ΓSpecIso R).hom = 𝟙 (Spec Γ(Spec R, ⊤))
Tactic: rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.hom_inv_id, Spec.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R : CommRingCat
rw : Spec.map (Scheme.ΓSpecIso R).inv ≫ Spec.map (Scheme.ΓSpecIso R).hom = 𝟙 (Spec Γ(Spec R, ⊤))
⊢ Spec.map (Scheme.ΓSpecIso R).inv ≫ (Spec R).toSpecΓ = 𝟙 (Spec Γ(Spec R, ⊤))
have rw₁ : Spec.map ((Scheme.ΓSpecIso R).hom ≫ (Scheme.ΓSpecIso R).inv) = 𝟙 (Spec Γ(Spec R, ⊤))
Tactic: rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.hom_inv_id, Spec.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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, ⊤))
⊢ Spec.map (Scheme.ΓSpecIso R).inv ≫ (Spec R).toSpecΓ = 𝟙 (Spec Γ(Spec R, ⊤))
have rw₂ : Spec.map (𝟙 Γ(Spec R, ⊤)) = 𝟙 (Spec Γ(Spec R, ⊤))
Tactic: rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.hom_inv_id, Spec.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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, ⊤))
⊢ Spec.map (Scheme.ΓSpecIso R).inv ≫ (Spec R).toSpecΓ = 𝟙 (Spec Γ(Spec R, ⊤))
have rw₃ : 𝟙 (Spec Γ(Spec R, ⊤)) = 𝟙 (Spec Γ(Spec R, ⊤))
Tactic: rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.hom_inv_id, Spec.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R : CommRingCat
⊢ (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
have rw : Spec.map (Scheme.ΓSpecIso R).hom ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
Tactic: rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.inv_hom_id, Spec.map_id]