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

Goal state before:
pp: case left.id
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ (left.comp (id one)).comp h = left.comp ((id one).comp h)

pp: case right.id
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ (right.comp (id one)).comp h = right.comp ((id one).comp h)

pp: case id.left
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ ((id zero).comp left).comp h = (id zero).comp (left.comp h)

pp: case id.right
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ ((id zero).comp right).comp h = (id zero).comp (right.comp h)

pp: case id.id
X W : WalkingParallelPair
h : WalkingParallelPairHom X W
⊢ ((id X).comp (id X)).comp h = (id X).comp ((id X).comp h)

Tactic:
<;>

Goal state after:
case left.id
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ (left.comp (id one)).comp h = left.comp ((id one).comp h)

case right.id
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ (right.comp (id one)).comp h = right.comp ((id one).comp h)

case id.left
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ ((id zero).comp left).comp h = (id zero).comp (left.comp h)

case id.right
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ ((id zero).comp right).comp h = (id zero).comp (right.comp h)

case id.id
X W : WalkingParallelPair
h : WalkingParallelPairHom X W
⊢ ((id X).comp (id X)).comp h = (id X).comp ((id X).comp h)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left.id.id
⊢ (left.comp (id one)).comp (id one) = left.comp ((id one).comp (id one))

pp: case right.id.id
⊢ (right.comp (id one)).comp (id one) = right.comp ((id one).comp (id one))

pp: case id.left.id
⊢ ((id zero).comp left).comp (id one) = (id zero).comp (left.comp (id one))

pp: case id.right.id
⊢ ((id zero).comp right).comp (id one) = (id zero).comp (right.comp (id one))

pp: case id.id.left
⊢ ((id zero).comp (id zero)).comp left = (id zero).comp ((id zero).comp left)

pp: case id.id.right
⊢ ((id zero).comp (id zero)).comp right = (id zero).comp ((id zero).comp right)

pp: case id.id.id
X : WalkingParallelPair
⊢ ((id X).comp (id X)).comp (id X) = (id X).comp ((id X).comp (id X))

Tactic:
<;>

Goal state after:
case left.id.id
⊢ (left.comp (id one)).comp (id one) = left.comp ((id one).comp (id one))

case right.id.id
⊢ (right.comp (id one)).comp (id one) = right.comp ((id one).comp (id one))

case id.left.id
⊢ ((id zero).comp left).comp (id one) = (id zero).comp (left.comp (id one))

case id.right.id
⊢ ((id zero).comp right).comp (id one) = (id zero).comp (right.comp (id one))

case id.id.left
⊢ ((id zero).comp (id zero)).comp left = (id zero).comp ((id zero).comp left)

case id.id.right
⊢ ((id zero).comp (id zero)).comp right = (id zero).comp ((id zero).comp right)

case id.id.id
X : WalkingParallelPair
⊢ ((id X).comp (id X)).comp (id X) = (id X).comp ((id X).comp (id X))
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
⊢ op
      (match zero with
      | zero => one
      | one => zero) ⟶
    op
      (match one with
      | zero => one
      | one => zero)

pp: case right
⊢ op
      (match zero with
      | zero => one
      | one => zero) ⟶
    op
      (match one with
      | zero => one
      | one => zero)

pp: case id
X✝ : WalkingParallelPair
⊢ op
      (match X✝ with
      | zero => one
      | one => zero) ⟶
    op
      (match X✝ with
      | zero => one
      | one => zero)

Tactic:
<;>

Goal state after:
case left
⊢ op
      (match zero with
      | zero => one
      | one => zero) ⟶
    op
      (match one with
      | zero => one
      | one => zero)

case right
⊢ op
      (match zero with
      | zero => one
      | one => zero) ⟶
    op
      (match one with
      | zero => one
      | one => zero)

case id
X✝ : WalkingParallelPair
⊢ op
      (match X✝ with
      | zero => one
      | one => zero) ⟶
    op
      (match X✝ with
      | zero => one
      | one => zero)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₀
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ fst f₁ g₁ = map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫ fst f₁ g₁

pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ snd f₁ g₁ = map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫ snd f₁ g₁

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ fst f₁ g₁ = map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫ fst f₁ g₁

case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ snd f₁ g₁ = map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫ snd f₁ g₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₀
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inl f₂ g₂ ≫ (congrHom h₁ h₂).inv = inl f₂ g₂ ≫ map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯

pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inr f₂ g₂ ≫ (congrHom h₁ h₂).inv = inr f₂ g₂ ≫ map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inl f₂ g₂ ≫ (congrHom h₁ h₂).inv = inl f₂ g₂ ≫ map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯

case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inr f₂ g₂ ≫ (congrHom h₁ h₂).inv = inr f₂ g₂ ≫ map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ (G.map (pullback.lift h k w) ≫ pullbackComparison G f g) ≫ pullback.fst (G.map f) (G.map g) =
    pullback.lift (G.map h) (G.map k) ⋯ ≫ pullback.fst (G.map f) (G.map g)

pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ (G.map (pullback.lift h k w) ≫ pullbackComparison G f g) ≫ pullback.snd (G.map f) (G.map g) =
    pullback.lift (G.map h) (G.map k) ⋯ ≫ pullback.snd (G.map f) (G.map g)

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ (G.map (pullback.lift h k w) ≫ pullbackComparison G f g) ≫ pullback.fst (G.map f) (G.map g) =
    pullback.lift (G.map h) (G.map k) ⋯ ≫ pullback.fst (G.map f) (G.map g)

