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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ g ≫ 𝟙 Z = 𝟙 X ≫ g

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
⊢ ∀ (s : PushoutCocone g f), t.inr ≫ ht.desc s.flip = s.inl

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
⊢ ∀ (s : PushoutCocone g f), t.inl ≫ ht.desc s.flip = s.inr

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
S : T
X Y : Over S
f : X ⟶ Y
⊢ ∃ (hg : Hom.left f ≫ Y.hom = X.hom), f = homMk (Hom.left f) ⋯

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
X✝¹ : T
f✝ g : Over X✝¹
φ : f✝ ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝ : Category.{v_1, u_1} J
D : J ⥤ T
X : T
s : D ⟶ (Functor.const J).obj X
X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ D.map f ≫ (mk (s.app Y✝)).hom = (mk (s.app X✝)).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
S : T
X Y : Under S
f : X ⟶ Y
⊢ ∃ (hg : X.hom ≫ Hom.right f = Y.hom), homMk (Hom.right f) ⋯ = f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : S.obj Y ⟶ T
⊢ mk (S.map (𝟙 Y) ≫ (mk f).hom) = mk f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : CostructuredArrow S T
g : Y' ⟶ f.left
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ f.hom) = mk (S.map g' ≫ (mk (S.map g ≫ f.hom)).hom)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
⊢ l = m

Tactic:
suffices l' = (homMk m) by apply congrArg CommaMorphism.right this

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
⊢ l' = homMk m ⋯
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ (mk f).hom) = mk (S.map g' ≫ (mk (S.map g ≫ f)).hom)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : S.obj Y ⟶ T
⊢ mk (S.map (𝟙 Y) ≫ f) = mk f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
Y : C
S : C ⥤ D
f : S.obj Y ⟶ T
⊢ mkPrecomp f (𝟙 Y) = eqToHom ⋯

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ f) = mk (S.map g' ≫ S.map g ≫ f)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A✝ B✝ : CostructuredArrow S T
f : A✝ ⟶ B✝
t : IsIso ((proj S T).map f)
⊢ f ≫ homMk (inv ((proj S T).map f)) ⋯ = 𝟙 A✝ ∧ homMk (inv ((proj S T).map f)) ⋯ ≫ f = 𝟙 B✝

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
inst✝ : G.Faithful
X✝ Y✝ : CostructuredArrow F S
f : (post F G S).obj X✝ ⟶ (post F G S).obj Y✝
⊢ (post F G S).map (homMk f.left ⋯) = f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
inst✝ : G.Full
h : CostructuredArrow (F ⋙ G) (G.obj S)
⊢ (F ⋙ G).map (Iso.refl ((post F G S).obj (mk (G.preimage h.hom))).left).hom ≫ h.hom =
    ((post F G S).obj (mk (G.preimage h.hom))).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
⊢ ∀ {Y_1 Z : StructuredArrow X (proj Y F)} (g : Y_1 ⟶ Z),
    Y_1.right.hom ≫ (Under.forget X ⋙ F).map (((proj X (proj Y F) ⋙ proj Y F).toUnder X (fun g ↦ g.hom) ⋯).map g) =
      Z.right.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
⊢ ∀ {Y_1 Z : StructuredArrow Y (Under.forget X ⋙ F)} (g : Y_1 ⟶ Z),
    Y_1.right.hom ≫
        (proj Y F).map
          (((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).toStructuredArrow Y F (fun g ↦ g.hom) ⋯).map g) =
      Z.right.hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (g ≫ inv f) ≫ f = 𝟙 Y ≫ g

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (pullbackConeOfLeftIso f g).π.app none = g

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯ ≫ pullback.snd f g = 𝟙 Y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
⊢ ∀ {X_1 Y_1 : StructuredArrow X (proj Y F)} (f : X_1 ⟶ Y_1),
    (𝟭 (StructuredArrow X (proj Y F))).map f ≫ (Iso.refl ((𝟭 (StructuredArrow X (proj Y F))).obj Y_1)).hom =
      (Iso.refl ((𝟭 (StructuredArrow X (proj Y F))).obj X_1)).hom ≫
        (ofStructuredArrowProjEquivalence.functor F Y X ⋙ ofStructuredArrowProjEquivalence.inverse F Y X).map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ 𝟙 X ≫ f = (f ≫ inv g) ≫ g

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ (pullbackConeOfRightIso f g).π.app none = f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ pullback.lift (𝟙 X) (f ≫ inv g) ⋯ ≫ pullback.fst f g = 𝟙 X

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
⊢ ∀ {X_1 Y : StructuredArrow X (Functor.diag T)} (f : X_1 ⟶ Y),
    (𝟭 (StructuredArrow X (Functor.diag T))).map f ≫ (Iso.refl ((𝟭 (StructuredArrow X (Functor.diag T))).obj Y)).hom =
      (Iso.refl ((𝟭 (StructuredArrow X (Functor.diag T))).obj X_1)).hom ≫
        (ofDiagEquivalence.functor X ⋙ ofDiagEquivalence.inverse X).map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ f ≫ inv f ≫ g = g ≫ 𝟙 Z

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
X✝ Y✝ : StructuredArrow c (Comma.fst F G)
f : X✝ ⟶ Y✝
⊢ (Under.forget c ⋙ F).map (Under.homMk (Hom.right f).left ⋯) ≫
      { left := Under.mk Y✝.hom, right := Y✝.right.right, hom := Y✝.right.hom }.hom =
    { left := Under.mk X✝.hom, right := X✝.right.right, hom := X✝.right.hom }.hom ≫ G.map (Hom.right f).right

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inr f g ≫ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ = 𝟙 Z

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
Y✝ Z✝ : Comma (Under.forget c ⋙ F) G
x✝ : Y✝ ⟶ Z✝
⊢ Y✝.left.hom ≫ (Comma.fst F G).map ((Comma.preLeft (Under.forget c) F G).map x✝) = Z✝.left.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
⊢ ∀ {Y_1 Z : CostructuredArrow (proj F Y) X} (g : Y_1 ⟶ Z),
    (Over.forget X ⋙ F).map (((proj (proj F Y) X ⋙ proj F Y).toOver X (fun g ↦ g.hom) ⋯).map g) ≫ Z.left.hom =
      Y_1.left.hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ f ≫ 𝟙 Y = g ≫ inv g ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
⊢ ∀ {Y_1 Z : CostructuredArrow (Over.forget X ⋙ F) Y} (g : Y_1 ⟶ Z),
    (proj F Y).map (((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).toCostructuredArrow F Y (fun g ↦ g.hom) ⋯).map g) ≫
        Z.left.hom =
      Y_1.left.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
⊢ ∀ {X_1 Y_1 : CostructuredArrow (proj F Y) X} (f : X_1 ⟶ Y_1),
    (𝟭 (CostructuredArrow (proj F Y) X)).map f ≫ (Iso.refl ((𝟭 (CostructuredArrow (proj F Y) X)).obj Y_1)).hom =
      (Iso.refl ((𝟭 (CostructuredArrow (proj F Y) X)).obj X_1)).hom ≫
        (ofCostructuredArrowProjEquivalence.functor F Y X ⋙ ofCostructuredArrowProjEquivalence.inverse F Y X).map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ pushout.inl f g ≫ pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ = 𝟙 Y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
⊢ ∀ {X_1 Y : CostructuredArrow (Functor.diag T) X} (f : X_1 ⟶ Y),
    (𝟭 (CostructuredArrow (Functor.diag T) X)).map f ≫
        (Iso.refl ((𝟭 (CostructuredArrow (Functor.diag T) X)).obj Y)).hom =
      (Iso.refl ((𝟭 (CostructuredArrow (Functor.diag T) X)).obj X_1)).hom ≫
        (ofDiagEquivalence.functor X ⋙ ofDiagEquivalence.inverse X).map f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
X✝ Y✝ : CostructuredArrow (Comma.fst F G) c
f : X✝ ⟶ Y✝
⊢ (Over.forget c ⋙ F).map (Over.homMk f.left.left ⋯) ≫
      { left := Over.mk Y✝.hom, right := Y✝.left.right, hom := Y✝.left.hom }.hom =
    { left := Over.mk X✝.hom, right := X✝.left.right, hom := X✝.left.hom }.hom ≫ G.map f.left.right

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
Y✝ Z✝ : Comma (Over.forget c ⋙ F) G
x✝ : Y✝ ⟶ Z✝
⊢ (Comma.fst F G).map ((Comma.preLeft (Over.forget c) F G).map x✝) ≫ Z✝.left.hom = Y✝.left.hom

Tactic:
by simp

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

Goal state before:
pp: 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
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
hf : W₁.MapFactorizationData W₂ f
⊢ (hf.p.op ≫ hf.i.op).unop = f.op.unop

Tactic:
by simp

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

Goal state before:
pp: 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
F : D ⥤ C
inst✝² : F.IsEquivalence
inst✝¹ : W₁.RespectsIso
inst✝ : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ F.map (F.preimage (h.i ≫ (F.objObjPreimageIso h.Z).inv) ≫ F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p)) = F.map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ ≫ t.fst = 𝟙 X

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
⊢ (StructuredArrow.Hom.right
        ((𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫
            (StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk y))).right) ⋯).op.hom).unop).op =
    (StructuredArrow.Hom.right
        ((StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk x))).right) ⋯).op.hom ≫
            (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map
              f).unop).op

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : MonoFactorisation f
hF : IsImage F
F' : MonoFactorisation f
⊢ (F.e ≫ hF.lift F') ≫ F'.m = F'.e ≫ F'.m

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF.lift F' ≫ hF'.lift F) ≫ F.m = 𝟙 F.I ≫ F.m

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF'.lift F ≫ hF.lift F') ≫ F'.m = 𝟙 F'.I ≫ F'.m

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF.isoExt hF').hom ≫ F'.m = F.m

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF.isoExt hF').inv ≫ F.m = F'.m

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ F.e ≫ (hF.isoExt hF').hom = F'.e

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ F'.e ≫ (hF.isoExt hF').inv = F.e

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ f ≫ 𝟙 Y = f ≫ 𝟙 Y

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inl ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ = 𝟙 Y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X : C
x : F.obj X ⟶ d
Y : C
y : F.obj Y ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)
⊢ ((𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫
            (CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk y))).left) ⋯).op.hom).unop.left.op =
    ((CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk x))).left) ⋯).op.hom ≫
            (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map
              f).unop.left.op

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
e : E
f : StructuredArrow e G
X : StructuredArrow f (pre e F G)
⊢ ((𝟭 (StructuredArrow f (pre e F G))).obj X).right.hom ≫
      (F ⋙ G).map (Iso.refl ((𝟭 (StructuredArrow f (pre e F G))).obj X).right.right).hom =
    ((preEquivalenceFunctor F f ⋙ preEquivalenceInverse F f).obj X).right.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
