awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
⊢ Eq (α := (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : 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 := Γ(𝔸(n; Spec R), ⊤)) (Scheme.Hom.app (SpecIso n R).inv ⊤) :
          (a : (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v))) →
            (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v)))
        (coord (Spec R) i) :
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : 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 := CommRingCat.of (MvPolynomial n (↑R : Type (max u v))))
            (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))))) :
          (a : (↑(CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))) : Type (max v u))) →
            (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max v u)))
        (X i) :
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max v u)))

Tactic:
exact SpecIso_inv_appTop_coord _ _

Premises used: AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
enter enter₁ :
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          CommRingCat.carrier) (X := Γ(𝔸(n; Spec R), ⊤)) (Scheme.Hom.app (SpecIso n R).inv ⊤) :
        (a : (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v))) →
          (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v)))
      (coord (Spec R) i) :
    (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v)))
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
enter [2]; tactic => exact SpecIso_inv_appTop_coord _ _

Premises used: AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S_1 X : Scheme
inst : X.Over S_1
R S : CommRingCat
φ : R ⟶ S
⊢ (SpecIso n R).inv ≫ (SpecIso n R).hom = 𝟙 (Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))))

Tactic:
have := (SpecIso n R).inv_hom_id
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S_1 X : Scheme
inst : X.Over S_1
R S : CommRingCat
φ : R ⟶ S
this : (SpecIso n R).inv ≫ (SpecIso n R).hom = 𝟙 (Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))))
⊢ (SpecIso n S).hom ≫
      (Arrow.mk (X := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))))
          (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))).hom =
    (Arrow.mk (map n (Spec.map φ))).hom ≫ (SpecIso n R).hom

Tactic:
simp [map_SpecMap]

Premises used: AlgebraicGeometry.AffineSpace.map_SpecMap
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ IsPullback (map n f) (AffineSpace.{v, u} n S ↘ S) (AffineSpace.{v, u} n T ↘ T) f

Tactic:
(IsPullback.paste_horiz_iff (.flip <| .of_hasPullback _ _) (map_over f)).mp ?_

Premises used: CategoryTheory.IsPullback.paste_horiz_iff, CategoryTheory.Limits.limit.π, AlgebraicGeometry.AffineSpace, AlgebraicGeometry.AffineSpace.map_over, CategoryTheory.over, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
refine :
  IsPullback (Z := ⊤_ Scheme) (map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])))
    (AffineSpace.{v, u} n S ↘ S) (terminal.from (Spec ℤ[n])) (f ≫ terminal.from T)
⊢ IsPullback (map n f) (AffineSpace.{v, u} n S ↘ S) (AffineSpace.{v, u} n T ↘ T) f

Tactic:
refine (IsPullback.paste_horiz_iff (.flip <| .of_hasPullback _ _) (map_over f)).mp ?_

Premises used: CategoryTheory.IsPullback.paste_horiz_iff, AlgebraicGeometry.AffineSpace.map_over, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
simp :
  IsPullback (Z := ⊤_ Scheme) (map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])))
    (AffineSpace.{v, u} n S ↘ S) (terminal.from (Spec ℤ[n])) (terminal.from S)
⊢ IsPullback (Z := ⊤_ Scheme) (map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])))
    (AffineSpace.{v, u} n S ↘ S) (terminal.from (Spec ℤ[n])) (f ≫ terminal.from T)

Tactic:
simp only [terminal.comp_from, ]

Premises used: CategoryTheory.Limits.terminal.comp_from
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ IsPullback (P := pullback (Z := ⊤_ Scheme) (terminal.from S) (terminal.from (Spec ℤ[n]))) (Z := ⊤_ Scheme)
    (pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n])))
    (pullback.fst (terminal.from S) (terminal.from (Spec ℤ[n]))) (terminal.from (Spec ℤ[n])) (terminal.from S)

Tactic:
(IsPullback.of_hasPullback _ _).flip

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
h :
  AffineSpace.{v, u} n S = pullback (Z := ⊤_ Scheme) (terminal.from S) (terminal.from (Spec ℤ[n])) →
    map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])) =
      pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))