case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ (G.map (pullback.lift h k w) ≫ pullbackComparison G f g) ≫ pullback.snd (G.map f) (G.map g) =
    pullback.lift (G.map h) (G.map k) ⋯ ≫ pullback.snd (G.map f) (G.map g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map f ≫ G.map (pushout.inl f g) = G.map g ≫ G.map (pushout.inr f g)

Tactic:
simp only [← G.map_comp, pushout.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ pushout.inl (G.map f) (G.map g) ≫ pushoutComparison G f g ≫ G.map (pushout.desc h k w) =
    pushout.inl (G.map f) (G.map g) ≫ pushout.desc (G.map h) (G.map k) ⋯

pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ pushout.inr (G.map f) (G.map g) ≫ pushoutComparison G f g ≫ G.map (pushout.desc h k w) =
    pushout.inr (G.map f) (G.map g) ≫ pushout.desc (G.map h) (G.map k) ⋯

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ pushout.inl (G.map f) (G.map g) ≫ pushoutComparison G f g ≫ G.map (pushout.desc h k w) =
    pushout.inl (G.map f) (G.map g) ≫ pushout.desc (G.map h) (G.map k) ⋯

case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ pushout.inr (G.map f) (G.map g) ≫ pushoutComparison G f g ≫ G.map (pushout.desc h k w) =
    pushout.inr (G.map f) (G.map g) ≫ pushout.desc (G.map h) (G.map k) ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₁.h₁
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ ((prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd) ≫
          pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) ≫
        pullback.snd f prod.fst) ≫
      prod.fst =
    (𝟙 (pullback f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.fst

pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ ((prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd) ≫
          pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) ≫
        pullback.snd f prod.fst) ≫
      prod.snd =
    (𝟙 (pullback f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.snd

Tactic:
<;>

Goal state after:
case h₁.h₁
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ ((prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd) ≫
          pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) ≫
        pullback.snd f prod.fst) ≫
      prod.fst =
    (𝟙 (pullback f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.fst

case h₂
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ ((prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd) ≫
          pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) ≫
        pullback.snd f prod.fst) ≫
      prod.snd =
    (𝟙 (pullback f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₀.h₁
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ ((prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f) ≫
          pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) ≫
        pullback.fst prod.snd f) ≫
      prod.fst =
    (𝟙 (pullback prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.fst

pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ ((prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f) ≫
          pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) ≫
        pullback.fst prod.snd f) ≫
      prod.snd =
    (𝟙 (pullback prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.snd

Tactic:
<;>

Goal state after:
case h₀.h₁
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ ((prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f) ≫
          pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) ≫
        pullback.fst prod.snd f) ≫
      prod.fst =
    (𝟙 (pullback prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.fst

case h₂
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ ((prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f) ≫
          pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) ≫
        pullback.fst prod.snd f) ≫
      prod.snd =
    (𝟙 (pullback prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ (mk s.fst s.snd ⋯).fst = t.fst
hr' : m✝ ≫ (mk s.fst s.snd ⋯).snd = t.snd
⊢ m✝ ≫ s.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ (mk s.fst s.snd ⋯).fst = t.fst
hr' : m✝ ≫ (mk s.fst s.snd ⋯).snd = t.snd
⊢ m✝ ≫ s.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ (mk s.fst s.snd ⋯).fst = t.fst
hr' : m✝ ≫ (mk s.fst s.snd ⋯).snd = t.snd
⊢ m✝ ≫ s.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ (mk s.fst s.snd ⋯).fst = t.fst
hr' : m✝ ≫ (mk s.fst s.snd ⋯).snd = t.snd
⊢ m✝ ≫ s.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

Goal state before:
pp: case e_u
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
j : J
⊢ f.left.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).left

pp: case e_v
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
j : J
⊢ f.right.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).right

Tactic:
<;>

Goal state after:
case e_u
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
j : J
⊢ f.left.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).left

case e_v
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
j : J
⊢ f.right.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).right
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ m✝ ≫ s.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ m✝ ≫ s.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ m✝ ≫ s.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ m✝ ≫ s.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ t.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ t.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ t.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ t.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

Goal state before:
pp: case e_u
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
X✝ Y✝ Z✝ : J
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ f.left.map (x✝¹ ≫ x✝) =
    (Arrow.homMk (f.left.map x✝¹) (f.right.map x✝¹) ⋯).left ≫ (Arrow.homMk (f.left.map x✝) (f.right.map x✝) ⋯).left

pp: case e_v
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
X✝ Y✝ Z✝ : J
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ f.right.map (x✝¹ ≫ x✝) =
    (Arrow.homMk (f.left.map x✝¹) (f.right.map x✝¹) ⋯).right ≫ (Arrow.homMk (f.left.map x✝) (f.right.map x✝) ⋯).right

Tactic:
<;>

Goal state after:
case e_u
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
X✝ Y✝ Z✝ : J
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ f.left.map (x✝¹ ≫ x✝) =
    (Arrow.homMk (f.left.map x✝¹) (f.right.map x✝¹) ⋯).left ≫ (Arrow.homMk (f.left.map x✝) (f.right.map x✝) ⋯).left

case e_v
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
X✝ Y✝ Z✝ : J
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ f.right.map (x✝¹ ≫ x✝) =
    (Arrow.homMk (f.left.map x✝¹) (f.right.map x✝¹) ⋯).right ≫ (Arrow.homMk (f.left.map x✝) (f.right.map x✝) ⋯).right