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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      (some val✝) =
    (𝟭 (WidePushoutShape J')).obj (some val✝)

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
⊢ ∀ (j : J), (g ≫ π arrows j) ≫ arrows j = g ≫ base arrows

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
⊢ ∀ (i : ι'), s.π (e i) ≫ f (e i) = s.base

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
i : ι
⊢ ((WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor ⋙
          WidePullbackShape.wideCospan X (fun i ↦ Y (e i)) fun i ↦ f (e i)).obj
      (some i) =
    (WidePullbackShape.wideCospan X Y f).obj (some i)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
h : HasLimit F₁
⊢ ∀ ⦃X Y : Discrete PEmpty.{w' + 1}⦄ (f : X ⟶ Y),
    ((Functor.const (Discrete PEmpty.{w' + 1})).obj (limit F₁)).map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X fun as ↦ ⋯.elim) ≫ F₂.map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
h : HasColimit F₁
⊢ ∀ ⦃X Y : Discrete PEmpty.{w' + 1}⦄ (f : X ⟶ Y),
    F₂.map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X fun as ↦ ⋯.elim) ≫ ((Functor.const (Discrete PEmpty.{w' + 1})).obj (colimit F₁)).map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsTerminal X
F : Discrete PEmpty.{1} ⥤ C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    ((Functor.const (Discrete PEmpty.{1})).obj X).map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X_1 fun as ↦ ⋯.elim) ≫ F.map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsInitial X
F : Discrete PEmpty.{1} ⥤ C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    F.map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X_1 fun as ↦ ⋯.elim) ≫ ((Functor.const (Discrete PEmpty.{1})).obj X).map f

Tactic:
by simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X : Discrete α ⥤ C
inst✝ : HasProduct fun j ↦ X.obj { as := j }
s : Cone X
⊢ ∀ (j : Discrete α), (Pi.lift fun j ↦ s.π.app { as := j }) ≫ (Pi.cone X).π.app j = s.π.app j

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
⊢ limit.lift F (coneOfDiagramInitial I F) ≫ limit.π F j = 𝟙 (F.obj j)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ limit.lift F (coneOfDiagramTerminal I F) ≫ limit.π F j = 𝟙 (F.obj j)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramTerminal I F) = 𝟙 (F.obj j)

Tactic:
by simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X : Discrete α ⥤ C
inst✝ : HasCoproduct fun j ↦ X.obj { as := j }
s : Cocone X
⊢ ∀ (j : Discrete α), ((Sigma.cocone X).ι.app j ≫ Sigma.desc fun j ↦ s.ι.app { as := j }) = s.ι.app j

Tactic:
by simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
J : Type u_1
K : Type u_2
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasProduct f
inst✝ : HasProduct g
k : K
⊢ g (e (e.symm k)) = g k

Tactic:
by simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
J : Type u_1
K : Type u_2
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct g
k : K
⊢ g k = g (e (e.symm k))

Tactic:
by simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasProduct (g i)
inst✝ : HasProduct fun i ↦ ∏ᶜ g i
⊢ ∀ (s : Fan fun p ↦ g p.fst p.snd) (j : (i : ι) × f i),
    (Pi.lift fun b ↦ Pi.lift fun c ↦ s.proj ⟨b, c⟩) ≫
        (Fan.mk (∏ᶜ fun i ↦ ∏ᶜ g i) fun X ↦ Pi.π (fun i ↦ ∏ᶜ g i) X.fst ≫ Pi.π (g X.fst) X.snd).proj j =
      s.proj j

Tactic:
by simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasCoproduct (g i)
inst✝ : HasCoproduct fun i ↦ ∐ g i
⊢ ∀ (t : Cofan fun p ↦ g p.fst p.snd) (j : (i : ι) × f i),
    ((Cofan.mk (∐ fun i ↦ ∐ g i) fun X ↦ Sigma.ι (g X.fst) X.snd ≫ Sigma.ι (fun i ↦ ∐ g i) X.fst).inj j ≫
        Sigma.desc fun b ↦ Sigma.desc fun c ↦ t.inj ⟨b, c⟩) =
      t.inj j

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso c.fst
T✝ : C
x✝¹ : T✝ ⟶ X
x✝ : T✝ ⟶ Y
⊢ (x✝¹ ≫ inv c.fst) ≫ c.fst = x✝¹

Tactic:
by simp

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

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
⊢ colimit.ι (pair X Y) { as := left } ≫ 𝟙 (colimit (pair X Y)) = coprod.inl

Tactic:
simp only [Category.comp_id]

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

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
⊢ colimit.ι (pair X Y) { as := right } ≫ 𝟙 (colimit (pair X Y)) = coprod.inr

Tactic:
simp only [Category.comp_id]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct Y Y
f : X ⟶ Y
⊢ f ≫ diag Y = lift f f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A B X Y : C
f : A ⟶ B
g : X ⟶ Y
inst✝ : HasLimitsOfShape (Discrete WalkingPair) C
⊢ map (𝟙 X) f ≫ map g (𝟙 B) = map g (𝟙 A) ≫ map (𝟙 Y) f

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasBinaryProduct X X
inst✝ : HasBinaryProduct Y Y
⊢ diag X ≫ map f f = f ≫ diag Y

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (X ⨯ Y) (X ⨯ Y)
⊢ diag (X ⨯ Y) ≫ map fst snd = 𝟙 (X ⨯ Y)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasLimitsOfShape (Discrete WalkingPair) C
X X' Y Y' : C
g : X ⟶ Y
g' : X' ⟶ Y'
⊢ diag (X ⨯ X') ≫ map (fst ≫ g) (snd ≫ g') = map g g'

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X X
f : X ⟶ Y
⊢ codiag X ≫ f = desc f f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A B X Y : C
f : A ⟶ B
g : X ⟶ Y
inst✝ : HasColimitsOfShape (Discrete WalkingPair) C
⊢ map (𝟙 X) f ≫ map g (𝟙 B) = map g (𝟙 A) ≫ map (𝟙 Y) f

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasBinaryCoproduct X X
inst✝ : HasBinaryCoproduct Y Y
⊢ map f f ≫ codiag Y = codiag X ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)
⊢ map inl inr ≫ codiag (X ⨿ Y) = 𝟙 (X ⨿ Y)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape (Discrete WalkingPair) C
X X' Y Y' : C
g : X ⟶ Y
g' : X' ⟶ Y'
⊢ map (g ≫ inl) (g' ≫ inr) ≫ codiag (Y ⨿ Y') = map g g'

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryProducts C
W X Y Z : C
f : X ⟶ Y
g : Z ⟶ W
⊢ prod.map f g ≫ (prod.braiding Y W).hom = (prod.braiding X Z).hom ≫ prod.map g f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct (⊤_ C) P
⊢ lift (terminal.from P) (𝟙 P) ≫ snd = 𝟙 P

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct P (⊤_ C)
⊢ lift (𝟙 P) (terminal.from P) ≫ fst = 𝟙 P

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inr ≫ desc (initial.to P) (𝟙 P) = 𝟙 P

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inl ≫ desc (𝟙 P) (initial.to P) = 𝟙 P

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryCoproduct A B
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : IsIso (coprodComparison F A B)
⊢ F.map coprod.inl ≫ inv (coprodComparison F A B) = coprod.inl

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryCoproduct A B
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : IsIso (coprodComparison F A B)
⊢ F.map coprod.inr ≫ inv (coprodComparison F A B) = coprod.inr

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan X Y
hc : IsLimit c
x✝ : BinaryCofan (op X) (op Y)
⊢ (c.fst.op ≫ (hc.lift x✝.unop).op).unop = x✝.inl.unop

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan X Y
hc : IsLimit c
x✝ : BinaryCofan (op X) (op Y)
⊢ (c.snd.op ≫ (hc.lift x✝.unop).op).unop = x✝.inr.unop

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan X Y
hc : IsColimit c
x✝ : BinaryFan (op X) (op Y)
⊢ ((hc.desc x✝.unop).op ≫ c.inl.op).unop = x✝.fst.unop

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan X Y
hc : IsColimit c
x✝ : BinaryFan (op X) (op Y)
⊢ ((hc.desc x✝.unop).op ≫ c.inr.op).unop = x✝.snd.unop

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan (op X) (op Y)
hc : IsLimit c
x✝ : BinaryCofan X Y
⊢ (c.fst.unop ≫ (hc.lift x✝.op).unop).op = x✝.inl.op

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan (op X) (op Y)
hc : IsLimit c
x✝ : BinaryCofan X Y
⊢ (c.snd.unop ≫ (hc.lift x✝.op).unop).op = x✝.inr.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
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
⊢ mk f = mk ((mk f).hom ≫ T.map (𝟙 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
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : StructuredArrow S T
g : f.right ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((mk (f.hom ≫ T.map g)).hom ≫ T.map g') = mk (f.hom ≫ T.map (g ≫ g'))

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
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((mk (f ≫ T.map g)).hom ≫ T.map g') = mk ((mk f).hom ≫ T.map (g ≫ g'))

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
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
⊢ mk f = mk (f ≫ T.map (𝟙 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
S : D
Y : C
T : C ⥤ D
f : S ⟶ T.obj Y
⊢ mkPostcomp f (𝟙 Y) = eqToHom ⋯

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan (op X) (op Y)
hc : IsColimit c
x✝ : BinaryFan X Y
⊢ ((hc.desc x✝.op).unop ≫ c.inl.unop).op = x✝.fst.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
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((f ≫ T.map g) ≫ T.map g') = mk (f ≫ T.map (g ≫ g'))

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan (op X) (op Y)
hc : IsColimit c
x✝ : BinaryFan X Y
⊢ ((hc.desc x✝.op).unop ≫ c.inr.unop).op = x✝.snd.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
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A✝ B✝ : StructuredArrow 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
S✝ S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
S : C
F : B ⥤ C
G : C ⥤ D
inst✝ : G.Faithful
X✝ Y✝ : StructuredArrow S F
f : (post S F G).obj X✝ ⟶ (post S F G).obj Y✝
⊢ (post S F G).map (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
S✝ S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
S : C
F : B ⥤ C
G : C ⥤ D
inst✝ : G.Full
h : StructuredArrow (G.obj S) (F ⋙ G)
⊢ ((post S F G).obj (mk (G.preimage h.hom))).hom ≫
      (F ⋙ G).map (Iso.refl ((post S F G).obj (mk (G.preimage h.hom))).right).hom =
    h.hom

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 ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ lift ht h k w ≫ t.fst = h ∧ lift ht h k w ≫ t.snd = k

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 ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.flip.flip.fst = (Iso.refl t.flip.flip.pt).hom ≫ t.fst

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 ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.flip.flip.snd = (Iso.refl t.flip.flip.pt).hom ≫ t.snd

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 ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
⊢ ∀ (s : PullbackCone g f), ht.lift s.flip ≫ t.snd = s.fst

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 ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
⊢ ∀ (s : PullbackCone g f), ht.lift s.flip ≫ t.fst = s.snd

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ lift h k ⋯ ≫ fst f g = h ∧ lift h k ⋯ ≫ snd f g = k

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ inl f g ≫ desc h k ⋯ = h ∧ inr f g ≫ desc h k ⋯ = k

Tactic:
by simp

Goal state after:
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
⊢ ∀ (s : PushoutCocone f g), pushout.inl f g ≫ pushout.desc s.inl s.inr ⋯ = s.inl

Tactic:
by simp

Goal state after:
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
⊢ ∀ (s : PushoutCocone f g), pushout.inr f g ≫ pushout.desc s.inl s.inr ⋯ = s.inr

Tactic:
by simp

Goal state after:
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 ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
by simp

Goal state after:
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 ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ 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
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ t.inl ≫ desc ht h k w = h ∧ t.inr ≫ desc ht h k w = k

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
⊢ t.flip.flip.inl ≫ (Iso.refl t.flip.flip.pt).hom = t.inl

Tactic:
by simp

Goal state after:
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
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

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
⊢ t.flip.flip.inr ≫ (Iso.refl t.flip.flip.pt).hom = t.inr

Tactic:
by simp

Goal state after: