Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this✝ : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
hfBC : Function.Surjective ⇑(ConcreteCategory.hom fBC)
F : (A ⟶ R) × (↑B ⊕ ↑C → ↑R) → ((A ⟶ R) × (↑B → ↑R)) × (A ⟶ R) × (↑C → ↑R) :=
  fun x ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H : IsEmbedding (Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm)
this : ∀ (s : ↑A), (Hom.hom (pushout.inr φ ψ)) ((Hom.hom ψ) s) = (Hom.hom (pushout.inl φ ψ)) ((Hom.hom φ) s)
⊢ ((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)) =
    ((Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm ∘ F) ∘
        ⇑(mvPolynomialHomeomorph (↑B ⊕ ↑C) R A)) ∘
      fun x ↦ fBC ≫ x

Tactic:
ext f s

Goal state after:
case fst.hC
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this✝ : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
hfBC : Function.Surjective ⇑(ConcreteCategory.hom fBC)
F : (A ⟶ R) × (↑B ⊕ ↑C → ↑R) → ((A ⟶ R) × (↑B → ↑R)) × (A ⟶ R) × (↑C → ↑R) :=
  fun x ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H : IsEmbedding (Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm)
this : ∀ (s : ↑A), (Hom.hom (pushout.inr φ ψ)) ((Hom.hom ψ) s) = (Hom.hom (pushout.inl φ ψ)) ((Hom.hom φ) s)
f : pushout φ ψ ⟶ R
s : ↑A
⊢ ((Hom.hom
            (((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))
                f).1).comp
        MvPolynomial.C)
      s =
    ((Hom.hom
            ((((Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm ∘ F) ∘
                    ⇑(mvPolynomialHomeomorph (↑B ⊕ ↑C) R A)) ∘
                  fun x ↦ fBC ≫ x)
                f).1).comp
        MvPolynomial.C)
      s

case fst.hX
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this✝ : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
hfBC : Function.Surjective ⇑(ConcreteCategory.hom fBC)
F : (A ⟶ R) × (↑B ⊕ ↑C → ↑R) → ((A ⟶ R) × (↑B → ↑R)) × (A ⟶ R) × (↑C → ↑R) :=
  fun x ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H : IsEmbedding (Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm)
this : ∀ (s : ↑A), (Hom.hom (pushout.inr φ ψ)) ((Hom.hom ψ) s) = (Hom.hom (pushout.inl φ ψ)) ((Hom.hom φ) s)
f : pushout φ ψ ⟶ R
s : ↑B
⊢ (Hom.hom (((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)) f).1)
      (MvPolynomial.X s) =
    (Hom.hom
        ((((Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm ∘ F) ∘
                ⇑(mvPolynomialHomeomorph (↑B ⊕ ↑C) R A)) ∘
              fun x ↦ fBC ≫ x)
            f).1)
      (MvPolynomial.X s)

case snd.hC
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this✝ : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
hfBC : Function.Surjective ⇑(ConcreteCategory.hom fBC)
F : (A ⟶ R) × (↑B ⊕ ↑C → ↑R) → ((A ⟶ R) × (↑B → ↑R)) × (A ⟶ R) × (↑C → ↑R) :=
  fun x ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H : IsEmbedding (Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm)
this : ∀ (s : ↑A), (Hom.hom (pushout.inr φ ψ)) ((Hom.hom ψ) s) = (Hom.hom (pushout.inl φ ψ)) ((Hom.hom φ) s)
f : pushout φ ψ ⟶ R
s : ↑A
⊢ ((Hom.hom
            (((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))
                f).2).comp
        MvPolynomial.C)
      s =
    ((Hom.hom
            ((((Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm ∘ F) ∘
                    ⇑(mvPolynomialHomeomorph (↑B ⊕ ↑C) R A)) ∘
                  fun x ↦ fBC ≫ x)
                f).2).comp
        MvPolynomial.C)
      s

case snd.hX
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this✝ : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
hfBC : Function.Surjective ⇑(ConcreteCategory.hom fBC)
F : (A ⟶ R) × (↑B ⊕ ↑C → ↑R) → ((A ⟶ R) × (↑B → ↑R)) × (A ⟶ R) × (↑C → ↑R) :=
  fun x ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H : IsEmbedding (Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm)
this : ∀ (s : ↑A), (Hom.hom (pushout.inr φ ψ)) ((Hom.hom ψ) s) = (Hom.hom (pushout.inl φ ψ)) ((Hom.hom φ) s)
f : pushout φ ψ ⟶ R
s : ↑C
⊢ (Hom.hom (((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)) f).2)
      (MvPolynomial.X s) =
    (Hom.hom
        ((((Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm ∘ F) ∘
                ⇑(mvPolynomialHomeomorph (↑B ⊕ ↑C) R A)) ∘
              fun x ↦ fBC ≫ x)
            f).2)
      (MvPolynomial.X s)