awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
⊢ Iso.hom (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) ≫
      CommRingCat.ofHom
          (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
            (CommRingCat.Hom.hom f) ⋯) ≫
        (Spec.stalkIso S p).inv =
    Hom.stalkMap (Spec.map f) p

Tactic:
AlgebraicGeometry.localRingHom_comp_stalkIso f p

Premises used: AlgebraicGeometry.Spec.topObj, Set.Mem, MonoidHomClass.toMonoidHom, TopCat.Presheaf.stalk, CategoryTheory.Limits.colimit, MulEquiv.toMonoidHom, RingHomClass.toRingHom, RingEquiv.toRingHom, AlgebraicGeometry.PrimeSpectrum.Top, AlgebraicGeometry.Scheme.Hom.stalkMap, AlgebraicGeometry.structurePresheafInCommRingCat, OreLocalization.liftExpand, AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap, AlgebraicGeometry.localRingHom_comp_stalkIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R_1 S_1 : CommRingCat
f_1 : R_1 ⟶ S_1
p_1 : PrimeSpectrum (↑S_1 : Type u)
x : PrimeSpectrum (↑R_1 : Type u)
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
rw :
  Iso.hom (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) ≫
      (Arrow.mk (X := CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal))
          (Y := CommRingCat.of (Localization.AtPrime p.asIdeal))
          (CommRingCat.ofHom
            (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
              (CommRingCat.Hom.hom f) ⋯))).hom =
    (Arrow.mk
          (Iso.hom (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) ≫
            CommRingCat.ofHom
                (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
                  (CommRingCat.Hom.hom f) ⋯) ≫
              (Spec.stalkIso S p).inv)).hom ≫
      (Spec.stalkIso S p).hom
⊢ Iso.hom (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) ≫
      (Arrow.mk (X := CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal))
          (Y := CommRingCat.of (Localization.AtPrime p.asIdeal))
          (CommRingCat.ofHom
            (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
              (CommRingCat.Hom.hom f) ⋯))).hom =
    (Arrow.mk (Hom.stalkMap (Spec.map f) p)).hom ≫ (Spec.stalkIso S p).hom

Tactic:
rw [← Scheme.localRingHom_comp_stalkIso]

Premises used: AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R_1 S_1 : CommRingCat
f_1 : R_1 ⟶ S_1
p_1 : PrimeSpectrum (↑S_1 : Type u)
x : PrimeSpectrum (↑R_1 : Type u)
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
⊢ Iso.hom (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) ≫
      (Arrow.mk (X := CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal))
          (Y := CommRingCat.of (Localization.AtPrime p.asIdeal))
          (CommRingCat.ofHom
            (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
              (CommRingCat.Hom.hom f) ⋯))).hom =
    (Arrow.mk
          (Iso.hom (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) ≫
            CommRingCat.ofHom
                (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
                  (CommRingCat.Hom.hom f) ⋯) ≫
              (Spec.stalkIso S p).inv)).hom ≫
      (Spec.stalkIso S p).hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h :
  ∀ (i : n),
    Eq (α := (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) f :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) g :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
this :
  Eq (α := MvPolynomial n ℤ →+* (↑R : Type (max u_1 v)))
    ((CommRingCat.Hom.hom f).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))
    ((CommRingCat.Hom.hom g).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))
hf :
  ∀ (x : ULift.{u_1, 0} ℤ),
    Eq (α := (↑R : Type (max u_1 v)))
      (((CommRingCat.Hom.hom f).comp C : (a : ULift.{u_1, 0} ℤ) → (↑R : Type (max u_1 v))) x : (↑R : Type (max u_1 v)))
      (((CommRingCat.Hom.hom g).comp C : (a : ULift.{u_1, 0} ℤ) → (↑R : Type (max u_1 v))) x : (↑R : Type (max u_1 v)))
hf₁ :
  ∀ (x : n),
    Eq (α := (↑R : Type (max u_1 v)))
      ((CommRingCat.Hom.hom f : (a : MvPolynomial n (ULift.{u_1, 0} ℤ)) → (↑R : Type (max u_1 v))) (X x) :
        (↑R : Type (max u_1 v)))
      ((CommRingCat.Hom.hom g : (a : MvPolynomial n (ULift.{u_1, 0} ℤ)) → (↑R : Type (max u_1 v))) (X x) :
        (↑R : Type (max u_1 v)))
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h :
  ∀ (i : n),
    Eq (α := (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) f :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) g :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
