-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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
H :
  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))
⊢ 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))
have h : Eq (α := (pushout φ ψ ⟶ R) → (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))
  (Function.comp (β := of (MvPolynomial ((↑B : Type u) ⊕ (↑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) ∘
        F) ∘
      (⇑(mvPolynomialHomeomorph ((↑B : Type u) ⊕ (↑C : Type u)) R A) :
        (a : of (MvPolynomial ((↑B : Type u) ⊕ (↑C : Type u)) (↑A : Type u)) ⟶ R) →
          (A ⟶ R) × ((↑B : Type u) ⊕ (↑C : Type u) → (↑R : Type u))))
    fun (x : pushout φ ψ ⟶ R) ↦ fBC ≫ x)
Tactic: convert!
    ((H.comp hF).comp (mvPolynomialHomeomorph _ R A).isEmbedding).comp
      (isEmbedding_precomp_of_surjective (R := R) fBC hfBC)