-- 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_1 :
  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))
this :
  ∀ (s : (↑A : Type u)),
    Eq (α := (↑(pushout φ ψ) : Type u))
      ((Hom.hom (pushout.inr φ ψ) : (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))
          ((Hom.hom ψ : (a : (↑A : Type u)) → (↑C : Type u)) s : (↑C : Type u)) :
        (↑(pushout φ ψ) : Type u))
      ((Hom.hom (pushout.inl φ ψ) : (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
          ((Hom.hom φ : (a : (↑A : Type u)) → (↑B : Type u)) s : (↑B : Type u)) :
        (↑(pushout φ ψ) : Type u))
h :
  ∀ (f : pushout φ ψ ⟶ R) (s : (↑A : Type u)),
    Eq (α := (↑R : Type u))
      ((@RingHom.comp _ (MvPolynomial (↑B : Type u) (↑A : Type u)) _ _
              (AddMonoidAlgebra.nonAssocSemiring :
                NonAssocSemiring (AddMonoidAlgebra (↑A : Type u) ((↑B : Type u) →₀ ℕ)))
              _
              (Hom.hom
                  (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)) f).1 :
                (↑PB : Type u) →+* (↑R : Type u))
              MvPolynomial.C :
            (a : (↑A : Type u)) → (↑R : Type u))
          s :
        (↑R : Type u))
      ((@RingHom.comp _ (MvPolynomial (↑B : Type u) (↑A : Type u)) _ _
              (AddMonoidAlgebra.nonAssocSemiring :
                NonAssocSemiring (AddMonoidAlgebra (↑A : Type u) ((↑B : Type u) →₀ ℕ)))
              _
              (Hom.hom
                  (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) f).1 :
                (↑PB : Type u) →+* (↑R : Type u))
              MvPolynomial.C :
            (a : (↑A : Type u)) → (↑R : Type u))
          s :
        (↑R : Type u))
h₁ :
  ∀ (f : pushout φ ψ ⟶ R) (s : (↑B : Type u)),
    Eq (α := (↑R : Type u))
      (((Hom.hom
                (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)) f).1 :
              (↑PB : Type u) →+* (↑R : Type u)) :
            (a : MvPolynomial (↑B : Type u) (↑A : Type u)) → (↑R : Type u))
          (MvPolynomial.X s) :
        (↑R : Type u))
      (((Hom.hom
                (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) f).1 :
              (↑PB : Type u) →+* (↑R : Type u)) :
            (a : MvPolynomial (↑B : Type u) (↑A : Type u)) → (↑R : Type u))
          (MvPolynomial.X s) :
        (↑R : Type u))
h₂ :
  ∀ (f : pushout φ ψ ⟶ R) (s : (↑A : Type u)),
    Eq (α := (↑R : Type u))
      ((@RingHom.comp _ (MvPolynomial (↑C : Type u) (↑A : Type u)) _ _
              (AddMonoidAlgebra.nonAssocSemiring :
                NonAssocSemiring (AddMonoidAlgebra (↑A : Type u) ((↑C : Type u) →₀ ℕ)))
              _
              (Hom.hom
                  (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)) f).2 :
                (↑PC : Type u) →+* (↑R : Type u))
              MvPolynomial.C :
            (a : (↑A : Type u)) → (↑R : Type u))
          s :
        (↑R : Type u))
      ((@RingHom.comp _ (MvPolynomial (↑C : Type u) (↑A : Type u)) _ _
              (AddMonoidAlgebra.nonAssocSemiring :
                NonAssocSemiring (AddMonoidAlgebra (↑A : Type u) ((↑C : Type u) →₀ ℕ)))
              _
              (Hom.hom
                  (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) f).2 :
                (↑PC : Type u) →+* (↑R : Type u))
              MvPolynomial.C :
            (a : (↑A : Type u)) → (↑R : Type u))
          s :
        (↑R : Type u))
h₃ :
  ∀ (f : pushout φ ψ ⟶ R) (s : (↑C : Type u)),
    Eq (α := (↑R : Type u))
      (((Hom.hom
                (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)) f).2 :
              (↑PC : Type u) →+* (↑R : Type u)) :
            (a : MvPolynomial (↑C : Type u) (↑A : Type u)) → (↑R : Type u))
          (MvPolynomial.X s) :
        (↑R : Type u))
      (((Hom.hom
                (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) f).2 :
              (↑PC : Type u) →+* (↑R : Type u)) :
            (a : MvPolynomial (↑C : Type u) (↑A : Type u)) → (↑R : Type u))
          (MvPolynomial.X s) :
        (↑R : Type u))
⊢ 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:
ext f s