awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : T1Space.{u} (↑R : Type u)
f : A ⟶ B
hf :
  Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f) :
      (a : (↑A : Type u)) → (↑B : Type u))
this :
  IsClosed[instTopologicalSpaceHom]
    (⋂ (i : ↥(RingHom.ker (Hom.hom f))),
      {f_1 : A ⟶ R |
        Eq (α := (↑R : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  f_1 :
                (a : (↑A : Type u)) → (↑R : Type u))
              (↑i : (↑A : Type u)) :
            (↑R : Type u))
          (0 : (↑R : Type u))})
x : A ⟶ R
⊢ (∀ (a : (↑A : Type u))
      (b :
        Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
          (0 : (↑B : Type u))),
      Eq (α := (↑R : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) x :
              (a : (↑A : Type u)) → (↑R : Type u))
            a :
          (↑R : Type u))
        (0 : (↑R : Type u))) →
    ∃ (y : B ⟶ R), f ≫ y = x

Tactic:
exact fun H ↦ ⟨CommRingCat.ofHom (RingHom.liftOfSurjective f.hom hf ⟨x.hom, H⟩),
      by ext; simp [RingHom.liftOfRightInverse_comp_apply]⟩
-- 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
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)))

Tactic:
simp
-- 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
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:
simp
-- 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))
fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))
fst :
  ∀ (x : (↑A : Type (max u v))),
    Eq (α := (↑R : Type (max u v)))
      ((Hom.hom
              ((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)))))
                  ((fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦
                      ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
                    fx)).1 :
            (a : (↑A : Type (max u v))) → (↑R : Type (max u v)))
          x :
        (↑R : Type (max u v)))
      ((Hom.hom fx.1 : (a : (↑A : Type (max u v))) → (↑R : Type (max u v))) x : (↑R : Type (max u v)))
snd :
  ∀ (x : σ),
    ((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)))))
            ((fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
              fx)).2
        x =
      fx.2 x
⊢ (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)))))
      ((fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)) fx) =
    fx

Tactic:
ext
-- 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))
fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))
x : (↑A : Type (max u v))
⊢ Eq (α := (↑R : Type (max u v)))
    ((Hom.hom
            ((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)))))
                ((fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
                  fx)).1 :
          (a : (↑A : Type (max u v))) → (↑R : Type (max u v)))
        x :
      (↑R : Type (max u v)))
    ((Hom.hom fx.1 : (a : (↑A : Type (max u v))) → (↑R : Type (max u v))) x : (↑R : Type (max u v)))

Tactic:
simp
-- 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))
fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))
x : σ
⊢ ((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)))))
          ((fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)) fx)).2
      x =
    fx.2 x

Tactic:
simp
-- 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))
⊢ Continuous[instTopologicalSpaceHom, instTopologicalSpaceProd]
    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))

Tactic:
fun_prop
-- 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))
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceHom] fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦
    ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)

Tactic:
continuous_induced_rng.mpr ?_

Premises used: Iff.mpr, continuous_induced_rng
-- 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))
refine :
  Continuous[instTopologicalSpaceProd, inferInstance]
    ((fun (f : of (MvPolynomial σ (↑A : Type (max u v))) ⟶ R) ↦
        (⇑(Hom.hom f) :
          (a : (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v))) → (↑R : Type (max u v)))) ∘
      fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceHom] fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦
    ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)

Tactic:
refine continuous_induced_rng.mpr ?_

Premises used: Iff.mpr, continuous_induced_rng
-- 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))
⊢ Continuous[instTopologicalSpaceProd, inferInstance]
    ((fun (f : of (MvPolynomial σ (↑A : Type (max u v))) ⟶ R) ↦
        (⇑(Hom.hom f) :
          (a : (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v))) → (↑R : Type (max u v)))) ∘
      fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))

Tactic:
continuous_pi fun p ↦ ?_

Premises used: continuous_pi
-- 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))
refine :
  ∀ (p : (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v))),
    Continuous[instTopologicalSpaceProd, inst_1] fun (a : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦
      ((fun (f : of (MvPolynomial σ (↑A : Type (max u v))) ⟶ R) ↦
            (⇑(Hom.hom f) :
              (a : (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v))) → (↑R : Type (max u v)))) ∘
          fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
        a p
⊢ Continuous[instTopologicalSpaceProd, inferInstance]
    ((fun (f : of (MvPolynomial σ (↑A : Type (max u v))) ⟶ R) ↦
        (⇑(Hom.hom f) :
          (a : (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v))) → (↑R : Type (max u v)))) ∘
      fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))

