awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
v : n → (↑Γ(X, ⊤) : Type (max u v))
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) ⋯ :
            { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }))
        v)
      i =
    v i

Tactic:
simp [-TopologicalSpace.Opens.map_top, homOfVector_appTop_coord]

Premises used: TopologicalSpace.Opens.map_top, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
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
⊢ (((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:
simp only [Category.assoc, homOfVector_over, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.AffineSpace.homOfVector_over, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
h₁ : AffineSpace.{v, u} n S ↘ S ≫ S.toSpecΓ ≫ S.isoSpec.inv = AffineSpace.{v, u} n S ↘ 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

Tactic:
rw [← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, eval₂Hom_comp_C,
            CommRingCat.ofHom_hom, ← Scheme.toSpecΓ_naturality_assoc]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, CommRingCat.ofHom_hom, AlgebraicGeometry.Spec.map_comp_assoc, CommRingCat.ofHom_comp, MvPolynomial.eval₂Hom_comp_C
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ AffineSpace.{v, u} n S ↘ S ≫ S.toSpecΓ ≫ S.isoSpec.inv = AffineSpace.{v, u} n S ↘ S

Tactic:
simp [Scheme.isoSpec]

Premises used: AlgebraicGeometry.Scheme.isoSpec
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
i : n
⊢ Eq (α := (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((@ConcreteCategory.hom _ CommRingCat.instCategory
            (fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) CommRingCat.carrier
            (fun (X Y : CommRingCat) ↦
              (RingHom.instFunLike :
                FunLike ((↑X : Type (max u v)) →+* (↑Y : Type (max u v))) (↑X : Type (max u v)) (↑Y : Type (max u v))))
            _ _ _
            (Scheme.Hom.appTop
                (((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)) :
              Γ(𝔸(n; S), ⊤) ⟶ Γ(𝔸(n; S), ⊤)) :
          (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        (coord S i) :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((@ConcreteCategory.hom _ CommRingCat.instCategory
            (fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) CommRingCat.carrier
            (fun (X Y : CommRingCat) ↦
              (RingHom.instFunLike :
                FunLike ((↑X : Type (max u v)) →+* (↑Y : Type (max u v))) (↑X : Type (max u v)) (↑Y : Type (max u v))))
            _ _ _ (Scheme.Hom.appTop (𝟙 (AffineSpace.{v, u} n S))) :
          (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        (coord S i) :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
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))))))
⊢ 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)))))

Tactic:
apply ext_of_isAffine

Premises used: AlgebraicGeometry.ext_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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)
⊢ 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:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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)
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)

Tactic:
apply ringHom_ext'

Premises used: MvPolynomial.ringHom_ext'
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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)

Tactic:
change _ = (CommRingCat.ofHom C ≫ _).hom

Premises used: CommRingCat.Hom.hom, CommRingCat.ofHom, CategoryTheory.CategoryStruct.comp, MvPolynomial.C
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
e :
  Eq (α := Γ(S, ⊤) ⟶ CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
    (CategoryStruct.comp (Y := Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
      (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ 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))
            ⊤ :
        Γ(S, ⊤) ⟶ Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
      (Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))) :
        Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) ⟶
          CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))))
    ((CommRingCat.ofHom C ≫ Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))))) ≫
      Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [CommRingCat.hom_comp, RingHom.comp_assoc, CommRingCat.hom_ofHom, eval₂Hom_comp_C,
            ← CommRingCat.hom_comp, ← CommRingCat.hom_ext_iff,
            ← cancel_mono (Scheme.ΓSpecIso _).hom]

Premises used: AlgebraicGeometry.Scheme.ΓSpecIso, CommRingCat.hom_comp, RingHom.comp_assoc, CategoryTheory.cancel_mono, CommRingCat.hom_ext_iff, CommRingCat.hom_ofHom, CategoryTheory.Iso.hom, MvPolynomial.eval₂Hom_comp_C
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
e :
  Eq (α := Γ(S, ⊤) ⟶ CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
    ((Scheme.Hom.appTop S.isoSpec.inv ≫ Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom C))) ≫
      Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))
    ((CommRingCat.ofHom C ≫ Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))))) ≫
      Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))
⊢ Eq (α := Γ(S, ⊤) ⟶ CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
    (CategoryStruct.comp (Y := Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
      (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ 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))
            ⊤ :
        Γ(S, ⊤) ⟶ Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
      (Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))) :
        Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) ⟶
          CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))))
    ((CommRingCat.ofHom C ≫ Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))))) ≫
      Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))

