mathlib-initiative/mathlib-tactics huggingface dataset:
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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) ≫ fst f f =
    (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
        map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst f f

pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) ≫ snd f f =
    (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
        map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) ≫ fst f f =
    (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
        map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst f f

case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) ≫ snd f f =
    (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
        map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd f f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P (pullback.fst f g)

Tactic:
exact hP₂ _ _ _ f g hg

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
⊢ pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ ≫ pullback.fst f' g' =
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
        (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫
          Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))) ≫
      pullback.fst f' g'

pp: case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
⊢ pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ ≫ pullback.snd f' g' =
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
        (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫
          Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))) ≫
      pullback.snd f' g'

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
⊢ pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ ≫ pullback.fst f' g' =
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
        (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫
          Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))) ≫
      pullback.fst f' g'

case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst✝¹ : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst✝ : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
⊢ pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ ≫ pullback.snd f' g' =
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
        (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫
          Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯))) ≫
      pullback.snd f' g'
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    P f → P (e.toRingHom.comp f)

Tactic:
introv H

Goal state after:
case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
e : S ≃+* T
H : P f
⊢ P (e.toRingHom.comp f)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
    P f → P (f.comp e.toRingHom)

Tactic:
introv H

Goal state after:
case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : S →+* T
e : R ≃+* S
H : P f
⊢ P (f.comp e.toRingHom)
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_1.refine_4.h₀
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i)) ≫ fst i i =
    ((congrHom ⋯ ⋯).hom ≫
        map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
          ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯) ≫
      fst i i

pp: case h₁
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i)) ≫ snd i i =
    ((congrHom ⋯ ⋯).hom ≫
        map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
          ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯) ≫
      snd i i

Tactic:
<;>

Goal state after:
case refine_1.refine_4.h₀
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i)) ≫ fst i i =
    ((congrHom ⋯ ⋯).hom ≫
        map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
          ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯) ≫
      fst i i

case h₁
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i)) ≫ snd i i =
    ((congrHom ⋯ ⋯).hom ≫
        map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
          ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯) ≫
      snd i i
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ pushout.inl f g ≫ pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    pushout.inl f g ≫
      ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
        (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))

pp: case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ pushout.inr f g ≫ pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    pushout.inr f g ≫
      ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
        (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ pushout.inl f g ≫ pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    pushout.inl f g ≫
      ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
        (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))

case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ pushout.inr f g ≫ pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    pushout.inr f g ≫
      ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
        (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hf
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this✝ : HasPushoutsAlong (Under.mk g').hom
this :
  pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))
⊢ P ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯)))

pp: case hg
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this✝ : HasPushoutsAlong (Under.mk g').hom
this :
  pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))
⊢ P ((pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))

Tactic:
<;>

Goal state after:
case hf
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this✝ : HasPushoutsAlong (Under.mk g').hom
this :
  pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))
⊢ P ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯)))

case hg
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this✝ : HasPushoutsAlong (Under.mk g').hom
this :
  pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))
⊢ P ((pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
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 Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
⊢ diagonal (f ≫ g) ≫ fst (f ≫ g) (f ≫ g) =
    (diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ snd (diagonal g) (map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯)) ≫
      fst (f ≫ g) (f ≫ g)

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

Tactic:
<;>

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
⊢ diagonal (f ≫ g) ≫ fst (f ≫ g) (f ≫ g) =
    (diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ snd (diagonal g) (map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯)) ≫
      fst (f ≫ g) (f ≫ g)

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
⊢ diagonal (f ≫ g) ≫ snd (f ≫ g) (f ≫ g) =
    (diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ snd (diagonal g) (map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯)) ≫
      snd (f ≫ g) (f ≫ g)
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 Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ diagonal g) ≫ fst g g = (diagonal (f ≫ g) ≫ map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯) ≫ fst g g

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

Tactic:
<;>

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

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ diagonal g) ≫ snd g g = (diagonal (f ≫ g) ≫ map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯) ≫ snd g g
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 T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ ((pullbackDiagonalMapIdIso f g i).symm.hom ≫ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)) ≫
      fst (f ≫ i) (g ≫ i) =
    map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ fst (f ≫ i) (g ≫ i)

pp: case h₁
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ ((pullbackDiagonalMapIdIso f g i).symm.hom ≫ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)) ≫
      snd (f ≫ i) (g ≫ i) =
    map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ snd (f ≫ i) (g ≫ i)

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 T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ ((pullbackDiagonalMapIdIso f g i).symm.hom ≫ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)) ≫
      fst (f ≫ i) (g ≫ i) =
    map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ fst (f ≫ i) (g ≫ i)

case h₁
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ ((pullbackDiagonalMapIdIso f g i).symm.hom ≫ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)) ≫
      snd (f ≫ i) (g ≫ i) =
    map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ snd (f ≫ i) (g ≫ i)
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 T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ ((fst f g ≫ f) ≫ diagonal i) ≫ fst i i =
    (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst i i

pp: case h₁
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ ((fst f g ≫ f) ≫ diagonal i) ≫ snd i i =
    (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd i i

Tactic:
<;>

Goal state after:
case h₀
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ ((fst f g ≫ f) ≫ diagonal i) ≫ fst i i =
    (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst i i

case h₁
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ ((fst f g ≫ f) ≫ diagonal i) ≫ snd i i =
    (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd i i