Tactic:
refine continuous_pi fun p ↦ ?_

Premises used: continuous_pi
-- 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))
p : (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v))
simp :
  Continuous[instTopologicalSpaceProd, inst_1] fun (a : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦
    ∑ d ∈ MvPolynomial.support p,
      HMul.hMul (α := (↑R : Type (max u v))) (β := (↑R : Type (max u v)))
        ((Hom.hom a.1 : (a : (↑A : Type (max u v))) → (↑R : Type (max u v))) (MvPolynomial.coeff d p) :
          (↑R : Type (max u v)))
        (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a.2 i) ((d : (a : σ) → ℕ) i : ℕ) : (↑R : Type (max u v)))
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (a : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦
    ((fun (f : of (MvPolynomial σ (↑A : Type (max u v))) ⟶ R) ↦
          (⇑(Hom.hom f) :
            (a : (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v))) → (↑R : Type (max u v)))) ∘
        fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
      a p

Tactic:
simp only [Function.comp_apply, hom_ofHom, MvPolynomial.coe_eval₂Hom, MvPolynomial.eval₂_eq]

Premises used: MvPolynomial.coe_eval₂Hom, CommRingCat.hom_ofHom, MvPolynomial.eval₂_eq, Function.comp_apply
-- 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))
p : (↑(of (MvPolynomial σ (↑A : Type (max u v)))) : Type (max u v))
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (a : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦
    ∑ d ∈ MvPolynomial.support p,
      HMul.hMul (α := (↑R : Type (max u v))) (β := (↑R : Type (max u v)))
        ((Hom.hom a.1 : (a : (↑A : Type (max u v))) → (↑R : Type (max u v))) (MvPolynomial.coeff d p) :
          (↑R : Type (max u v)))
        (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a.2 i) ((d : (a : σ) → ℕ) i : ℕ) : (↑R : Type (max u v)))

Tactic:
fun_prop
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
inst_2 : T1Space.{u} (↑R : Type u)
f : of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u)) ⟶ A :=
  ofHom (MvPolynomial.eval₂Hom (Hom.hom (initial.to A)) id)
x : (↑A : Type u)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f :
        (a : (↑(of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u))) : Type u)) → (↑A : Type u))
      (MvPolynomial.X x) =
    x

Tactic:
simp [f]
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
inst_2 : T1Space.{u} (↑R : Type u)
f : of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u)) ⟶ A :=
  ofHom (MvPolynomial.eval₂Hom (Hom.hom (initial.to A)) id)
⊢ Function.Surjective (α := (↑(of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u))) : Type u)) (β :=
    (↑A : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f) :
      (a : (↑(of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u))) : Type u)) → (↑A : Type u))

Tactic:
have : Function.Surjective f := Function.LeftInverse.surjective (g := .X) fun x ↦ by simp [f]
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
inst_2 : T1Space.{u} (↑R : Type u)
f : of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u)) ⟶ A :=
  ofHom (MvPolynomial.eval₂Hom (Hom.hom (initial.to A)) id)
this :
  Function.Surjective (α := (↑(of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u))) : Type u)) (β :=
    (↑A : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f) :
      (a : (↑(of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u))) : Type u)) → (↑A : Type u))
⊢ IsClosedEmbedding (X := A ⟶ R) (Y := (↑A : Type u) → (↑R : Type u))
    (Function.comp (β :=
      of (MvPolynomial (↑A : Type u) (↑(of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)) : Type u)) ⟶ R)
      (⇑(Homeomorph.trans
            (mvPolynomialHomeomorph (↑A : Type u) R (of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)))
            (Homeomorph.uniqueProd (⊥_ CommRingCat ⟶ R) ((↑A : Type u) → (↑R : Type u)))) :
        (a :
            of
                (MvPolynomial (↑A : Type u)
                  (↑(of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)) : Type u)) ⟶
              R) →
          (↑A : Type u) → (↑R : Type u))
      fun (x : A ⟶ R) ↦ f ≫ x)

Tactic:
((mvPolynomialHomeomorph A R (.of _)).trans
          (.uniqueProd (⊥_ CommRingCat ⟶ R) _)).isClosedEmbedding.comp
      (isClosedEmbedding_precomp_of_surjective f this)

Premises used: CommRingCat.HomTopology.isClosedEmbedding_precomp_of_surjective, CommRingCat.HomTopology.mvPolynomialHomeomorph, CommRingCat.carrier, Quiver.Hom, CommRingCat, Topology.IsClosedEmbedding.comp, CommRingCat.of, Homeomorph.uniqueProd, Homeomorph.trans, Homeomorph.isClosedEmbedding, CategoryTheory.Limits.initial
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
inst_2 : T1Space.{u} (↑R : Type u)
f : of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u)) ⟶ A :=
  ofHom (MvPolynomial.eval₂Hom (Hom.hom (initial.to A)) id)