this :
  Eq (α := MvPolynomial n ℤ →+* (↑R : Type (max u_1 v)))
    ((CommRingCat.Hom.hom f).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))
    ((CommRingCat.Hom.hom g).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))
x : ULift.{u_1, 0} ℤ
hf :
  ∀ (x : ℤ),
    Eq (α := (↑R : Type (max u_1 v)))
      (((CommRingCat.Hom.hom f).comp C : (a : ULift.{u_1, 0} ℤ) → (↑R : Type (max u_1 v))) { down := x } :
        (↑R : Type (max u_1 v)))
      (((CommRingCat.Hom.hom g).comp C : (a : ULift.{u_1, 0} ℤ) → (↑R : Type (max u_1 v))) { down := x } :
        (↑R : Type (max u_1 v)))
⊢ Eq (α := (↑R : Type (max u_1 v)))
    (((CommRingCat.Hom.hom f).comp C : (a : ULift.{u_1, 0} ℤ) → (↑R : Type (max u_1 v))) x : (↑R : Type (max u_1 v)))
    (((CommRingCat.Hom.hom g).comp C : (a : ULift.{u_1, 0} ℤ) → (↑R : Type (max u_1 v))) x : (↑R : Type (max u_1 v)))

Tactic:
obtain ⟨x⟩ := x
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h :
  ∀ (i : n),
    Eq (α := (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) f :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) g :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
this :
  Eq (α := MvPolynomial n ℤ →+* (↑R : Type (max u_1 v)))
    ((CommRingCat.Hom.hom f).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))
    ((CommRingCat.Hom.hom g).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))
x : ℤ
⊢ Eq (α := (↑R : Type (max u_1 v)))
    (((CommRingCat.Hom.hom f).comp C : (a : ULift.{u_1, 0} ℤ) → (↑R : Type (max u_1 v))) { down := x } :
      (↑R : Type (max u_1 v)))
    (((CommRingCat.Hom.hom g).comp C : (a : ULift.{u_1, 0} ℤ) → (↑R : Type (max u_1 v))) { down := x } :
      (↑R : Type (max u_1 v)))

Tactic:
simpa [-map_intCast, -eq_intCast] using DFunLike.congr_fun this (C x)

Premises used: DFunLike.congr_fun, map_intCast, eq_intCast, MvPolynomial.C, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h :
  ∀ (i : n),
    Eq (α := (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) f :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) g :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
this :
  Eq (α := MvPolynomial n ℤ →+* (↑R : Type (max u_1 v)))
    ((CommRingCat.Hom.hom f).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))
    ((CommRingCat.Hom.hom g).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))
x : n
⊢ Eq (α := (↑R : Type (max u_1 v)))
    ((CommRingCat.Hom.hom f : (a : MvPolynomial n (ULift.{u_1, 0} ℤ)) → (↑R : Type (max u_1 v))) (X x) :
      (↑R : Type (max u_1 v)))
    ((CommRingCat.Hom.hom g : (a : MvPolynomial n (ULift.{u_1, 0} ℤ)) → (↑R : Type (max u_1 v))) (X x) :
      (↑R : Type (max u_1 v)))

Tactic:
simpa [-map_intCast, -eq_intCast] using DFunLike.congr_fun this (X x)

Premises used: DFunLike.congr_fun, MvPolynomial.X, map_intCast, eq_intCast
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h :
  ∀ (i : n),
    Eq (α := (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) f :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) g :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
suffices :
  Eq (α := MvPolynomial n ℤ →+* (↑R : Type (max u_1 v)))
    ((CommRingCat.Hom.hom f).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))
    ((CommRingCat.Hom.hom g).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))
⊢ f = g

Tactic:
suffices f.hom.comp (MvPolynomial.mapEquiv _ ULift.ringEquiv.symm).toRingHom =
      g.hom.comp (MvPolynomial.mapEquiv _ ULift.ringEquiv.symm).toRingHom by
    ext x
    · obtain ⟨x⟩ := x
      simpa [-map_intCast, -eq_intCast] using DFunLike.congr_fun this (C x)
    · simpa [-map_intCast, -eq_intCast] using DFunLike.congr_fun this (X x)
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h :
  ∀ (i : n),
    Eq (α := (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) f :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) g :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