⊢ IsPullback (Z := ⊤_ Scheme) (map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])))
    (AffineSpace.{v, u} n S ↘ S) (terminal.from (Spec ℤ[n])) (terminal.from S)

Tactic:
convert! (IsPullback.of_hasPullback _ _).flip

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
e_3 : AffineSpace.{v, u} n S = pullback (Z := ⊤_ Scheme) (terminal.from S) (terminal.from (Spec ℤ[n]))
h : map n f ≫ toSpecMvPoly n T = pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))
h₁ : map n f ≫ toSpecMvPoly n T = toSpecMvPoly n S
h₂ h₃ : toSpecMvPoly n S = toSpecMvPoly n S
⊢ map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])) =
    pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))

Tactic:
rw [← toSpecMvPoly, ← toSpecMvPoly, map_toSpecMvPoly]

Premises used: AlgebraicGeometry.AffineSpace.toSpecMvPoly, AlgebraicGeometry.AffineSpace.map_toSpecMvPoly
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n m : Type v
i : m → n
S : Scheme
⊢ reindex i S ≫ AffineSpace.{v, u} m S ↘ S = AffineSpace.{v, u} n S ↘ S

Tactic:
pullback.lift_fst _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n m : Type v
i : m → n
S : Scheme
j : m
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u)) →+* (↑S : Type (max v u))) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (reindex i S)) :
        (a : (↑Γ(𝔸(m; S), ⊤) : Type (max v u))) → (↑Γ(𝔸(n; S), ⊤) : Type (max v u)))
      (coord S j) =
    coord S (i j)

Tactic:
homOfVector_appTop_coord _ _ _

Premises used: AlgebraicGeometry.AffineSpace.coord, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h₁ : reindex id S ≫ AffineSpace.{v, u} n S ↘ S = 𝟙 (AffineSpace.{v, u} n S) ≫ AffineSpace.{v, u} n S ↘ S
h₂ :
  ∀ (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 (reindex id S) : Γ(𝔸(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)))
