awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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))))
⊢ f = g
have 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)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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)))
⊢ f = g
have 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)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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} ℤ
⊢ 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)))
have 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)))
Tactic: obtain ⟨x⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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)))
⊢ f = g
have 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))))
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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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 (α := 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))))
have 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)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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)
⊢ 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))))
have 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)))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
f : X ⟶ Spec ℤ[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
have 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])
Tactic: apply (ΓSpec.adjunction.homEquiv _ _).symm.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
v : n → (↑Γ(X, ⊤) : Type (max u v))
⊢ (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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
f : X ⟶ S
v : n → (↑Γ(X, ⊤) : Type (max u v))
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 (homOfVector f v)) :
        (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
      (coord S i) =
    v i
have rw : (ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
        CommRingCat.carrier) (Scheme.Hom.appTop (homOfVector f v)) :
      (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S)
      i) =
  v i
Tactic: rw [coord, ← toSpecMvPolyIntEquiv_comp, homOfVector_toSpecMvPoly,
    Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
f : X ⟶ S
v : n → (↑Γ(X, ⊤) : Type (max u v))
i : n
rw :
  (ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (homOfVector f v)) :
        (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
      ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S)
        i) =
    v i
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (homOfVector f v)) :
        (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
      (coord S i) =
    v i
have rw₁ : (toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u v))) (homOfVector f v ≫ toSpecMvPoly n S)
    i =
  v i
Tactic: rw [coord, ← toSpecMvPolyIntEquiv_comp, homOfVector_toSpecMvPoly,
    Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
f : X ⟶ S
v : n → (↑Γ(X, ⊤) : Type (max u v))
i : n
rw :
  (ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (homOfVector f v)) :
        (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
      ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S)
        i) =
    v i
rw₁ :
  (toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u v))) (homOfVector f v ≫ toSpecMvPoly n S)
      i =
    v i
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (homOfVector f v)) :
        (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
      (coord S i) =
    v i
have rw₂ : (toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u v)))
    ((Equiv.symm (toSpecMvPolyIntEquiv n) : (a : n → (↑Γ(X, ⊤) : Type (max v u))) → X ⟶ Spec ℤ[n]) v : X ⟶ Spec ℤ[n])
    i =
  v i
Tactic: rw [coord, ← toSpecMvPolyIntEquiv_comp, homOfVector_toSpecMvPoly,
    Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
f : X ⟶ S
v : n → (↑Γ(X, ⊤) : Type (max u v))
i : n
rw :
  (ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (homOfVector f v)) :
        (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
      ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S)
        i) =
    v i
rw₁ :
  (toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u v))) (homOfVector f v ≫ toSpecMvPoly n S)
      i =
    v i
rw₂ :
  (toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u v)))
      ((Equiv.symm (toSpecMvPolyIntEquiv n) : (a : n → (↑Γ(X, ⊤) : Type (max v u))) → X ⟶ Spec ℤ[n]) v : X ⟶ Spec ℤ[n])
      i =
    v i
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (homOfVector f v)) :
        (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
      (coord S i) =
    v i
have rw₃ : v i = v i
Tactic: rw [coord, ← toSpecMvPolyIntEquiv_comp, homOfVector_toSpecMvPoly,
    Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
f g : X ⟶ AffineSpace.{v, u} n S
h₁ : f ≫ AffineSpace.{v, u} n S ↘ S = g ≫ AffineSpace.{v, u} n S ↘ S
h₂ :
  ∀ (i : n),
    Eq (α := (↑Γ(X, ⊤) : Type (max u v)))
      ((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 : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
          (coord S i) :
        (↑Γ(X, ⊤) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop g) :
            (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
          (coord S i) :
        (↑Γ(X, ⊤) : Type (max u v)))
⊢ f = g
have apply : f ≫ pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n])) =
  g ≫ pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))
Tactic: apply pullback.hom_ext h₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
f g : X ⟶ AffineSpace.{v, u} n S
h₁ : f ≫ AffineSpace.{v, u} n S ↘ S = g ≫ AffineSpace.{v, u} n S ↘ S
h₂ :
  ∀ (i : n),
    Eq (α := (↑Γ(X, ⊤) : Type (max u v)))
      ((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 : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
          (coord S i) :
        (↑Γ(X, ⊤) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop g) :
            (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
          (coord S i) :
        (↑Γ(X, ⊤) : Type (max u v)))
⊢ f ≫ toSpecMvPoly n S = g ≫ toSpecMvPoly n S
have a : Eq (α := n → (↑Γ(X, ⊤) : Type (max u v)))
  ((toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u v))) (f ≫ toSpecMvPoly n S) :
    n → (↑Γ(X, ⊤) : Type (max u v)))
  ((toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u v))) (g ≫ toSpecMvPoly n S) :
    n → (↑Γ(X, ⊤) : Type (max u v)))
Tactic: apply (toSpecMvPolyIntEquiv n).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
f g : X ⟶ AffineSpace.{v, u} n S
h₁ : f ≫ AffineSpace.{v, u} n S ↘ S = g ≫ AffineSpace.{v, u} n S ↘ S
h₂ :
  ∀ (i : n),
    Eq (α := (↑Γ(X, ⊤) : Type (max u v)))
      ((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 : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
          (coord S i) :
        (↑Γ(X, ⊤) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop g) :
            (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
          (coord S i) :
        (↑Γ(X, ⊤) : Type (max u v)))
⊢ Eq (α := n → (↑Γ(X, ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u v))) (f ≫ toSpecMvPoly n S) :
      n → (↑Γ(X, ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u v))) (g ≫ toSpecMvPoly n S) :
      n → (↑Γ(X, ⊤) : Type (max u v)))
have a : ∀ (i : n),
  Eq (α := (↑Γ(X, ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u v))) (f ≫ toSpecMvPoly n S) i :
      (↑Γ(X, ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u v))) (g ≫ toSpecMvPoly n S) i :
      (↑Γ(X, ⊤) : Type (max u v)))
Tactic: ext i