awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
v : n → (↑Γ(X, ⊤) : Type (max u v))
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:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Spec ℤ[n]
i : n
⊢ Eq (α := (↑Γ(X, ⊤) : Type (max u_1 v)))
    ((toSpecMvPolyIntEquiv n : (a : X ⟶ Spec ℤ[n]) → n → (↑Γ(X, ⊤) : Type (max u_1 v))) (f ≫ g) i :
      (↑Γ(X, ⊤) : Type (max u_1 v)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u_1)) →+* (↑S : Type (max v u_1))) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop f) :
          (a : (↑Γ(Y, ⊤) : Type (max v u_1))) → (↑Γ(X, ⊤) : Type (max v u_1)))
        ((toSpecMvPolyIntEquiv n : (a : Y ⟶ Spec ℤ[n]) → n → (↑Γ(Y, ⊤) : Type (max u_1 v))) g i) :
      (↑Γ(X, ⊤) : Type (max v u_1)))

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
f : X ⟶ S
v : n → (↑Γ(X, ⊤) : Type (max u v))
⊢ Eq (α := X ⟶ ⊤_ Scheme) (f ≫ terminal.from S)
    ((Equiv.symm (toSpecMvPolyIntEquiv n) : (a : n → (↑Γ(X, ⊤) : Type (max u v))) → X ⟶ Spec ℤ[n]) v ≫
      terminal.from (Spec ℤ[n]))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
f : X ⟶ S
v : n → (↑Γ(X, ⊤) : Type (max u v))
⊢ homOfVector f v ≫ toSpecMvPoly n S =
    (Equiv.symm (toSpecMvPolyIntEquiv n) : (a : n → (↑Γ(X, ⊤) : Type (max v u))) → X ⟶ Spec ℤ[n]) v

Tactic:
pullback.lift_snd _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_snd
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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
rw₃ rw₄ : v 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

Tactic:
rw [coord, ← toSpecMvPolyIntEquiv_comp, homOfVector_toSpecMvPoly,
    Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, AlgebraicGeometry.AffineSpace.coord, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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)))
apply :
  f ≫ pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n])) =
    g ≫ pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))
⊢ f = g

Tactic:
apply pullback.hom_ext h₁

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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)))
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)))
⊢ f ≫ toSpecMvPoly n S = g ≫ toSpecMvPoly n S

Tactic:
apply (toSpecMvPolyIntEquiv n).injective

Premises used: AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv, Equiv.injective
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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)))
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)))
⊢ 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:
ext i
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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
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)))
⊢ 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:
rw [toSpecMvPolyIntEquiv_comp, toSpecMvPolyIntEquiv_comp]

Premises used: AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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)))
    ((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:
h₂ i

Premises used: AlgebraicGeometry.AffineSpace.coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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)))
    ((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:
exact h₂ i
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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
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)))
⊢ 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)

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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) ≫ 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:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X Y : Scheme
v : n → (↑Γ(Y, ⊤) : Type (max u v))
f : X ⟶ Y
g : Y ⟶ 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) (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:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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)) :
        X ⟶ 𝔸(n; S)) ≫
      AffineSpace.{v, u} n S ↘ S =
    (↑f : X ⟶ 𝔸(n; S)) ≫ AffineSpace.{v, u} n S ↘ S

Tactic:
simp [f.2.1]

Premises used: CategoryTheory.HomIsOver.comp_over
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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
a 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)))
⊢ 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)))

Tactic:
rw [homOfVector_appTop_coord]

Premises used: AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
v : n → (↑Γ(X, ⊤) : Type (max u v))
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) ⋯ :
              { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }))
          v)
        i =
      v i
⊢ (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

Tactic:
ext i