-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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)))
⊢ (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
have 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)))
Tactic: ext