-- Mathlib/AlgebraicGeometry/AffineSpace.lean
lemma map_Spec_map {R S : CommRingCat.{max u v}} (φ : R ⟶ S) :
    map n (Spec.map φ) =
      (SpecIso n S).hom ≫ Spec.map (CommRingCat.ofHom (MvPolynomial.map φ.hom)) ≫
        (SpecIso n R).inv

Proof state:
case h₂
n : Type v
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop ((SpecIso n S).inv ≫ map n (Spec.map φ)))) (coord (Spec R) i✝) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop
          (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv)))
      (coord (Spec R) i✝)

Tactic:
simp only [Scheme.comp_coeBase, TopologicalSpace.Opens.map_comp_obj,
  TopologicalSpace.Opens.map_top, Scheme.comp_app, CommRingCat.comp_apply]

Result:
case h₂
n : Type v
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n S).inv ⊤))
      ((ConcreteCategory.hom (Scheme.Hom.app (map n (Spec.map φ)) ⊤)) (coord (Spec R) i✝)) =
    (ConcreteCategory.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
      ((ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝))

Proof state:
case h₁
n : Type v
R S : CommRingCat
φ : R ⟶ S
⊢ Spec.map (φ ≫ CommRingCat.ofHom C) = Spec.map (CommRingCat.ofHom ((MvPolynomial.map (CommRingCat.Hom.hom φ)).comp C))

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

Result:
no goals

Proof state:
case h₁
n : Type v
R S : CommRingCat
φ : R ⟶ S
⊢ ((SpecIso n S).inv ≫ map n (Spec.map φ)) ≫ 𝔸(n; Spec R) ↘ Spec R =
    (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv) ≫
      𝔸(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]

Result:
case h₁
n : Type v
R S : CommRingCat
φ : R ⟶ S
⊢ Spec.map (φ ≫ CommRingCat.ofHom C) = Spec.map (CommRingCat.ofHom ((MvPolynomial.map (CommRingCat.Hom.hom φ)).comp C))

Proof state:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝) = ?m.309967

Tactic:
exact SpecIso_inv_appTop_coord _ _

Result:
no goals

Proof state:
case h₂
n : Type v
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n S).inv ⊤))
      ((ConcreteCategory.hom (Scheme.Hom.app (map n (Spec.map φ)) ⊤)) (coord (Spec R) i✝)) =
    (ConcreteCategory.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
      ((ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝))

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

Result:
case h₂
n : Type v
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n S).inv ⊤)) (coord (Spec S) i✝) =
    (ConcreteCategory.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
      ((ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝))

Proof state:
case h₂
n : Type v
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n S).inv ⊤)) (coord (Spec S) i✝) =
    (ConcreteCategory.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
      ((ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i✝))

Tactic:
rw [SpecIso_inv_appTop_coord, ← CommRingCat.comp_apply, ← Scheme.ΓSpecIso_inv_naturality,
    CommRingCat.comp_apply, ConcreteCategory.hom_ofHom, map_X]

Result:
no goals

Proof state:
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

Tactic:
rw [← Iso.inv_comp_eq]

Result:
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

Proof state:
case h₂
n : Type v
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n S).inv ⊤)) (coord (Spec S) i✝) =
    (ConcreteCategory.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
      ((ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝))

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

Result:
case h₂
n : Type v
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n S).inv ⊤)) (coord (Spec S) i✝) =
    (ConcreteCategory.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
      ((ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i✝))

Proof state:
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

Tactic:
ext1

Result:
case h₁
n : Type v
R S : CommRingCat
φ : R ⟶ S
⊢ ((SpecIso n S).inv ≫ map n (Spec.map φ)) ≫ 𝔸(n; Spec R) ↘ Spec R =
    (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv) ≫
      𝔸(n; Spec R) ↘ Spec R

case h₂
n : Type v
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop ((SpecIso n S).inv ≫ map n (Spec.map φ)))) (coord (Spec R) i✝) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop
          (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv)))
      (coord (Spec R) i✝)

Proof state:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.app (map n (Spec.map φ)) ⊤)) (coord (Spec R) i✝) = ?m.309828

Tactic:
exact map_appTop_coord _ _

Result:
no goals