mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₀.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ fst (fst f g) (fst f g)) ≫ fst f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        fst (fst f g) (fst f g)) ≫
      fst f g

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ fst (fst f g) (fst f g)) ≫ snd f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        fst (fst f g) (fst f g)) ≫
      snd f g

pp: case h₁.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ snd (fst f g) (fst f g)) ≫ fst f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        snd (fst f g) (fst f g)) ≫
      fst f g

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ snd (fst f g) (fst f g)) ≫ snd f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        snd (fst f g) (fst f g)) ≫
      snd f g

Tactic:
<;>

Goal state after:
case h₀.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ fst (fst f g) (fst f g)) ≫ fst f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        fst (fst f g) (fst f g)) ≫
      fst f g

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ fst (fst f g) (fst f g)) ≫ snd f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        fst (fst f g) (fst f g)) ≫
      snd f g

case h₁.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ snd (fst f g) (fst f g)) ≫ fst f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        snd (fst f g) (fst f g)) ≫
      fst f g

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ snd (fst f g) (fst f g)) ≫ snd f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        snd (fst f g) (fst f g)) ≫
      snd f g
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
⊢ P (algebraMap R S)

Tactic:
have : (e.symm : _ →+* _).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S) := by
    ext r
    simp [e]

Goal state after:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
this : (↑e.symm).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S)
⊢ P (algebraMap R S)
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
⊢ (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj f)) ≫ fst f f =
    (i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ fst f f

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
⊢ (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj f)) ≫ snd f f =
    (i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ snd f f

Tactic:
<;>

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
⊢ (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj f)) ≫ fst f f =
    (i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ fst f f

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
⊢ (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj f)) ≫ snd f f =
    (i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ snd f f
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case w₂.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ ((e ≪≫ pullbackDiagonalMapIdIso g (𝟙 X) f ≪≫ asIso (fst g (𝟙 X))).symm.hom ≫
        snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) ≫
      fst (g ≫ f) f =
    lift (𝟙 Y) g ⋯ ≫ fst (g ≫ f) f

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ ((e ≪≫ pullbackDiagonalMapIdIso g (𝟙 X) f ≪≫ asIso (fst g (𝟙 X))).symm.hom ≫
        snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) ≫
      snd (g ≫ f) f =
    lift (𝟙 Y) g ⋯ ≫ snd (g ≫ f) f

Tactic:
<;>

Goal state after:
case w₂.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ ((e ≪≫ pullbackDiagonalMapIdIso g (𝟙 X) f ≪≫ asIso (fst g (𝟙 X))).symm.hom ≫
        snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) ≫
      fst (g ≫ f) f =
    lift (𝟙 Y) g ⋯ ≫ fst (g ≫ f) f

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ ((e ≪≫ pullbackDiagonalMapIdIso g (𝟙 X) f ≪≫ asIso (fst g (𝟙 X))).symm.hom ≫
        snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) ≫
      snd (g ≫ f) f =
    lift (𝟙 Y) g ⋯ ≫ snd (g ≫ f) f
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ (g ≫ diagonal f) ≫ fst f f = (lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ fst f f

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ (g ≫ diagonal f) ≫ snd f f = (lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ snd f f

Tactic:
<;>

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ (g ≫ diagonal f) ≫ fst f f = (lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ fst f f

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ (g ≫ diagonal f) ≫ snd f f = (lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ snd f f
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_2.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) ≫
      fst g h =
    c.fst ≫ fst g h

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) ≫
      snd g h =
    c.fst ≫ snd g h

Tactic:
<;>

Goal state after:
case refine_2.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) ≫
      fst g h =
    c.fst ≫ fst g h

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) ≫
      snd g h =
    c.fst ≫ snd g h
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_3.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h)) ≫ fst f g = c.snd ≫ fst f g

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h)) ≫ snd f g = c.snd ≫ snd f g

Tactic:
<;>

