Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
x : ↑S
⊢ ((Hom.hom (Under.Hom.right h')).comp Algebra.TensorProduct.includeLeftRingHom) x =
    (((Hom.hom
                (Under.Hom.right
                  ((toAlgHom ((R.tensorProd S).map f)).equalizer (toAlgHom ((R.tensorProd S).map g))).val.toUnder)).comp
            (Hom.hom
              (Under.Hom.right (AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
                ofHom
                  (RingHom.id
                    ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                        (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g))))))).comp
        Algebra.TensorProduct.includeLeftRingHom)
      x

pp: case h₂
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
x : ↑(R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))).right
⊢ ((Hom.hom (Under.Hom.right h')).comp Algebra.TensorProduct.includeRight.toRingHom) x =
    (((Hom.hom
                (Under.Hom.right
                  ((toAlgHom ((R.tensorProd S).map f)).equalizer (toAlgHom ((R.tensorProd S).map g))).val.toUnder)).comp
            (Hom.hom
              (Under.Hom.right (AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
                ofHom
                  (RingHom.id
                    ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                        (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g))))))).comp
        Algebra.TensorProduct.includeRight.toRingHom)
      x

Tactic:
<;>

Goal state after:
case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
x : ↑S
⊢ ((Hom.hom (Under.Hom.right h')).comp Algebra.TensorProduct.includeLeftRingHom) x =
    (((Hom.hom
                (Under.Hom.right
                  ((toAlgHom ((R.tensorProd S).map f)).equalizer (toAlgHom ((R.tensorProd S).map g))).val.toUnder)).comp
            (Hom.hom
              (Under.Hom.right (AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
                ofHom
                  (RingHom.id
                    ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                        (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g))))))).comp
        Algebra.TensorProduct.includeLeftRingHom)
      x

case h₂
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
x : ↑(R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))).right
⊢ ((Hom.hom (Under.Hom.right h')).comp Algebra.TensorProduct.includeRight.toRingHom) x =
    (((Hom.hom
                (Under.Hom.right
                  ((toAlgHom ((R.tensorProd S).map f)).equalizer (toAlgHom ((R.tensorProd S).map g))).val.toUnder)).comp
            (Hom.hom
              (Under.Hom.right (AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
                ofHom
                  (RingHom.id
                    ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                        (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g))))))).comp
        Algebra.TensorProduct.includeRight.toRingHom)
      x