-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (hypothesis)
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))
⊢ 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)
have 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))
Tactic: have (s : _) : (pushout.inr φ ψ).hom (ψ.hom s) = (pushout.inl φ ψ).hom (φ.hom s) :=
    congr($(pushout.condition (f := φ)).hom s).symm