⊢ reindex id S = 𝟙 (AffineSpace.{v, u} n S)

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
⊢ reindex id S ≫ AffineSpace.{v, u} n S ↘ S = 𝟙 (AffineSpace.{v, u} n S) ≫ AffineSpace.{v, u} n S ↘ S

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
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 (reindex id S) : Γ(𝔸(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₁ n₂ n₃ : Type v
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
⊢ Eq (α := AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₃) S ⟶ S)
    (reindex
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (i ≫ j)) :
          (a : (fun (X : Type v) ↦ X) n₁) → (fun (X : Type v) ↦ X) n₃)
        S ≫
      AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₁) S ↘ S)
    (CategoryStruct.comp (Y := AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₂) S)
        (reindex
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) j) : (a : (fun (X : Type v) ↦ X) n₂) → (fun (X : Type v) ↦ X) n₃)
          S)
        (reindex
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) i) : (a : (fun (X : Type v) ↦ X) n₁) → (fun (X : Type v) ↦ X) n₂)
          S) ≫
      AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₁) S ↘ S)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n₁ n₂ n₃ : Type v
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
k : (fun (X : Type v) ↦ X) n₁
⊢ Eq (α := (↑Γ(𝔸((fun (X : Type v) ↦ X) 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 := Γ(𝔸((fun (X : Type v) ↦ X) n₁; S), ⊤)) (Y :=
            Γ(𝔸((fun (X : Type v) ↦ X) n₃; S), ⊤))
            (Scheme.Hom.appTop
              (reindex
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (i ≫ j)) :
                  (a : (fun (X : Type v) ↦ X) n₁) → (fun (X : Type v) ↦ X) n₃)
                S)) :
          (a : (↑Γ(𝔸((fun (X : Type v) ↦ X) n₁; S), ⊤) : Type (max u v))) →
            (↑Γ(𝔸((fun (X : Type v) ↦ X) n₃; S), ⊤) : Type (max u v)))
        (coord S k) :
      (↑Γ(𝔸((fun (X : Type v) ↦ X) 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 := Γ(𝔸((fun (X : Type v) ↦ X) n₁; S), ⊤)) (Y :=
            Γ(𝔸((fun (X : Type v) ↦ X) n₃; S), ⊤))
            (Scheme.Hom.appTop
              (CategoryStruct.comp (Y := AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₂) S)
                (reindex
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) j) :
                    (a : (fun (X : Type v) ↦ X) n₂) → (fun (X : Type v) ↦ X) n₃)
                  S)
                (reindex
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) i) :
                    (a : (fun (X : Type v) ↦ X) n₁) → (fun (X : Type v) ↦ X) n₂)
                  S))) :
          (a : (↑Γ(𝔸((fun (X : Type v) ↦ X) n₁; S), ⊤) : Type (max u v))) →
            (↑Γ(𝔸((fun (X : Type v) ↦ X) n₃; S), ⊤) : Type (max u v)))
        (coord S k) :
      (↑Γ(𝔸((fun (X : Type v) ↦ X) n₃; S), ⊤) : Type (max u v)))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n₁ n₂ : Type v
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
h₁ : (map n₂ f ≫ reindex i T) ≫ AffineSpace.{v, u} n₁ T ↘ T = (reindex i S ≫ map n₁ f) ≫ AffineSpace.{v, u} n₁ T ↘ T
h₂ :
  ∀ (i_1 : n₁),
    Eq (α := (↑Γ(𝔸(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) (Scheme.Hom.appTop (map n₂ f ≫ reindex i T)) :
            (a : (↑Γ(𝔸(n₁; T), ⊤) : Type (max u v))) → (↑Γ(𝔸(n₂; S), ⊤) : Type (max u v)))
          (coord T i_1) :
        (↑Γ(𝔸(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) (Scheme.Hom.appTop (reindex i S ≫ map n₁ f)) :
            (a : (↑Γ(𝔸(n₁; T), ⊤) : Type (max u v))) → (↑Γ(𝔸(n₂; S), ⊤) : Type (max u v)))
          (coord T i_1) :
        (↑Γ(𝔸(n₂; S), ⊤) : Type (max u v)))
⊢ map n₂ f ≫ reindex i T = reindex i S ≫ map n₁ f

Tactic:
apply hom_ext

Premises used: AlgebraicGeometry.AffineSpace.hom_ext
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n₁ n₂ : Type v
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
⊢ (map n₂ f ≫ reindex i T) ≫ AffineSpace.{v, u} n₁ T ↘ T = (reindex i S ≫ map n₁ f) ≫ AffineSpace.{v, u} n₁ T ↘ T

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n₁ n₂ : Type v
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
⊢ ∀ (i_1 : n₁),
    Eq (α := (↑Γ(𝔸(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) (Scheme.Hom.appTop (map n₂ f ≫ reindex i T)) :
            (a : (↑Γ(𝔸(n₁; T), ⊤) : Type (max u v))) → (↑Γ(𝔸(n₂; S), ⊤) : Type (max u v)))
          (coord T i_1) :
        (↑Γ(𝔸(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) (Scheme.Hom.appTop (reindex i S ≫ map n₁ f)) :
            (a : (↑Γ(𝔸(n₁; T), ⊤) : Type (max u v))) → (↑Γ(𝔸(n₂; S), ⊤) : Type (max u v)))
          (coord T i_1) :
        (↑Γ(𝔸(n₂; S), ⊤) : Type (max u v)))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S X : Scheme
inst : X.Over S
n : Type vᵒᵖ
w :
  ∀ (x : Scheme),
    NatTrans.app
        {
          app :=
            reindex
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Quiver.Hom.unop (𝟙 n))) :
                (a : (fun (X : Type v) ↦ X) (Opposite.unop n)) → (fun (X : Type v) ↦ X) (Opposite.unop n)),
          naturality := ⋯ }
        x =
      NatTrans.app
        (𝟙
          { obj := AffineSpace.{v, u} (Opposite.unop n), map := fun {X Y : Scheme} ↦ map (Opposite.unop n), map_id := ⋯,
            map_comp := ⋯ : Scheme ⥤ Scheme })
        x
⊢ {
      app :=
        reindex
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Quiver.Hom.unop (𝟙 n))) :
            (a : (fun (X : Type v) ↦ X) (Opposite.unop n)) → (fun (X : Type v) ↦ X) (Opposite.unop n)),
      naturality := ⋯ } =
    𝟙
      { obj := AffineSpace.{v, u} (Opposite.unop n), map := fun {X Y : Scheme} ↦ map (Opposite.unop n), map_id := ⋯,
        map_comp := ⋯ : Scheme ⥤ Scheme }

