awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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:
simp +instances [f]
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : T2Space.{u} (↑R : Type u)
⊢ T2Space.{u} (A ⟶ R)

Tactic:
(isEmbedding_hom R A).t2Space

Premises used: CommRingCat.HomTopology.isEmbedding_hom, Topology.IsEmbedding.t2Space
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
inst_2 : T1Space.{u} (↑R : Type u)
inst_3 : CompactSpace.{u} (↑R : Type u)
⊢ CompactSpace.{u} (A ⟶ R)

Tactic:
(isClosedEmbedding_hom R A).compactSpace

Premises used: CommRingCat.HomTopology.isClosedEmbedding_hom, Topology.IsClosedEmbedding.compactSpace
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
x : (↑B : Type u)
⊢ (Hom.hom fB : (a : (↑PB : Type u)) → (↑B : Type u)) (MvPolynomial.X x) = x

Tactic:
simp [PB, fB]
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
⊢ Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))

Tactic:
have hfB : Function.Surjective fB.hom := fun x ↦ ⟨.X x, by simp [PB, fB]⟩
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
x : (↑C : Type u)
⊢ (Hom.hom fC : (a : (↑PC : Type u)) → (↑C : Type u)) (MvPolynomial.X x) = x

Tactic:
simp [PC, fC]
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
⊢ Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))

Tactic:
have hfC : Function.Surjective fC.hom := fun x ↦ ⟨.X x, by simp [PC, fC]⟩
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC :
  Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))
⊢ IsEmbedding.{u, u} (X := (B ⟶ R) × (C ⟶ R)) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)

Tactic:
have := (isEmbedding_precomp_of_surjective (R := R) fB hfB).prodMap
    (isEmbedding_precomp_of_surjective (R := R) fC hfC)
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC :
  Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))
this :
  IsEmbedding.{u, u} (X := (B ⟶ R) × (C ⟶ R)) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
rw :
  IsEmbedding.{u, u} (X := pushout φ ψ ⟶ R) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Function.comp (β := (B ⟶ R) × (C ⟶ R)) (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
      fun (f : pushout φ ψ ⟶ R) ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))
⊢ IsEmbedding (Y := (B ⟶ R) × (C ⟶ R)) fun (f : pushout φ ψ ⟶ R) ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)

Tactic:
rw [← IsEmbedding.of_comp_iff this]

Premises used: Topology.IsEmbedding.of_comp_iff
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC :
  Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))
this :
  IsEmbedding.{u, u} (X := (B ⟶ R) × (C ⟶ R)) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial ((↑B : Type u) ⊕ (↑C : Type u)) (↑A : Type u))
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim (⇑(Hom.hom (pushout.inl φ ψ)) : (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
        (⇑(Hom.hom (pushout.inr φ ψ)) : (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))))
rw :
  Set.range (ι := (↑B : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (Y := pushout φ ψ) (pushout.inl φ ψ)) :
          (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u)) ∪
      Set.range (ι := (↑C : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (Y := pushout φ ψ) (pushout.inr φ ψ)) :
          (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u)) ⊆
    (↑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            fBC).range :
      Set (↑(pushout φ ψ) : Type u))
⊢ Function.Surjective (α := (↑PBC : Type u)) (β := (↑(pushout φ ψ) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) fBC) :
      (a : (↑PBC : Type u)) → (↑(pushout φ ψ) : Type u))

Tactic:
rw [← RingHom.range_eq_top, ← top_le_iff,
      ← closure_range_union_range_eq_top_of_isPushout (.of_hasPushout _ _), Subring.closure_le]

Premises used: CategoryTheory.IsPushout.of_hasPushout, CommRingCat.closure_range_union_range_eq_top_of_isPushout, top_le_iff, RingHom.range_eq_top, Subring.closure_le
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC :
  Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))
