awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)))
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)))
have a : 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)))
      ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n 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)))
      ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S)
        i) :
    (↑Γ(X, ⊤) : Type (max u v)))
Tactic: rw [toSpecMvPolyIntEquiv_comp, toSpecMvPolyIntEquiv_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X Y : Scheme
v : n → (↑Γ(Y, ⊤) : Type (max u v))
f : X ⟶ Y
g : Y ⟶ S
⊢ f ≫ homOfVector g v =
    homOfVector (f ≫ g)
      ((⇑(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 : (↑Γ(Y, ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v))) ∘
        v)
have h₁ : (f ≫ homOfVector g v) ≫ AffineSpace.{v, u} n S ↘ S =
  homOfVector (f ≫ g)
      ((⇑(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 : (↑Γ(Y, ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v))) ∘
        v) ≫
    AffineSpace.{v, u} n S ↘ S
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X Y : Scheme
v : n → (↑Γ(Y, ⊤) : Type (max u v))
f : X ⟶ Y
g : Y ⟶ S
h₁ :
  (f ≫ homOfVector g v) ≫ AffineSpace.{v, u} n S ↘ S =
    homOfVector (f ≫ g)
        ((⇑(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 : (↑Γ(Y, ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v))) ∘
          v) ≫
      AffineSpace.{v, u} n S ↘ S
⊢ f ≫ homOfVector g v =
    homOfVector (f ≫ g)
      ((⇑(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 : (↑Γ(Y, ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v))) ∘
        v)
have 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 ≫ homOfVector g v)) :
          (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
              (homOfVector (f ≫ g)
                ((⇑(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 : (↑Γ(Y, ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v))) ∘
                  v))) :
          (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
        (coord S i) :
      (↑Γ(X, ⊤) : Type (max u v)))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }
⊢ (fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
        (Subtype.mk (p := fun (f : X ⟶ AffineSpace.{v, u} n S) ↦ Scheme.Hom.IsOver f S) (homOfVector (X ↘ S) v) ⋯ :
          { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }))
      ((fun (f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }) (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 : X ⟶ 𝔸(n; S))) :
                (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
              (coord S i) :
            (↑Γ(X, ⊤) : Type (max u v))))
        f) =
    f
have a : (↑((fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
            (Subtype.mk (p := fun (f : X ⟶ AffineSpace.{v, u} n S) ↦ Scheme.Hom.IsOver f S) (homOfVector (X ↘ S) v) sorry :
              { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }))
          ((fun (f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }) (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 : X ⟶ 𝔸(n; S))) :
                    (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
                  (coord S i) :
                (↑Γ(X, ⊤) : Type (max u v))))
            f)) :
      X ⟶ 𝔸(n; S)) ≫
    AffineSpace.{v, u} n S ↘ S =
  (↑f : X ⟶ 𝔸(n; S)) ≫ AffineSpace.{v, u} n S ↘ S
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }
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) (X := Γ(𝔸(n; S), ⊤)) (Y := Γ(X, ⊤))
            (Scheme.Hom.appTop
              (↑((fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
                      (Subtype.mk (p := fun (f : X ⟶ AffineSpace.{v, u} n S) ↦ Scheme.Hom.IsOver f S)
                          (homOfVector (X ↘ S) v) ⋯ :
                        { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }))
                    ((fun (f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }) (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 : X ⟶ 𝔸(n; S))) :
                              (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
                            (coord S i) :
                          (↑Γ(X, ⊤) : Type (max u v))))
                      f)) :
                X ⟶ 𝔸(n; S))) :
          (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 (↑f : X ⟶ 𝔸(n; S))) :
          (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
        (coord S i) :
      (↑Γ(X, ⊤) : Type (max u v)))
have a : Eq (α := (↑Γ(X, ⊤) : Type (max u v)))
  ((fun (f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }) (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 : X ⟶ 𝔸(n; S))) :
              (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
            (coord S i) :
          (↑Γ(X, ⊤) : Type (max u v))))
      f 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 (↑f : X ⟶ 𝔸(n; S))) :
        (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
      (coord S i) :
    (↑Γ(X, ⊤) : Type (max u v)))
Tactic: rw [homOfVector_appTop_coord]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
v : n → (↑Γ(X, ⊤) : Type (max u v))
⊢ (fun (f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }) (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 : X ⟶ 𝔸(n; S))) :
              (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
            (coord S i) :
          (↑Γ(X, ⊤) : Type (max u v))))
      ((fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
          (Subtype.mk (p := fun (f : X ⟶ AffineSpace.{v, u} n S) ↦ Scheme.Hom.IsOver f S) (homOfVector (X ↘ S) v) ⋯ :
            { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }))
        v) =
    v