Tactic:
rw [← Scheme.Hom.comp_appTop, homOfVector_over, Scheme.Hom.comp_appTop]

Premises used: AlgebraicGeometry.AffineSpace.homOfVector_over, AlgebraicGeometry.Scheme.Hom.comp_appTop
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
e :
  Eq (α := Γ(S, ⊤) ⟶ CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
    (Scheme.Hom.appTop S.isoSpec.inv ≫ Scheme.Hom.appTop S.toSpecΓ ≫ CommRingCat.ofHom C)
    (CommRingCat.ofHom C ≫
      Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))) ≫
        Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))
⊢ Eq (α := Γ(S, ⊤) ⟶ CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
    ((Scheme.Hom.appTop S.isoSpec.inv ≫ Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom C))) ≫
      Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))
    ((CommRingCat.ofHom C ≫ Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))))) ≫
      Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))

Tactic:
simp only [Category.assoc, Scheme.ΓSpecIso_naturality, CommRingCat.of_carrier,
            ← Scheme.toSpecΓ_appTop]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.toSpecΓ_appTop, CommRingCat.of_carrier
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
e :
  Eq (α := Γ(S, ⊤) ⟶ CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
    (Scheme.Hom.appTop (𝟙 S) ≫ CommRingCat.ofHom C)
    (CommRingCat.ofHom C ≫
      Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))) ≫
        Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))
⊢ Eq (α := Γ(S, ⊤) ⟶ CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
    (Scheme.Hom.appTop S.isoSpec.inv ≫ Scheme.Hom.appTop S.toSpecΓ ≫ CommRingCat.ofHom C)
    (CommRingCat.ofHom C ≫
      Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))) ≫
        Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))

Tactic:
rw [← Scheme.Hom.comp_appTop_assoc, Scheme.isoSpec, asIso_inv, IsIso.hom_inv_id]

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.asIso_inv, CategoryTheory.IsIso.hom_inv_id, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ Eq (α := Γ(S, ⊤) ⟶ CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
    (Scheme.Hom.appTop (𝟙 S) ≫ CommRingCat.ofHom C)
    (CommRingCat.ofHom C ≫
      Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))) ≫
        Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
i : n
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)

Tactic:
simp only [eval₂_X]

Premises used: MvPolynomial.eval₂_X
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
homOfVector_appTop_coord _ _ _

Premises used: Set.Mem, setOf, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact homOfVector_appTop_coord _ _ _

Premises used: AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
inst : IsAffine S
⊢ Scheme.Hom.appTop (isoOfIsAffine n S).hom =
    Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max v u))))) ≫
      CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S))

Tactic:
simp [isoOfIsAffine_hom]

Premises used: AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
inst : IsAffine S
i : n
⊢ Eq (α := (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u)) →+* (↑S : Type (max v u))) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (isoOfIsAffine n S).inv) :
          (a : (↑Γ(𝔸(n; S), ⊤) : Type (max v u))) →
            (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max v u)))
        (coord S i) :
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u)) →+* (↑S : Type (max v u))) (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 v u))) →
            (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max v u)))
        (X i) :
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max v u)))

Tactic:
homOfVector_appTop_coord _ _ _

Premises used: Set.Mem, setOf, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
inst : IsAffine S
⊢ (isoOfIsAffine n S).inv ≫ AffineSpace.{v, u} n S ↘ S = Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv

Tactic:
pullback.lift_fst _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ IsAffine (AffineSpace.{v, u} n S)

Tactic:
.of_isIso (isoOfIsAffine n S).hom

Premises used: AlgebraicGeometry.IsAffine.of_isIso, AlgebraicGeometry.AffineSpace.isoOfIsAffine, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
hf :
  ∀ (i : (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v))),
    Eq (α := (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v)))
      ((CommRingCat.Hom.hom (Scheme.Hom.appTop (SpecIso n R).hom) :
            (a : (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v))) →
              (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v)))
          i :
        (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v)))
      ((CommRingCat.Hom.hom
              (Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑R : Type (max u v))))) ≫
                CommRingCat.ofHom
                  (eval₂Hom
                    (CommRingCat.Hom.hom
                      ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (AffineSpace.{v, u} n (Spec R) ↘ Spec R)))
                    (coord (Spec R)))) :
            (a : (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v))) →
              (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v)))
          i :
        (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v)))
⊢ Scheme.Hom.appTop (SpecIso n R).hom =
    Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑R : Type (max u v))))) ≫
      CommRingCat.ofHom
        (eval₂Hom
          (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (AffineSpace.{v, u} n (Spec R) ↘ Spec R)))
          (coord (Spec R)))

Tactic:
ext i