e : E
f : CostructuredArrow G e
X : CostructuredArrow (pre F G e) f
⊢ (F ⋙ G).map (Iso.refl ((𝟭 (CostructuredArrow (pre F G e) f)).obj X).left.left).hom ≫
      ((preEquivalence.functor F f ⋙ preEquivalence.inverse F f).obj X).left.hom =
    ((𝟭 (CostructuredArrow (pre F G e) f)).obj X).left.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow (S, S') (T.prod T')
η : X✝ ⟶ Y✝
⊢ (mk X✝.hom.1, mk X✝.hom.2).1.hom ≫ T.map (Hom.right η).1 = (mk Y✝.hom.1, mk Y✝.hom.2).1.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow (S, S') (T.prod T')
η : X✝ ⟶ Y✝
⊢ (mk X✝.hom.1, mk X✝.hom.2).2.hom ≫ T'.map (Hom.right η).2 = (mk Y✝.hom.1, mk Y✝.hom.2).2.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
η : X✝ ⟶ Y✝
⊢ (mk (X✝.1.hom, X✝.2.hom)).hom ≫ (T.prod T').map (Hom.right η.1, Hom.right η.2) = (mk (Y✝.1.hom, Y✝.2.hom)).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
⊢ ∀ {X Y : StructuredArrow (S, S') (T.prod T')} (f : X ⟶ Y),
    (𝟭 (StructuredArrow (S, S') (T.prod T'))).map f ≫ (Iso.refl ((𝟭 (StructuredArrow (S, S') (T.prod T'))).obj Y)).hom =
      (Iso.refl ((𝟭 (StructuredArrow (S, S') (T.prod T'))).obj X)).hom ≫
        (prodFunctor S S' T T' ⋙ prodInverse S S' T T').map f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow (S.prod S') (T, T')
η : X✝ ⟶ Y✝
⊢ S.map η.left.1 ≫ (mk Y✝.hom.1, mk Y✝.hom.2).1.hom = (mk X✝.hom.1, mk X✝.hom.2).1.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow (S.prod S') (T, T')
η : X✝ ⟶ Y✝
⊢ S'.map η.left.2 ≫ (mk Y✝.hom.1, mk Y✝.hom.2).2.hom = (mk X✝.hom.1, mk X✝.hom.2).2.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
η : X✝ ⟶ Y✝
⊢ (S.prod S').map (η.1.left, η.2.left) ≫ (mk (Y✝.1.hom, Y✝.2.hom)).hom = (mk (X✝.1.hom, X✝.2.hom)).hom

Tactic:
by simp

Goal state after: