awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
⊢ Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R)
    (((SpecIso n S).inv ≫ map n (Spec.map φ)) ≫ AffineSpace.{v, u} n (Spec R) ↘ Spec R)
    ((Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv) ≫
      AffineSpace.{v, u} n (Spec R) ↘ Spec R)
have h₁ : Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R) (Spec.map (φ ≫ CommRingCat.ofHom C))
  (Spec.map (CommRingCat.ofHom (RingHom.comp (MvPolynomial.map (CommRingCat.Hom.hom φ)) C)))
Tactic: simp only [map_over, Category.assoc, SpecIso_inv_over, SpecIso_inv_over_assoc,
      ← Spec.map_comp, ← CommRingCat.ofHom_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
⊢ Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R) (Spec.map (φ ≫ CommRingCat.ofHom C))
    (Spec.map (CommRingCat.ofHom (RingHom.comp (MvPolynomial.map (CommRingCat.Hom.hom φ)) C)))
have h₁ : Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R) (Spec.map (φ ≫ CommRingCat.ofHom C))
  (Spec.map (CommRingCat.ofHom (RingHom.comp C (CommRingCat.Hom.hom φ))))
Tactic: rw [map_comp_C, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
h₁ :
  Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R) (Spec.map (φ ≫ CommRingCat.ofHom C))
    (Spec.map (CommRingCat.ofHom (RingHom.comp C (CommRingCat.Hom.hom φ))))
⊢ Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R) (Spec.map (φ ≫ CommRingCat.ofHom C))
    (Spec.map (CommRingCat.ofHom (RingHom.comp (MvPolynomial.map (CommRingCat.Hom.hom φ)) C)))
have h₂ : Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R) (Spec.map (φ ≫ CommRingCat.ofHom C))
  (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom φ) ≫ CommRingCat.ofHom C))
Tactic: rw [map_comp_C, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
h₁ :
  Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R) (Spec.map (φ ≫ CommRingCat.ofHom C))
    (Spec.map (CommRingCat.ofHom (RingHom.comp C (CommRingCat.Hom.hom φ))))
h₂ :
  Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R) (Spec.map (φ ≫ CommRingCat.ofHom C))
    (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom φ) ≫ CommRingCat.ofHom C))
⊢ Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R) (Spec.map (φ ≫ CommRingCat.ofHom C))
    (Spec.map (CommRingCat.ofHom (RingHom.comp (MvPolynomial.map (CommRingCat.Hom.hom φ)) C)))
have h₃ : Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R) (Spec.map (φ ≫ CommRingCat.ofHom C))
  (Spec.map (φ ≫ CommRingCat.ofHom C))
Tactic: rw [map_comp_C, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
| ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          CommRingCat.carrier) (X := Γ(𝔸(n; Spec S), ⊤)) (Scheme.Hom.app (SpecIso n S).inv ⊤) :
        (a : (↑Γ(𝔸(n; Spec S), ⊤) : Type (max u v))) →
          (↑Γ(Spec (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 := Γ(𝔸(n; Spec R), ⊤)) (Scheme.Hom.app (map n (Spec.map φ)) ⊤) :
          (a : (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; Spec S), ⊤) : Type (max u v)))
        (coord (Spec R) i)) :
    (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤) : Type (max u v)))
have 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 (map n (Spec.map φ)) ⊤) :
      (a : (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; Spec S), ⊤) : Type (max u v)))
    (coord (Spec R) i) :
  (↑Γ(𝔸(n; Spec S), ⊤) : Type (max u v)))
Tactic: enter [2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
| ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          CommRingCat.carrier) (X := Γ(𝔸(n; Spec S), ⊤)) (Scheme.Hom.app (SpecIso n S).inv ⊤) :
        (a : (↑Γ(𝔸(n; Spec S), ⊤) : Type (max u v))) →
          (↑Γ(Spec (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 := Γ(𝔸(n; Spec R), ⊤)) (Scheme.Hom.app (map n (Spec.map φ)) ⊤) :
          (a : (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; Spec S), ⊤) : Type (max u v)))
        (coord (Spec R) i)) :
    (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤) : Type (max u v)))
have 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 (map n (Spec.map φ)) ⊤) :
      (a : (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; Spec S), ⊤) : Type (max u v)))
    (coord (Spec R) i) :
  (↑Γ(𝔸(n; Spec S), ⊤) : Type (max u v)))
Tactic: enter [2]; tactic => exact map_appTop_coord _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have 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)))
Tactic: enter [2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have 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)))
Tactic: enter [2]; tactic => exact SpecIso_inv_appTop_coord _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (hypothesis)
Goal:
n : Type v
S_1 X : Scheme
inst : X.Over S_1
R S : CommRingCat
φ : R ⟶ S
⊢ (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
have this : (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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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
have 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)
Tactic: refine (IsPullback.paste_horiz_iff (.flip <| .of_hasPullback _ _) (map_over f)).mp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ 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)
have 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)
Tactic: simp only [terminal.comp_from, ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ 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)
have 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]))
Tactic: convert! (IsPullback.of_hasPullback _ _).flip
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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]))
⊢ map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])) =
    pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))