Tactic:
ext : 2
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S X : Scheme
inst : X.Over S
n : Type vᵒᵖ
x : Scheme
⊢ NatTrans.app
      {
        app :=
          reindex
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Quiver.Hom.unop (𝟙 n))) :
              (a : (fun (X : Type v) ↦ X) (Opposite.unop n)) → (fun (X : Type v) ↦ X) (Opposite.unop n)),
        naturality := ⋯ }
      x =
    NatTrans.app
      (𝟙
        { obj := AffineSpace.{v, u} (Opposite.unop n), map := fun {X Y : Scheme} ↦ map (Opposite.unop n), map_id := ⋯,
          map_comp := ⋯ : Scheme ⥤ Scheme })
      x

Tactic:
reindex_id _

Premises used: AlgebraicGeometry.AffineSpace.homOfVector, AlgebraicGeometry.AffineSpace, CategoryTheory.Limits.limit, AlgebraicGeometry.AffineSpace.reindex, CategoryTheory.Limits.limit.lift, AlgebraicGeometry.AffineSpace.reindex_id
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S X : Scheme
inst : X.Over S
n : Type vᵒᵖ
x : Scheme
⊢ NatTrans.app
      {
        app :=
          reindex
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Quiver.Hom.unop (𝟙 n))) :
              (a : (fun (X : Type v) ↦ X) (Opposite.unop n)) → (fun (X : Type v) ↦ X) (Opposite.unop n)),
        naturality := ⋯ }
      x =
    NatTrans.app
      (𝟙
        { obj := AffineSpace.{v, u} (Opposite.unop n), map := fun {X Y : Scheme} ↦ map (Opposite.unop n), map_id := ⋯,
          map_comp := ⋯ : Scheme ⥤ Scheme })
      x

Tactic:
exact reindex_id _

Premises used: AlgebraicGeometry.AffineSpace.reindex_id
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
X_1 Y Z : Type vᵒᵖ
f : X_1 ⟶ Y
g : Y ⟶ Z
w :
  ∀ (x : Scheme),
    Eq (α :=
      { obj := AffineSpace.{v, u} (Opposite.unop X_1), map := fun {X Y : Scheme} ↦ map (Opposite.unop X_1), map_id := ⋯,
              map_comp := ⋯ : Scheme ⥤ Scheme }.obj
          x ⟶
        { obj := AffineSpace.{v, u} (Opposite.unop Z), map := fun {X Y : Scheme} ↦ map (Opposite.unop Z), map_id := ⋯,
              map_comp := ⋯ : Scheme ⥤ Scheme }.obj
          x)
      (NatTrans.app
        {
          app :=
            reindex
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g).unop) :
                (a : (fun (X : Type v) ↦ X) (Opposite.unop Z)) → (fun (X : Type v) ↦ X) (Opposite.unop X_1)),
          naturality := ⋯ }
        x)
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          { obj := AffineSpace.{v, u} (Opposite.unop Y), map := fun {X Y_1 : Scheme} ↦ map (Opposite.unop Y),
            map_id := ⋯, map_comp := ⋯ })
          {
            app :=
              reindex
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.unop) :
                  (a : (fun (X : Type v) ↦ X) (Opposite.unop Y)) → (fun (X : Type v) ↦ X) (Opposite.unop X_1)),
            naturality := ⋯ }
          {
            app :=
              reindex
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g.unop) :
                  (a : (fun (X : Type v) ↦ X) (Opposite.unop Z)) → (fun (X : Type v) ↦ X) (Opposite.unop Y)),
            naturality := ⋯ })
        x)