hC :
  Eq (α := ℤ →+* (↑R : Type (max u_1 v)))
    (RingHom.comp ((CommRingCat.Hom.hom f).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv)))) C)
    (RingHom.comp ((CommRingCat.Hom.hom g).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv)))) C)
hX :
  ∀ (i : n),
    Eq (α := (↑R : Type (max u_1 v)))
      (((CommRingCat.Hom.hom f).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))) :
            (a : MvPolynomial n ℤ) → (↑R : Type (max u_1 v)))
          (X i) :
        (↑R : Type (max u_1 v)))
      (((CommRingCat.Hom.hom g).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))) :
            (a : MvPolynomial n ℤ) → (↑R : Type (max u_1 v)))
          (X i) :
        (↑R : Type (max u_1 v)))
⊢ Eq (α := MvPolynomial n ℤ →+* (↑R : Type (max u_1 v)))
    ((CommRingCat.Hom.hom f).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))
    ((CommRingCat.Hom.hom g).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))))

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h :
  ∀ (i : n),
    Eq (α := (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) f :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) g :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
⊢ Eq (α := ℤ →+* (↑R : Type (max u_1 v)))
    (RingHom.comp ((CommRingCat.Hom.hom f).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv)))) C)
    (RingHom.comp ((CommRingCat.Hom.hom g).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv)))) C)

Tactic:
RingHom.ext_int _ _

Premises used: RingHom.ext_int
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h :
  ∀ (i : n),
    Eq (α := (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) f :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) g :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
⊢ Eq (α := ℤ →+* (↑R : Type (max u_1 v)))
    (RingHom.comp ((CommRingCat.Hom.hom f).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv)))) C)
    (RingHom.comp ((CommRingCat.Hom.hom g).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv)))) C)

Tactic:
exact RingHom.ext_int _ _

Premises used: RingHom.ext_int
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h :
  ∀ (i : n),
    Eq (α := (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) f :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1)))
              (CC := CommRingCat.carrier) g :
            (a : (↑ℤ[n] : Type (max v u_1))) → (↑R : Type (max v u_1)))
          (X i) :
        (↑R : Type (max v u_1)))
i : n
⊢ Eq (α := (↑R : Type (max u_1 v)))
    (((CommRingCat.Hom.hom f).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))) :
          (a : MvPolynomial n ℤ) → (↑R : Type (max u_1 v)))
        (X i) :
      (↑R : Type (max u_1 v)))
    (((CommRingCat.Hom.hom g).comp (RingEquiv.toRingHom (mapEquiv n (RingEquiv.symm ULift.ringEquiv))) :
          (a : MvPolynomial n ℤ) → (↑R : Type (max u_1 v)))
        (X i) :
      (↑R : Type (max u_1 v)))

Tactic:
simpa using h _
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
f : X ⟶ Spec ℤ[n]
a :
  Eq (α := Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (Opposite.op ℤ[n])) :
          (a : X ⟶ Scheme.Spec.obj (Opposite.op ℤ[n])) → Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
        ((fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
            (X.toSpecΓ ≫
                Spec.map
                  (CommRingCat.ofHom
                    (eval₂Hom
                      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                        (algebraMap ℤ (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v)))
                        (RingEquiv.toRingHom ULift.ringEquiv))
                      v)) :
              X ⟶ Spec ℤ[n]))
          ((fun (f : X ⟶ Spec ℤ[n]) (i : n) ↦
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                      (CC := CommRingCat.carrier) (Scheme.Hom.appTop f) :
                    (a : (↑Γ(Spec ℤ[n], ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦
                        (↑R : Type (max v u)) →+* (↑S : Type (max v u))) (CC := CommRingCat.carrier) (X := ℤ[n])
                        (Iso.inv (Scheme.ΓSpecIso ℤ[n])) :
                      (a : (↑ℤ[n] : Type (max v u))) → (↑Γ(Spec ℤ[n], ⊤) : Type (max v u)))
                    (MvPolynomial.X i)) :
                (↑Γ(X, ⊤) : Type (max u v))))
            f)) :
      Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (Opposite.op ℤ[n])) :
          (a : X ⟶ Scheme.Spec.obj (Opposite.op ℤ[n])) → Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
        f :
      Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