Goal state after:
case refine_3.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h)) ≫ fst f g = c.snd ≫ fst f g

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h)) ≫ snd f g = c.snd ≫ snd f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_4.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ (m ≫ snd (fst f g) (fst f h)) ≫ fst f h =
    (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ snd (fst f g) (fst f h)) ≫ fst f h

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ (m ≫ snd (fst f g) (fst f h)) ≫ snd f h =
    (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ snd (fst f g) (fst f h)) ≫ snd f h

Tactic:
<;>

Goal state after:
case refine_4.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ (m ≫ snd (fst f g) (fst f h)) ≫ fst f h =
    (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ snd (fst f g) (fst f h)) ≫ fst f h

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ (m ≫ snd (fst f g) (fst f h)) ≫ snd f h =
    (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ snd (fst f g) (fst f h)) ≫ snd f h
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hprecomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.diagonal f → P.diagonal (e.hom ≫ f)

Tactic:
introv H

Goal state after:
case hprecomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : P.diagonal f
⊢ P.diagonal (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hpostcomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.diagonal f → P.diagonal (f ≫ e.hom)

Tactic:
introv H

Goal state after:
case hpostcomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : P.diagonal f
⊢ P.diagonal (f ≫ e.hom)
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ ((codiagonal f).op ≫ (pullbackIsoOpPushout f.op f.op).inv) ≫ pullback.fst f.op f.op =
    pullback.diagonal f.op ≫ pullback.fst f.op f.op

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ ((codiagonal f).op ≫ (pullbackIsoOpPushout f.op f.op).inv) ≫ pullback.snd f.op f.op =
    pullback.diagonal f.op ≫ pullback.snd f.op f.op

Tactic:
<;>

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ ((codiagonal f).op ≫ (pullbackIsoOpPushout f.op f.op).inv) ≫ pullback.fst f.op f.op =
    pullback.diagonal f.op ≫ pullback.fst f.op f.op

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ ((codiagonal f).op ≫ (pullbackIsoOpPushout f.op f.op).inv) ≫ pullback.snd f.op f.op =
    pullback.diagonal f.op ≫ pullback.snd f.op f.op
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: case zero
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r ⋯
hc : IsColimit c
⊢ P ((parallelPair (h.r ≫ h.i) (𝟙 Y)).obj WalkingParallelPair.zero)

pp: case one
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r ⋯
hc : IsColimit c
⊢ P ((parallelPair (h.r ≫ h.i) (𝟙 Y)).obj WalkingParallelPair.one)

Tactic:
<;>

Goal state after:
case zero
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r ⋯
hc : IsColimit c
⊢ P ((parallelPair (h.r ≫ h.i) (𝟙 Y)).obj WalkingParallelPair.zero)

case one
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r ⋯
hc : IsColimit c
⊢ P ((parallelPair (h.r ≫ h.i) (𝟙 Y)).obj WalkingParallelPair.one)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ tensorHom ℬ (𝟙 X) (𝟙 Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.left } =
    𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ tensorHom ℬ (𝟙 X) (𝟙 Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.right } =
    𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ tensorHom ℬ (𝟙 X) (𝟙 Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.left } =
    𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.left }

case right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ tensorHom ℬ (𝟙 X) (𝟙 Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.right } =
    𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.left } =
    tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right } =
    tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.left } =
    tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.left }

case right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right } =
    tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
        tensorHom ℬ (𝟙 X) (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.left } =
    tensorHom ℬ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (𝟙 Y) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
        tensorHom ℬ (𝟙 X) (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.right } =
    tensorHom ℬ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (𝟙 Y) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
        tensorHom ℬ (𝟙 X) (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.left } =
    tensorHom ℬ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (𝟙 Y) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.left }

case right
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
        tensorHom ℬ (𝟙 X) (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.right } =
    tensorHom ℬ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (𝟙 Y) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ fst X Y = lift (f ≫ g) (f ≫ h) ≫ fst X Y

pp: case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ snd X Y = lift (f ≫ g) (f ≫ h) ≫ snd X Y

Tactic:
<;>

Goal state after:
case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ fst X Y = lift (f ≫ g) (f ≫ h) ≫ fst X Y

case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ snd X Y = lift (f ≫ g) (f ≫ h) ≫ snd X Y