-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R_1 A_1 B C : CommRingCat
inst : TopologicalSpace (↑R_1 : Type u)
σ : Type v
R A : CommRingCat
inst_1 : TopologicalSpace (↑R : Type (max u v))
inst_2 : IsTopologicalRing (↑R : Type (max u v))
f : of (MvPolynomial σ (↑A : Type (max u v))) ⟶ R
hf :
  ∀ (x : (↑A : Type (max u v))),
    Eq (α := (↑(of (↑R : Type (max u v))) : Type (max u v)))
      ((@RingHom.comp _ (MvPolynomial σ (↑A : Type (max u v))) _ _
              (AddMonoidAlgebra.nonAssocSemiring : NonAssocSemiring (AddMonoidAlgebra (↑A : Type (max u v)) (σ →₀ ℕ))) _
              (Hom.hom
                  ((fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦
                      ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
                    ((fun (f : of (MvPolynomial σ (↑A : Type (max u v))) ⟶ R) ↦
                        ((ofHom MvPolynomial.C ≫ f, fun (i : σ) ↦
                            (ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦
                                  (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) f :
                                (a : (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v))) →
                                  (↑R : Type (max u v)))
                              (MvPolynomial.X i)) :
                          (A ⟶ R) × (σ → (↑R : Type (max u v)))))
                      f)) :
                (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v)) →+*
                  (↑(of (↑R : Type (max u v))) : Type (max u v)))
              MvPolynomial.C :
            (a : (↑A : Type (max u v))) → (↑(of (↑R : Type (max u v))) : Type (max u v)))
          x :
        (↑(of (↑R : Type (max u v))) : Type (max u v)))
      (((Hom.hom f).comp MvPolynomial.C : (a : (↑A : Type (max u v))) → (↑(of (↑R : Type (max u v))) : Type (max u v)))
          x :
        (↑(of (↑R : Type (max u v))) : Type (max u v)))
hf₁ :
  ∀ (i : σ),
    Eq (α := (↑(of (↑R : Type (max u v))) : Type (max u v)))
      (((Hom.hom
                ((fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
                  ((fun (f : of (MvPolynomial σ (↑A : Type (max u v))) ⟶ R) ↦
                      ((ofHom MvPolynomial.C ≫ f, fun (i : σ) ↦
                          (ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦
                                (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) f :
                              (a : (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v))) →
                                (↑R : Type (max u v)))
                            (MvPolynomial.X i)) :
                        (A ⟶ R) × (σ → (↑R : Type (max u v)))))
                    f)) :
              (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v)) →+*
                (↑(of (↑R : Type (max u v))) : Type (max u v))) :
            (a : MvPolynomial σ (↑A : Type (max u v))) → (↑(of (↑R : Type (max u v))) : Type (max u v)))
          (MvPolynomial.X i) :
        (↑(of (↑R : Type (max u v))) : Type (max u v)))
      ((Hom.hom f : (a : MvPolynomial σ (↑A : Type (max u v))) → (↑(of (↑R : Type (max u v))) : Type (max u v)))
          (MvPolynomial.X i) :
        (↑(of (↑R : Type (max u v))) : Type (max u v)))
⊢ (fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
      ((fun (f : of (MvPolynomial σ (↑A : Type (max u v))) ⟶ R) ↦
          ((ofHom MvPolynomial.C ≫ f, fun (i : σ) ↦
              (ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                    (CC := carrier) f :
                  (a : (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v))) → (↑R : Type (max u v)))
                (MvPolynomial.X i)) :
            (A ⟶ R) × (σ → (↑R : Type (max u v)))))
        f) =
    f

Tactic:
ext