⊢ (fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
        (X.toSpecΓ ≫
            Spec.map
              (CommRingCat.ofHom
                (eval₂Hom
                  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                    (algebraMap ℤ (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v)))
                    (RingEquiv.toRingHom ULift.ringEquiv))
                  v)) :
          X ⟶ Spec ℤ[n]))
      ((fun (f : X ⟶ Spec ℤ[n]) (i : n) ↦
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Spec ℤ[n], ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u)) →+* (↑S : Type (max v u)))
                    (CC := CommRingCat.carrier) (X := ℤ[n]) (Iso.inv (Scheme.ΓSpecIso ℤ[n])) :
                  (a : (↑ℤ[n] : Type (max v u))) → (↑Γ(Spec ℤ[n], ⊤) : Type (max v u)))
                (MvPolynomial.X i)) :
            (↑Γ(X, ⊤) : Type (max u v))))
        f) =
    f

Tactic:
apply (ΓSpec.adjunction.homEquiv _ _).symm.injective

Premises used: AlgebraicGeometry.ΓSpec.adjunction, CategoryTheory.Adjunction.homEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
f : X ⟶ Spec ℤ[n]
i : n
⊢ Eq (α := (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop f) :
          (a : (↑Γ(Spec ℤ[n], ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
        (((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u)) →+* (↑S : Type (max v u))) (CC :=
                CommRingCat.carrier) (X := ℤ[n]) (Iso.inv (Scheme.ΓSpecIso ℤ[n])) :
              (↑ℤ[n] : Type (max v u)) →+* (↑Γ(Spec ℤ[n], ⊤) : Type (max v u))) :
            (a : MvPolynomial n (ULift.{u, 0} ℤ)) → (↑Γ(Spec ℤ[n], ⊤) : Type (max v u)))
          (MvPolynomial.X i)) :
      (↑Γ(X, ⊤) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u)) →+* (↑S : Type (max v u))) (CC :=
            CommRingCat.carrier) (Iso.inv (Scheme.ΓSpecIso ℤ[n]) ≫ Scheme.Hom.appTop f) :
          (a : (↑ℤ[n] : Type (max v u))) →
            (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max v u)))
        (MvPolynomial.X i) :
      (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max v u)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
v : n → (↑Γ(X, ⊤) : Type (max u v))
h :
  ∀ (x : n),
    (fun (f : X ⟶ Spec ℤ[n]) (i : n) ↦
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Spec ℤ[n], ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u)) →+* (↑S : Type (max v u)))
                    (CC := CommRingCat.carrier) (X := ℤ[n]) (Iso.inv (Scheme.ΓSpecIso ℤ[n])) :
                  (a : (↑ℤ[n] : Type (max v u))) → (↑Γ(Spec ℤ[n], ⊤) : Type (max v u)))
                (MvPolynomial.X i)) :
            (↑Γ(X, ⊤) : Type (max u v))))
        ((fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
            (X.toSpecΓ ≫
                Spec.map
                  (CommRingCat.ofHom
                    (eval₂Hom
                      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                        (algebraMap ℤ (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v)))
                        (RingEquiv.toRingHom ULift.ringEquiv))
                      v)) :
              X ⟶ Spec ℤ[n]))
          v)
        x =
      v x
⊢ (fun (f : X ⟶ Spec ℤ[n]) (i : n) ↦
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop f) :
              (a : (↑Γ(Spec ℤ[n], ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u)) →+* (↑S : Type (max v u)))
                  (CC := CommRingCat.carrier) (X := ℤ[n]) (Iso.inv (Scheme.ΓSpecIso ℤ[n])) :
                (a : (↑ℤ[n] : Type (max v u))) → (↑Γ(Spec ℤ[n], ⊤) : Type (max v u)))
              (MvPolynomial.X i)) :
          (↑Γ(X, ⊤) : Type (max u v))))
      ((fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
          (X.toSpecΓ ≫
              Spec.map
                (CommRingCat.ofHom
                  (eval₂Hom
                    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                      (algebraMap ℤ (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v)))
                      (RingEquiv.toRingHom ULift.ringEquiv))
                    v)) :
            X ⟶ Spec ℤ[n]))
        v) =
    v

Tactic:
ext