-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[simp]
lemma SpecIso_hom_appTop (R : CommRingCat.{max u v}) :
    (SpecIso n R).hom.appTop = (Scheme.ΓSpecIso _).hom ≫
      CommRingCat.ofHom (eval₂Hom ((Scheme.ΓSpecIso _).inv ≫
        (𝔸(n; Spec R) ↘ Spec R).appTop).hom (coord (Spec R)))

Proof state:
case e_a.hf.hC.a
n : Type v
R : CommRingCat
x✝ : ↑R
⊢ ((CommRingCat.Hom.hom
            ((mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
              CommRingCat.ofHom
                (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R))))).comp
        C)
      x✝ =
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
              (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
                (coord (Spec R))))).comp
        C)
      x✝

Tactic:
simp

Result:
no goals

Proof state:
case e_a.hf.hX
n : Type v
R : CommRingCat
⊢ ∀ (i : n),
    (CommRingCat.Hom.hom
          ((mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
            CommRingCat.ofHom
              (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R)))))
        (X i) =
      (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
              (coord (Spec R)))))
        (X i)

Tactic:
simp

Result:
no goals

Proof state:
case e_a.hf
n : Type v
R : CommRingCat
⊢ CommRingCat.Hom.hom
      ((mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
        CommRingCat.ofHom
          (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R)))) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
          (coord (Spec R))))

Tactic:
apply ringHom_ext'

Result:
case e_a.hf.hC
n : Type v
R : CommRingCat
⊢ (CommRingCat.Hom.hom
          ((mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
            CommRingCat.ofHom
              (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R))))).comp
      C =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
              (coord (Spec R))))).comp
      C

case e_a.hf.hX
n : Type v
R : CommRingCat
⊢ ∀ (i : n),
    (CommRingCat.Hom.hom
          ((mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
            CommRingCat.ofHom
              (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R)))))
        (X i) =
      (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
              (coord (Spec R)))))
        (X i)

Proof state:
case e_a.hf.hC
n : Type v
R : CommRingCat
⊢ (CommRingCat.Hom.hom
          ((mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
            CommRingCat.ofHom
              (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R))))).comp
      C =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
              (coord (Spec R))))).comp
      C

Tactic:
ext

Result:
case e_a.hf.hC.a
n : Type v
R : CommRingCat
x✝ : ↑R
⊢ ((CommRingCat.Hom.hom
            ((mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
              CommRingCat.ofHom
                (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R))))).comp
        C)
      x✝ =
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
              (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
                (coord (Spec R))))).comp
        C)
      x✝

Proof state:
case e_a
n : Type v
R : CommRingCat
⊢ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
      CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R))) =
    CommRingCat.ofHom
      (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
        (coord (Spec R)))

Tactic:
ext : 1

Result:
case e_a.hf
n : Type v
R : CommRingCat
⊢ CommRingCat.Hom.hom
      ((mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
        CommRingCat.ofHom
          (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R)))) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
          (coord (Spec R))))

Proof state:
n : Type v
R : CommRingCat
⊢ Scheme.Hom.appTop (SpecIso n R).hom =
    (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).hom ≫
      CommRingCat.ofHom
        (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
          (coord (Spec R)))

Tactic:
simp only [SpecIso, Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom,
  RingEquiv.toRingHom_eq_coe, Scheme.Spec_map, Quiver.Hom.unop_op, Scheme.comp_coeBase,
  TopologicalSpace.Opens.map_comp_obj, TopologicalSpace.Opens.map_top, Scheme.comp_app,
  isoOfIsAffine_hom_appTop, Scheme.ΓSpecIso_naturality_assoc]

Result:
n : Type v
R : CommRingCat
⊢ (Scheme.ΓSpecIso (CommRingCat.mk✝ (MvPolynomial n ↑R))).hom ≫
      (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
        CommRingCat.ofHom
          (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R))) =
    (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).hom ≫
      CommRingCat.ofHom
        (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
          (coord (Spec R)))

Proof state:
n : Type v
R : CommRingCat
⊢ (Scheme.ΓSpecIso (CommRingCat.mk✝ (MvPolynomial n ↑R))).hom ≫
      (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
        CommRingCat.ofHom
          (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R))) =
    (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).hom ≫
      CommRingCat.ofHom
        (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
          (coord (Spec R)))

Tactic:
congr 1

Result:
case e_a
n : Type v
R : CommRingCat
⊢ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.hom ≫
      CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R))) (coord (Spec R))) =
    CommRingCat.ofHom
      (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
        (coord (Spec R)))