awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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
⊢ Membership.mem (γ := Set (A ⟶ R)) (Set.range fun (x : B ⟶ R) ↦ f ≫ x) x ↔
    Membership.mem (γ := Set (A ⟶ R))
      (⋂ (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
have h : (∃ (y : B ⟶ R), f ≫ y = x) ↔
  ∀ (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))
Tactic: simp only [Set.mem_range, Set.mem_iInter, Set.mem_setOf_eq, Subtype.forall, RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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
⊢ (∃ (y : B ⟶ R), f ≫ y = x) ↔
    ∀ (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))
have h : (∃ (y : B ⟶ R), f ≫ y = x) →
  ∀ (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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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
h :
  (∃ (y : B ⟶ R), f ≫ y = x) →
    ∀ (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) ↔
    ∀ (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))
have h₁ : (∀ (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: constructor
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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
H :
  ∀ (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))
⊢ f ≫
      ofHom
        (((Hom.hom f).liftOfSurjective hf :
            (a : { g : (↑A : Type u) →+* (↑R : Type u) // RingHom.ker (Hom.hom f) ≤ RingHom.ker g }) →
              (↑B : Type u) →+* (↑R : Type u))
          (Subtype.mk (p := fun (g : (↑A : Type u) →+* (↑R : Type u)) ↦
            LE.le (α := Ideal (↑A : Type u)) (RingHom.ker (Hom.hom f)) (RingHom.ker g)) (Hom.hom x) H)) =
    x
have hf₁ : ∀ (x_1 : (↑A : Type u)),
  Eq (α := (↑R : Type u))
    ((Hom.hom
            (f ≫
              ofHom
                (((Hom.hom f).liftOfSurjective hf :
                    (a : { g : (↑A : Type u) →+* (↑R : Type u) // RingHom.ker (Hom.hom f) ≤ RingHom.ker g }) →
                      (↑B : Type u) →+* (↑R : Type u))
                  (Subtype.mk (p := fun (g : (↑A : Type u) →+* (↑R : Type u)) ↦
                    LE.le (α := Ideal (↑A : Type u)) (RingHom.ker (Hom.hom f)) (RingHom.ker g)) (Hom.hom x) H))) :
          (a : (↑A : Type u)) → (↑R : Type u))
        x_1 :
      (↑R : Type u))
    ((Hom.hom x : (a : (↑A : Type u)) → (↑R : Type u)) x_1 : (↑R : Type u))
Tactic: ext
-- 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
⊢ (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 : ∀ (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: ext
-- 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))
fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))
⊢ (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
have 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)))
Tactic: ext
-- 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))
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)))
⊢ (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
have 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
Tactic: ext
-- 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))
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceHom] fun (fx : (A ⟶ R) × (σ → (↑R : Type (max u v)))) ↦
    ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)
have 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))
Tactic: refine continuous_induced_rng.mpr ?_
-- 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))
⊢ 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))
have 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
Tactic: refine continuous_pi fun p ↦ ?_
-- 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))
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
have 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)))
Tactic: simp only [Function.comp_apply, hom_ofHom, MvPolynomial.coe_eval₂Hom, MvPolynomial.eval₂_eq]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (hypothesis)
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)
⊢ IsClosedEmbedding (Y := (a : (↑A : Type u)) → (↑R : Type u)) fun (f : A ⟶ R) ↦
    (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑R : Type u))
have 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))
Tactic: have : Function.Surjective f := Function.LeftInverse.surjective (g := .X) fun x ↦ by simp [f]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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 (Y := (a : (↑A : Type u)) → (↑R : Type u)) fun (f : A ⟶ R) ↦
    (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑R : Type u))
have 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)
Tactic: convert!
    ((mvPolynomialHomeomorph A R (.of _)).trans
          (.uniqueProd (⊥_ CommRingCat ⟶ R) _)).isClosedEmbedding.comp
      (isClosedEmbedding_precomp_of_surjective f this) using
    2 with g
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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
⊢ 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)
have 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))
Tactic: ext x