awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
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:
simp [SpecIso]

Premises used: AlgebraicGeometry.AffineSpace.SpecIso
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
i : n
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [isoOfIsAffine_inv_appTop_coord, ← CommRingCat.comp_apply, ← Scheme.ΓSpecIso_inv_naturality,
      CommRingCat.comp_apply]

Premises used: AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality, CommRingCat.comp_apply
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
i : n
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
map_X _ _

Premises used: Set.Mem, Finsupp.onFinset, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.map, AddMonoidAlgebra, Finsupp.mapRange, MvPolynomial.map_X
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact map_X _ _

Premises used: MvPolynomial.map_X
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
simp :
  Spec.map
      ((Scheme.ΓSpecIso R).inv ≫
        CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv) =
    Spec.map (CommRingCat.ofHom C)
⊢ (SpecIso n R).inv ≫ AffineSpace.{v, u} n (Spec R) ↘ Spec R = 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]

Premises used: AlgebraicGeometry.AffineSpace.SpecIso, CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.Iso.op_inv, AlgebraicGeometry.Spec.map_comp, CategoryTheory.Functor.mapIso_inv, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, AlgebraicGeometry.Scheme.Spec_map, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, CategoryTheory.Iso.trans_inv
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
e_f :
  (Scheme.ΓSpecIso R).inv ≫
      CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    CommRingCat.ofHom C
⊢ Spec.map
      ((Scheme.ΓSpecIso R).inv ≫
        CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv) =
    Spec.map (CommRingCat.ofHom C)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
e_f :
  CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C
⊢ (Scheme.ΓSpecIso R).inv ≫
      CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    CommRingCat.ofHom C

Tactic:
rw [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
e_f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C

Tactic:
ext : 2
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
x : (↑(CommRingCat.of (↑((Spec R).presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max u v))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
map_C _ _

Premises used: Set.Mem, MvPolynomial.map_C, Finsupp.onFinset, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.map, AddMonoidAlgebra, Finsupp.mapRange, Finsupp.single
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R : CommRingCat
x : (↑(CommRingCat.of (↑((Spec R).presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max u v))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact map_C _ _

Premises used: MvPolynomial.map_C
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ map n f ≫ AffineSpace.{v, u} n T ↘ T = AffineSpace.{v, u} n S ↘ S ≫ f

Tactic:
pullback.lift_fst _ _ _

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

Tactic:
homOfVector_appTop_coord _ _ _

Premises used: AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
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)))
⊢ map n f ≫ toSpecMvPoly n T = toSpecMvPoly n S

Tactic:
apply (toSpecMvPolyIntEquiv _).injective

Premises used: AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv, Equiv.injective
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S T : Scheme
f : S ⟶ T
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)))
⊢ 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:
ext i
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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
a₃ 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)))
⊢ 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:
rw [toSpecMvPolyIntEquiv_comp, ← coord, map_appTop_coord, coord]

Premises used: AlgebraicGeometry.AffineSpace.coord, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.AffineSpace.map_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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''
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)))
⊢ map n (f ≫ g) = map n f ≫ map n g

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
⊢ 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:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
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:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
rw :
  (SpecIso n S).inv ≫ map n (Spec.map φ) =
    Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv
⊢ map n (Spec.map φ) =
    (SpecIso n S).hom ≫ Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv

Tactic:
rw [← Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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)
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)))
⊢ (SpecIso n S).inv ≫ map n (Spec.map φ) =
    Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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 (MvPolynomial.map (CommRingCat.Hom.hom φ)) C)))
⊢ 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:
simp only [map_over, Category.assoc, SpecIso_inv_over, SpecIso_inv_over_assoc,
      ← Spec.map_comp, ← CommRingCat.ofHom_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.AffineSpace.map_over, AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.AffineSpace.SpecIso_inv_over, CommRingCat.ofHom_comp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
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))
h₃ h₄ :
  Eq (α := Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))) ⟶ Spec R) (Spec.map (φ ≫ CommRingCat.ofHom C))
    (Spec.map (φ ≫ 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)))

Tactic:
rw [map_comp_C, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom]

Premises used: MvPolynomial.map_comp_C, CommRingCat.ofHom_hom, CommRingCat.ofHom_comp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
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)))
| ((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)))

Tactic:
enter [2]
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
⊢ Eq (α := (↑Γ(𝔸(n; Spec 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 := Γ(𝔸(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)))
    (coord (Spec S) i : (↑Γ(𝔸(n; Spec S), ⊤) : Type (max v u)))

Tactic:
map_appTop_coord _ _

Premises used: AlgebraicGeometry.AffineSpace.map_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
⊢ Eq (α := (↑Γ(𝔸(n; Spec 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 := Γ(𝔸(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)))
    (coord (Spec S) i : (↑Γ(𝔸(n; Spec S), ⊤) : Type (max v u)))

Tactic:
exact map_appTop_coord _ _

Premises used: AlgebraicGeometry.AffineSpace.map_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 (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)))
| ((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)))

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

Premises used: AlgebraicGeometry.AffineSpace.map_appTop_coord
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
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]
-- 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:
SpecIso_inv_appTop_coord _ _

Premises used: Set.Mem, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord