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

Goal state before:
pp: case zero
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      0 =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      0

pp: case tmul
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ : ↑S
y✝ : (i : ι) → ↑(P i).right
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ ⊗ₜ[↑R] y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ ⊗ₜ[↑R] y✝)

pp: case add
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ y✝ : ↑S ⊗[↑R] ((i : ι) → ↑(P i).right)
a✝¹ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      x✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      x✝
a✝ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      y✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      y✝
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ + y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ + y✝)

Tactic:
· simp only [map_zero, Under.comp_right]

Goal state after:
case tmul
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ : ↑S
y✝ : (i : ι) → ↑(P i).right
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ ⊗ₜ[↑R] y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ ⊗ₜ[↑R] y✝)

case add
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ y✝ : ↑S ⊗[↑R] ((i : ι) → ↑(P i).right)
a✝¹ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      x✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      x✝
a✝ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      y✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      y✝
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ + y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ + y✝)