this :
  IsEmbedding.{u, u} (X := (B ⟶ R) × (C ⟶ R)) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial ((↑B : Type u) ⊕ (↑C : Type u)) (↑A : Type u))
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim (⇑(Hom.hom (pushout.inl φ ψ)) : (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
        (⇑(Hom.hom (pushout.inr φ ψ)) : (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))))
x : (↑B : Type u)
⊢ Eq (α := (↑(pushout φ ψ) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) fBC :
          (a : (↑PBC : Type u)) → (↑(pushout φ ψ) : Type u))
        (MvPolynomial.X (Sum.inl x)) :
      (↑(pushout φ ψ) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (Y :=
            pushout φ ψ) (pushout.inl φ ψ) :
          (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
        x :
      (↑(pushout φ ψ) : Type u))

Tactic:
simp [fBC, PBC]
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC :
  Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))
this :
  IsEmbedding.{u, u} (X := (B ⟶ R) × (C ⟶ R)) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial ((↑B : Type u) ⊕ (↑C : Type u)) (↑A : Type u))
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim (⇑(Hom.hom (pushout.inl φ ψ)) : (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
        (⇑(Hom.hom (pushout.inr φ ψ)) : (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))))
x : (↑C : Type u)
⊢ Eq (α := (↑(pushout φ ψ) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) fBC :
          (a : (↑PBC : Type u)) → (↑(pushout φ ψ) : Type u))
        (MvPolynomial.X (Sum.inr x)) :
      (↑(pushout φ ψ) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (Y :=
            pushout φ ψ) (pushout.inr φ ψ) :
          (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))
        x :
      (↑(pushout φ ψ) : Type u))

Tactic:
simp [fBC, PBC]
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC :
  Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))
this :
  IsEmbedding.{u, u} (X := (B ⟶ R) × (C ⟶ R)) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial ((↑B : Type u) ⊕ (↑C : Type u)) (↑A : Type u))
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim (⇑(Hom.hom (pushout.inl φ ψ)) : (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
        (⇑(Hom.hom (pushout.inr φ ψ)) : (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))))
⊢ (∀ (y : (↑B : Type u)),
      ∃ (y_1 : (↑PBC : Type u)),
        Eq (α := (↑(pushout φ ψ) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  fBC :
                (a : (↑PBC : Type u)) → (↑(pushout φ ψ) : Type u))
              y_1 :
            (↑(pushout φ ψ) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  (Y := pushout φ ψ) (pushout.inl φ ψ) :
                (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
              y :
            (↑(pushout φ ψ) : Type u))) ∧
    ∀ (y : (↑C : Type u)),
      ∃ (y_1 : (↑PBC : Type u)),
        Eq (α := (↑(pushout φ ψ) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  fBC :
                (a : (↑PBC : Type u)) → (↑(pushout φ ψ) : Type u))
              y_1 :
            (↑(pushout φ ψ) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  (Y := pushout φ ψ) (pushout.inr φ ψ) :
                (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))
              y :
            (↑(pushout φ ψ) : Type u))

Tactic:
exact ⟨fun x ↦ ⟨.X (.inl x), by simp [fBC, PBC]⟩, fun x ↦ ⟨.X (.inr x), by simp [fBC, PBC]⟩⟩
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC :
  Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))
this :
  IsEmbedding.{u, u} (X := (B ⟶ R) × (C ⟶ R)) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial ((↑B : Type u) ⊕ (↑C : Type u)) (↑A : Type u))
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim (⇑(Hom.hom (pushout.inl φ ψ)) : (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
        (⇑(Hom.hom (pushout.inr φ ψ)) : (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))))
⊢ Function.Surjective (α := (↑PBC : Type u)) (β := (↑(pushout φ ψ) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) fBC) :
      (a : (↑PBC : Type u)) → (↑(pushout φ ψ) : Type u))