have h : map n f ≫ toSpecMvPoly n T = pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))
Tactic: rw [← toSpecMvPoly, ← toSpecMvPoly, map_toSpecMvPoly]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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]))
⊢ map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])) =
    pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))
have h₁ : map n f ≫ toSpecMvPoly n T = toSpecMvPoly n S
Tactic: rw [← toSpecMvPoly, ← toSpecMvPoly, map_toSpecMvPoly]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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
⊢ map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])) =
    pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))
have h₂ : toSpecMvPoly n S = toSpecMvPoly n S
Tactic: rw [← toSpecMvPoly, ← toSpecMvPoly, map_toSpecMvPoly]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S : Scheme
⊢ reindex id S = 𝟙 (AffineSpace.{v, u} n S)
have h₁ : reindex id S ≫ 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 : Scheme
h₁ : reindex id S ≫ AffineSpace.{v, u} n S ↘ S = 𝟙 (AffineSpace.{v, u} n S) ≫ AffineSpace.{v, u} n S ↘ S
⊢ reindex id S = 𝟙 (AffineSpace.{v, u} n S)
have 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)))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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 ⟶ AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₁) S)
    (reindex
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (i ≫ j)) :
        (a : (fun (X : Type v) ↦ X) n₁) → (fun (X : Type v) ↦ X) n₃)
      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))
have h₁ : 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: ext k
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n₁ n₂ : Type v
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
⊢ map n₂ f ≫ reindex i T = reindex i S ≫ map n₁ f
have 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
Tactic: apply hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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
⊢ map n₂ f ≫ reindex i T = reindex i S ≫ map n₁ f
have 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)))
Tactic: apply hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n_1 : Type v
S X : Scheme
inst : X.Over S
n : Type vᵒᵖ
⊢ {
      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 }
have 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 := sorry }
      x =
    NatTrans.app
      (𝟙
        { obj := AffineSpace.{v, u} (Opposite.unop n), map := fun {X Y : Scheme} ↦ map (Opposite.unop n), map_id := sorry,
          map_comp := sorry : Scheme ⥤ Scheme })
      x
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
X_1 Y Z : Type vᵒᵖ
f : X_1 ⟶ Y
g : Y ⟶ Z
⊢ 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 := ⋯ })
have w : ∀ (x : Scheme),
  Eq (α :=
    { obj := AffineSpace.{v, u} (Opposite.unop X_1), map := fun {X Y : Scheme} ↦ map (Opposite.unop X_1), map_id := sorry,
            map_comp := sorry : Scheme ⥤ Scheme }.obj
        x ⟶
      { obj := AffineSpace.{v, u} (Opposite.unop Z), map := fun {X Y : Scheme} ↦ map (Opposite.unop Z), map_id := sorry,
            map_comp := sorry : 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 := sorry }
      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 := sorry,
          map_comp := sorry })
        {
          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 := sorry }
        {
          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 := sorry })
      x)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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 (α :=
    { 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)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (hypothesis)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
⊢ Surjective (Y := ⊤_ Scheme) (terminal.from (Spec ℤ[n]))
have this : IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
Tactic: have := isIso_of_isTerminal specULiftZIsTerminal terminalIsTerminal (terminal.from _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
this : IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
⊢ Surjective (Y := ⊤_ Scheme) (terminal.from (Spec ℤ[n]))
have rw : Surjective (X := Spec ℤ[n]) (Spec.map (CommRingCat.ofHom C))
Tactic: rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),
    MorphismProperty.cancel_right_of_respectsIso (P := @Surjective)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (hypothesis)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : Finite n
⊢ LocallyOfFinitePresentation (Y := ⊤_ Scheme) (terminal.from (Spec ℤ[n]))
have this : IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
Tactic: have := isIso_of_isTerminal specULiftZIsTerminal.{max u v} terminalIsTerminal (terminal.from _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : Finite n
this : IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
⊢ LocallyOfFinitePresentation (Y := ⊤_ Scheme) (terminal.from (Spec ℤ[n]))
have rw : Algebra.FinitePresentation (↑(CommRingCat.of (ULift.{max u v, 0} ℤ)) : Type (max u v)) (↑ℤ[n] : Type (max u v))
Tactic: rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),
    MorphismProperty.cancel_right_of_respectsIso (P := @LocallyOfFinitePresentation),
    HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation), RingHom.FinitePresentation]