have h : ∀ (i : n),
  (fun (f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }) (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 : X ⟶ 𝔸(n; S))) :
              (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
            (coord S i) :
          (↑Γ(X, ⊤) : Type (max u v))))
      ((fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
          (Subtype.mk (p := fun (f : X ⟶ AffineSpace.{v, u} n S) ↦ Scheme.Hom.IsOver f S) (homOfVector (X ↘ S) v) sorry :
            { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }))
        v)
      i =
    v i
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ ((AffineSpace.{v, u} n S).toSpecΓ ≫
        Spec.map
          (CommRingCat.ofHom
            (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S)))) ≫
      homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
        (Function.comp (β := (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v)))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := CommRingCat.carrier) (X := CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
                (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))) :
            (a : (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v))) →
              (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max u v)))
          MvPolynomial.X) =
    𝟙 (AffineSpace.{v, u} n S)
have h₁ : (((AffineSpace.{v, u} n S).toSpecΓ ≫
        Spec.map
          (CommRingCat.ofHom
            (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S)))) ≫
      homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
        (Function.comp (β := (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v)))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := CommRingCat.carrier) (X := CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
                (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))) :
            (a : (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v))) →
              (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max u v)))
          MvPolynomial.X)) ≫
    AffineSpace.{v, u} n S ↘ S =
  𝟙 (AffineSpace.{v, u} n S) ≫ AffineSpace.{v, u} n S ↘ S
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ (((AffineSpace.{v, u} n S).toSpecΓ ≫
          Spec.map
            (CommRingCat.ofHom
              (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S)))) ≫
        homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
          (Function.comp (β := (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v)))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := CommRingCat.carrier) (X := CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
                  (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))) :
              (a : (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v))) →
                (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max u v)))
            MvPolynomial.X)) ≫
      AffineSpace.{v, u} n S ↘ S =
    𝟙 (AffineSpace.{v, u} n S) ≫ AffineSpace.{v, u} n S ↘ S
have h₁ : (AffineSpace.{v, u} n S).toSpecΓ ≫
    Spec.map
        (CommRingCat.ofHom
          (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S))) ≫
      Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv =
  AffineSpace.{v, u} n S ↘ S
Tactic: simp only [Category.assoc, homOfVector_over, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ (AffineSpace.{v, u} n S).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom
            (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S))) ≫
        Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv =
    AffineSpace.{v, u} n S ↘ S
have h₁ : AffineSpace.{v, u} n S ↘ S ≫ S.toSpecΓ ≫ S.isoSpec.inv = AffineSpace.{v, u} n S ↘ S
Tactic: rw [← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, eval₂Hom_comp_C,
            CommRingCat.ofHom_hom, ← Scheme.toSpecΓ_naturality_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
        (Function.comp (β := (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v)))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := CommRingCat.carrier) (X := CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
                (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))) :
            (a : (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v))) →
              (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max u v)))
          MvPolynomial.X) ≫
      (AffineSpace.{v, u} n S).toSpecΓ ≫
        Spec.map
          (CommRingCat.ofHom
            (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S))) =
    𝟙 (Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))))
have e : Scheme.Hom.appTop
    (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
        (Function.comp (β := (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v)))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := CommRingCat.carrier) (X := CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
                (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))) :
            (a : (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v))) →
              (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max u v)))
          MvPolynomial.X) ≫
      (AffineSpace.{v, u} n S).toSpecΓ ≫
        Spec.map
          (CommRingCat.ofHom
            (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S)))) =
  Scheme.Hom.appTop (𝟙 (Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))
Tactic: apply ext_of_isAffine
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ Scheme.Hom.appTop
      (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
          (Function.comp (β := (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v)))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := CommRingCat.carrier) (X := CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
                  (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))) :
              (a : (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v))) →
                (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max u v)))
            MvPolynomial.X) ≫
        (AffineSpace.{v, u} n S).toSpecΓ ≫
          Spec.map
            (CommRingCat.ofHom
              (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S)))) =
    Scheme.Hom.appTop (𝟙 (Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))
have e : Eq (α :=
  CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) ⟶
    Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
  (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S)) ≫
      Scheme.Hom.app
        (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
          (Function.comp (β := MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := CommRingCat.carrier) (X := CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
                  (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))) :
              (a : MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) →
                (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max u v)))
            MvPolynomial.X))
        ⊤ :
    CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) ⟶
      Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
  (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))) :
    CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) ⟶
      Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
Tactic: simp only [Scheme.Hom.comp_base, TopologicalSpace.Opens.map_comp_obj,
          TopologicalSpace.Opens.map_top, Scheme.Hom.comp_app, Scheme.toSpecΓ_appTop,
          Scheme.ΓSpecIso_naturality, Category.assoc, Scheme.Hom.id_app, ← Iso.eq_inv_comp,
          Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ Eq (α :=
    CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) ⟶
      Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
    (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S)) ≫
        Scheme.Hom.app
          (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
            (Function.comp (β := MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))
              (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                    (CC := CommRingCat.carrier) (X := CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
                    (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))) :
                (a : MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) →
                  (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max u v)))
              MvPolynomial.X))
          ⊤ :
      CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) ⟶
        Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
    (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))) :
      CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) ⟶
        Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
have e : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have e : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply ringHom_ext'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
e : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have e₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply ringHom_ext'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have e : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: change _ = (CommRingCat.ofHom C ≫ _).hom