⊢ Eq (α :=
    { obj := AffineSpace.{v, u} (Opposite.unop X_1), map := fun {X Y : Scheme} ↦ map (Opposite.unop X_1), map_id := ⋯,
        map_comp := ⋯ : Scheme ⥤ Scheme } ⟶
      { obj := AffineSpace.{v, u} (Opposite.unop Z), map := fun {X Y : Scheme} ↦ map (Opposite.unop Z), map_id := ⋯,
        map_comp := ⋯ })
    {
      app :=
        reindex
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g).unop) :
            (a : (fun (X : Type v) ↦ X) (Opposite.unop Z)) → (fun (X : Type v) ↦ X) (Opposite.unop X_1)),
      naturality := ⋯ }
    (CategoryStruct.comp (Y :=
      { obj := AffineSpace.{v, u} (Opposite.unop Y), map := fun {X Y_1 : Scheme} ↦ map (Opposite.unop Y), map_id := ⋯,
        map_comp := ⋯ })
      {
        app :=
          reindex
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.unop) :
              (a : (fun (X : Type v) ↦ X) (Opposite.unop Y)) → (fun (X : Type v) ↦ X) (Opposite.unop X_1)),
        naturality := ⋯ }
      {
        app :=
          reindex
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g.unop) :
              (a : (fun (X : Type v) ↦ X) (Opposite.unop Z)) → (fun (X : Type v) ↦ X) (Opposite.unop Y)),
        naturality := ⋯ })

Tactic:
ext : 2
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
X_1 Y Z : Type vᵒᵖ
f : X_1 ⟶ Y
g : Y ⟶ Z
x : Scheme
w :
  Eq (α := AffineSpace.{v, u} (Opposite.unop X_1) x ⟶ AffineSpace.{v, u} (Opposite.unop Z) x)
    (reindex (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (g.unop ≫ f.unop)) : (a : Opposite.unop Z) → Opposite.unop X_1)
      x)
    (CategoryStruct.comp (Y := AffineSpace.{v, u} (Opposite.unop Y) x)
      (reindex (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.unop) : (a : Opposite.unop Y) → Opposite.unop X_1) x)
      (reindex (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g.unop) : (a : Opposite.unop Z) → Opposite.unop Y) x))
⊢ Eq (α :=
    { obj := AffineSpace.{v, u} (Opposite.unop X_1), map := fun {X Y : Scheme} ↦ map (Opposite.unop X_1), map_id := ⋯,
            map_comp := ⋯ : Scheme ⥤ Scheme }.obj
        x ⟶
      { obj := AffineSpace.{v, u} (Opposite.unop Z), map := fun {X Y : Scheme} ↦ map (Opposite.unop Z), map_id := ⋯,
            map_comp := ⋯ : Scheme ⥤ Scheme }.obj
        x)
    (NatTrans.app
      {
        app :=
          reindex
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g).unop) :
              (a : (fun (X : Type v) ↦ X) (Opposite.unop Z)) → (fun (X : Type v) ↦ X) (Opposite.unop X_1)),
        naturality := ⋯ }
      x)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        { obj := AffineSpace.{v, u} (Opposite.unop Y), map := fun {X Y_1 : Scheme} ↦ map (Opposite.unop Y), map_id := ⋯,
          map_comp := ⋯ })
        {
          app :=
            reindex
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.unop) :
                (a : (fun (X : Type v) ↦ X) (Opposite.unop Y)) → (fun (X : Type v) ↦ X) (Opposite.unop X_1)),
          naturality := ⋯ }
        {
          app :=
            reindex
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g.unop) :
                (a : (fun (X : Type v) ↦ X) (Opposite.unop Z)) → (fun (X : Type v) ↦ X) (Opposite.unop Y)),
          naturality := ⋯ })
      x)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
X_1 Y Z : Type vᵒᵖ
f : X_1 ⟶ Y
g : Y ⟶ Z
x : Scheme
⊢ Eq (α := AffineSpace.{v, u} (Opposite.unop X_1) x ⟶ AffineSpace.{v, u} (Opposite.unop Z) x)
    (reindex (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (g.unop ≫ f.unop)) : (a : Opposite.unop Z) → Opposite.unop X_1)
      x)
    (CategoryStruct.comp (Y := AffineSpace.{v, u} (Opposite.unop Y) x)
      (reindex (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.unop) : (a : Opposite.unop Y) → Opposite.unop X_1) x)
      (reindex (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g.unop) : (a : Opposite.unop Z) → Opposite.unop Y) x))

Tactic:
reindex_comp _ _ _

Premises used: AlgebraicGeometry.AffineSpace.reindex_comp