Tactic:
have hfBC : Function.Surjective fBC := by
    rw [← RingHom.range_eq_top, ← top_le_iff,
      ← closure_range_union_range_eq_top_of_isPushout (.of_hasPushout _ _), Subring.closure_le]
    simp only [Set.union_subset_iff, RingHom.coe_range, Set.range_subset_iff, Set.mem_range]
    exact ⟨fun x ↦ ⟨.X (.inl x), by simp [fBC, PBC]⟩, fun x ↦ ⟨.X (.inr x), by simp [fBC, PBC]⟩⟩
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC :
  Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))
this :
  IsEmbedding.{u, u} (X := (B ⟶ R) × (C ⟶ R)) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial ((↑B : Type u) ⊕ (↑C : Type u)) (↑A : Type u))
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim (⇑(Hom.hom (pushout.inl φ ψ)) : (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
        (⇑(Hom.hom (pushout.inr φ ψ)) : (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))))
hfBC :
  Function.Surjective (α := (↑PBC : Type u)) (β := (↑(pushout φ ψ) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) fBC) :
      (a : (↑PBC : Type u)) → (↑(pushout φ ψ) : Type u))
F : (A ⟶ R) × ((↑B : Type u) ⊕ (↑C : Type u) → (↑R : Type u)) →
  ((A ⟶ R) × ((↑B : Type u) → (↑R : Type u))) × (A ⟶ R) × ((↑C : Type u) → (↑R : Type u)) :=
  fun (x : (A ⟶ R) × ((↑B : Type u) ⊕ (↑C : Type u) → (↑R : Type u))) ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
⊢ IsEmbedding F

Tactic:
have hF : IsEmbedding F := (Homeomorph.prodProdProdComm _ _ _ _).isEmbedding.comp
    ((isEmbedding_graph continuous_id).prodMap Homeomorph.sumArrowHomeomorphProdArrow.isEmbedding)
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC :
  Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))
this :
  IsEmbedding.{u, u} (X := (B ⟶ R) × (C ⟶ R)) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial ((↑B : Type u) ⊕ (↑C : Type u)) (↑A : Type u))
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim (⇑(Hom.hom (pushout.inl φ ψ)) : (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
        (⇑(Hom.hom (pushout.inr φ ψ)) : (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))))
hfBC :
  Function.Surjective (α := (↑PBC : Type u)) (β := (↑(pushout φ ψ) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) fBC) :
      (a : (↑PBC : Type u)) → (↑(pushout φ ψ) : Type u))
F : (A ⟶ R) × ((↑B : Type u) ⊕ (↑C : Type u) → (↑R : Type u)) →
  ((A ⟶ R) × ((↑B : Type u) → (↑R : Type u))) × (A ⟶ R) × ((↑C : Type u) → (↑R : Type u)) :=
  fun (x : (A ⟶ R) × ((↑B : Type u) ⊕ (↑C : Type u) → (↑R : Type u))) ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
⊢ IsEmbedding (X := ((A ⟶ R) × ((↑B : Type u) → (↑R : Type u))) × (A ⟶ R) × ((↑C : Type u) → (↑R : Type u))) (Y :=
    (of (MvPolynomial (↑B : Type u) (↑A : Type u)) ⟶ R) × (of (MvPolynomial (↑C : Type u) (↑A : Type u)) ⟶ R))
    (Prod.map
      (⇑(Homeomorph.symm (mvPolynomialHomeomorph (↑B : Type u) R A)) :
        (a : (A ⟶ R) × ((↑B : Type u) → (↑R : Type u))) → of (MvPolynomial (↑B : Type u) (↑A : Type u)) ⟶ R)
      (⇑(Homeomorph.symm (mvPolynomialHomeomorph (↑C : Type u) R A)) :
        (a : (A ⟶ R) × ((↑C : Type u) → (↑R : Type u))) → of (MvPolynomial (↑C : Type u) (↑A : Type u)) ⟶ R))

Tactic:
have H := (mvPolynomialHomeomorph B R A).symm.isEmbedding.prodMap
    (mvPolynomialHomeomorph C R A).symm.isEmbedding