-- 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))))
⊢ 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))
have simp : (∀ (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: simp only [Set.union_subset_iff, RingHom.coe_range, Set.range_subset_iff, Set.mem_range]