awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have e : 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 [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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ Eq (α := Γ(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))))))
have 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))))))
Tactic: rw [← Scheme.Hom.comp_appTop, homOfVector_over, Scheme.Hom.comp_appTop]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ Eq (α := Γ(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))))))
have 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))))))
Tactic: simp only [Category.assoc, Scheme.ΓSpecIso_naturality, CommRingCat.of_carrier,
            ← Scheme.toSpecΓ_appTop]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
⊢ Eq (α := Γ(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))))))
have 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))))))
Tactic: rw [← Scheme.Hom.comp_appTop_assoc, Scheme.isoSpec, asIso_inv, IsIso.hom_inv_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have e : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [eval₂_X]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R : CommRingCat
⊢ 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)))
have 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)))
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R : CommRingCat
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [isoOfIsAffine_inv_appTop_coord, ← CommRingCat.comp_apply, ← Scheme.ΓSpecIso_inv_naturality,
      CommRingCat.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R : CommRingCat
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R : CommRingCat
⊢ (SpecIso n R).inv ≫ AffineSpace.{v, u} n (Spec R) ↘ Spec R = Spec.map (CommRingCat.ofHom C)
have simp : Spec.map
    ((Scheme.ΓSpecIso R).inv ≫
      CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv) =
  Spec.map (CommRingCat.ofHom C)
Tactic: simp only [SpecIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, Scheme.Spec_map,
    Quiver.Hom.unop_op, Category.assoc, isoOfIsAffine_inv_over, Scheme.isoSpec_Spec_inv,
    ← Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R : CommRingCat
⊢ Spec.map
      ((Scheme.ΓSpecIso R).inv ≫
        CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv) =
    Spec.map (CommRingCat.ofHom C)
have e_f : (Scheme.ΓSpecIso R).inv ≫
    CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
  CommRingCat.ofHom C
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R : CommRingCat
⊢ (Scheme.ΓSpecIso R).inv ≫
      CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    CommRingCat.ofHom C
have e_f : CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
  (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C
Tactic: rw [Iso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R : CommRingCat
⊢ CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C
have e_f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ map n f ≫ toSpecMvPoly n T = toSpecMvPoly n S
have a : Eq (α := n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
  ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
      (map n f ≫ toSpecMvPoly n T) :
    n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
  ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) :
    n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
Tactic: apply (toSpecMvPolyIntEquiv _).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ Eq (α := n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        (map n f ≫ toSpecMvPoly n T) :
      n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) :
      n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
have a : ∀ (i : n),
  Eq (α := (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        (map n f ≫ toSpecMvPoly n T) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
i : n
⊢ Eq (α := (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        (map n f ≫ toSpecMvPoly n T) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
have a : 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)) :
        (a : (↑Γ(𝔸(n; T), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
      ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; T) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; T), ⊤) : Type (max u v))) (toSpecMvPoly n T)
        i) :
    (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
  ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
    (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
Tactic: rw [toSpecMvPolyIntEquiv_comp, ← coord, map_appTop_coord, coord]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
i : n
a :
  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)) :
          (a : (↑Γ(𝔸(n; T), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; T) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; T), ⊤) : Type (max u v))) (toSpecMvPoly n T)
          i) :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
⊢ Eq (α := (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        (map n f ≫ toSpecMvPoly n T) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
have a₁ : 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)) :
        (a : (↑Γ(𝔸(n; T), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
      (coord T i) :
    (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
  ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
    (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
Tactic: rw [toSpecMvPolyIntEquiv_comp, ← coord, map_appTop_coord, coord]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
i : n
a :
  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)) :
          (a : (↑Γ(𝔸(n; T), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; T) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; T), ⊤) : Type (max u v))) (toSpecMvPoly n T)
          i) :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
a₁ :
  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)) :
          (a : (↑Γ(𝔸(n; T), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        (coord T i) :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
⊢ Eq (α := (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        (map n f ≫ toSpecMvPoly n T) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
have a₂ : coord S i =
  (toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i
Tactic: rw [toSpecMvPolyIntEquiv_comp, ← coord, map_appTop_coord, coord]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
i : n
a :
  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)) :
          (a : (↑Γ(𝔸(n; T), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; T) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; T), ⊤) : Type (max u v))) (toSpecMvPoly n T)
          i) :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
a₁ :
  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)) :
          (a : (↑Γ(𝔸(n; T), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        (coord T i) :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
a₂ :
  coord S i =
    (toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i
⊢ Eq (α := (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
        (map n f ≫ toSpecMvPoly n T) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
    ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
have a₃ : Eq (α := (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
  ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
    (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
  ((toSpecMvPolyIntEquiv n : (a : 𝔸(n; S) ⟶ Spec ℤ[n]) → n → (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) (toSpecMvPoly n S) i :
    (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
Tactic: rw [toSpecMvPolyIntEquiv_comp, ← coord, map_appTop_coord, coord]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
⊢ map n (f ≫ g) = map n f ≫ map n g
have h₁ : map n (f ≫ g) ≫ AffineSpace.{v, u_1} n S'' ↘ S'' = (map n f ≫ map n g) ≫ AffineSpace.{v, u_1} n S'' ↘ S''
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
h₁ : map n (f ≫ g) ≫ AffineSpace.{v, u_1} n S'' ↘ S'' = (map n f ≫ map n g) ≫ AffineSpace.{v, u_1} n S'' ↘ S''
⊢ map n (f ≫ g) = map n f ≫ map n g
have h₂ : ∀ (i : n),
  Eq (α := (↑Γ(𝔸(n; S), ⊤) : Type (max u_1 v)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u_1 v)) →+* (↑S : Type (max u_1 v))) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (map n (f ≫ g))) :
          (a : (↑Γ(𝔸(n; S''), ⊤) : Type (max u_1 v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u_1 v)))
        (coord S'' i) :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u_1 v)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u_1 v)) →+* (↑S : Type (max u_1 v))) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (map n f ≫ map n g)) :
          (a : (↑Γ(𝔸(n; S''), ⊤) : Type (max u_1 v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u_1 v)))
        (coord S'' i) :
      (↑Γ(𝔸(n; S), ⊤) : Type (max u_1 v)))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
⊢ map n (Spec.map φ) =
    (SpecIso n S).hom ≫ Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv
have rw : (SpecIso n S).inv ≫ map n (Spec.map φ) =
  Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv
Tactic: rw [← Iso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
⊢ (SpecIso n S).inv ≫ map n (Spec.map φ) =
    Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv
have h₁ : 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)
Tactic: ext1
-- 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)
    (((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)
⊢ (SpecIso n S).inv ≫ map n (Spec.map φ) =
    Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv
have h₂ : ∀ (i : n),
  Eq (α := (↑Γ(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) (Scheme.Hom.appTop ((SpecIso n S).inv ≫ map n (Spec.map φ))) :
          (a : (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v))) →
            (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤) : Type (max u v)))
        (coord (Spec R) i) :
      (↑Γ(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)
            (Scheme.Hom.appTop
              (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv)) :
          (a : (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v))) →
            (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤) : Type (max u v)))
        (coord (Spec R) i) :
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤) : Type (max u v)))
Tactic: ext1