this :
  Function.Surjective (α := (↑(of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u))) : Type u)) (β :=
    (↑A : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f) :
      (a : (↑(of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u))) : Type u)) → (↑A : Type u))
h :
  ∀ (g : A ⟶ R),
    Eq (α := (a : (↑A : Type u)) → (↑R : Type u)) (⇑(Hom.hom g) : (a : (↑A : Type u)) → (↑R : Type u))
      (Function.comp (β :=
        of (MvPolynomial (↑A : Type u) (↑(of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)) : Type u)) ⟶ R)
        (⇑(Homeomorph.trans
              (mvPolynomialHomeomorph (↑A : Type u) R (of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)))
              (Homeomorph.uniqueProd (⊥_ CommRingCat ⟶ R) ((↑A : Type u) → (↑R : Type u)))) :
          (a :
              of
                  (MvPolynomial (↑A : Type u)
                    (↑(of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)) : Type u)) ⟶
                R) →
            (↑A : Type u) → (↑R : Type u))
        (fun (x : A ⟶ R) ↦ f ≫ x) g)
⊢ IsClosedEmbedding (Y := (a : (↑A : Type u)) → (↑R : Type u)) fun (f : A ⟶ R) ↦
    (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑R : Type u))

Tactic:
convert!
    ((mvPolynomialHomeomorph A R (.of _)).trans
          (.uniqueProd (⊥_ CommRingCat ⟶ R) _)).isClosedEmbedding.comp
      (isClosedEmbedding_precomp_of_surjective f this) using
    2 with g

Premises used: CommRingCat.HomTopology.isClosedEmbedding_precomp_of_surjective, CommRingCat.HomTopology.mvPolynomialHomeomorph, CommRingCat.carrier, Quiver.Hom, CommRingCat, Topology.IsClosedEmbedding.comp, CommRingCat.of, Homeomorph.uniqueProd, Homeomorph.trans, Homeomorph.isClosedEmbedding, CategoryTheory.Limits.initial
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
inst_2 : T1Space.{u} (↑R : Type u)
f : of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u)) ⟶ A :=
  ofHom (MvPolynomial.eval₂Hom (Hom.hom (initial.to A)) id)
this :
  Function.Surjective (α := (↑(of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u))) : Type u)) (β :=
    (↑A : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f) :
      (a : (↑(of (MvPolynomial (↑A : Type u) (↑(⊥_ CommRingCat) : Type u))) : Type u)) → (↑A : Type u))
g : A ⟶ R
h :
  ∀ (x : (↑A : Type u)),
    Eq (α := (↑R : Type u)) ((Hom.hom g : (a : (↑A : Type u)) → (↑R : Type u)) x : (↑R : Type u))
      (Function.comp (β :=
          of (MvPolynomial (↑A : Type u) (↑(of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)) : Type u)) ⟶
            R)
          (⇑(Homeomorph.trans
                (mvPolynomialHomeomorph (↑A : Type u) R (of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)))
                (Homeomorph.uniqueProd (⊥_ CommRingCat ⟶ R) ((↑A : Type u) → (↑R : Type u)))) :
            (a :
                of
                    (MvPolynomial (↑A : Type u)
                      (↑(of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)) : Type u)) ⟶
                  R) →
              (↑A : Type u) → (↑R : Type u))
          (fun (x : A ⟶ R) ↦ f ≫ x) g x :
        (↑R : Type u))
⊢ Eq (α := (a : (↑A : Type u)) → (↑R : Type u)) (⇑(Hom.hom g) : (a : (↑A : Type u)) → (↑R : Type u))
    (Function.comp (β :=
      of (MvPolynomial (↑A : Type u) (↑(of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)) : Type u)) ⟶ R)
      (⇑(Homeomorph.trans
            (mvPolynomialHomeomorph (↑A : Type u) R (of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)))
            (Homeomorph.uniqueProd (⊥_ CommRingCat ⟶ R) ((↑A : Type u) → (↑R : Type u)))) :
        (a :
            of
                (MvPolynomial (↑A : Type u)
                  (↑(of (↑(colimit.cocone (Functor.empty CommRingCat)).1 : Type u)) : Type u)) ⟶
              R) →
          (↑A : Type u) → (↑R : Type u))
      (fun (x : A ⟶ R) ↦ f ≫ x) g)

Tactic:
ext x