mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
f : A ⟶ B
i : IsInitial K
t : IsTerminal Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom (t.from X) ↔ HasLiftingProperty f (t.from (L ⟹ X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
X : C
f : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j
j : J
⊢ ι F j ≫ desc f hf = f j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
X : C
f✝ : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f✝ i = (F.obj (op j)).map g ≫ f✝ j
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
⊢ (F.map φ.op).app j ≫ (f.app (op j)).app j ≫ ι G j = (F.obj (op j')).map φ ≫ (f.app (op j')).app j' ≫ ι G j'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j : J
⊢ ι F j ≫ map f = (f.app (op j)).app j ≫ ι G j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
⊢ map (𝟙 F) = 𝟙 (chosenCoend F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
G H : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
g : G ⟶ H
⊢ map f ≫ map g = map (f ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
X : C
f : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j
j : J
⊢ lift f hf ≫ π F j = f j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J✝ : Type u_1
C✝ : Type u_2
inst✝⁵ : Category.{v_1, u_2} C✝
inst✝⁴ : Category.{v_2, u_1} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ C✝
inst✝³ : ChosenCoendsOfShape J✝ C✝
X✝ : C✝
f✝¹ : (j : J✝) → (F✝.obj (op j)).obj j ⟶ X✝
hf✝ : ∀ ⦃i j : J✝⦄ (g : i ⟶ j), (F✝.map g.op).app i ≫ f✝¹ i = (F✝.obj (op j)).map g ≫ f✝¹ j
J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
⊢ (π F j ≫ (f.app (op j)).app j) ≫ (G.obj (op j)).map φ = (π F j' ≫ (f.app (op j')).app j') ≫ (G.map φ.op).app j'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j : J
⊢ map f ≫ π G j = π F j ≫ (f.app (op j)).app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
⊢ map (𝟙 F) = 𝟙 (chosenEnd F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
G H : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
g : G ⟶ H
⊢ map f ≫ map g = map (f ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
inst✝¹ : Category.{v_3, u_3} C
inst✝ : Category.{v_4, u_4} D
F : B ⥤ C
G H : C ⥤ D
η : G ⟶ H
⊢ mapWhiskerLeft (𝟭 A) (F.whiskerLeft η) =
    (mapCompRight A F G).hom ≫ (mapPair (𝟭 A) F).whiskerLeft (mapWhiskerLeft (𝟭 A) η) ≫ (mapCompRight A F H).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type w
B : C
objs : ι → C
arrows : (j : ι) → objs j ⟶ B
c : Fan objs
hc : IsLimit c
hB : IsTerminal B
s : WidePullbackCone arrows
m : s.pt ⟶ (ofFan arrows c hB).pt
x✝¹ : m ≫ (ofFan arrows c hB).base = s.base
hm : ∀ (i : ι), m ≫ (ofFan arrows c hB).π i = s.π i
x✝ : Discrete ι
i : ι
⊢ m ≫ c.π.app { as := i } = hc.lift (toFan arrows s) ≫ c.π.app { as := i }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
⊢ ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk ⋯.some)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
⊢ IsConnected (CostructuredArrow (parallelPair f g) Z)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a
Z : C
i j : X ⟶ Z
⊢ Zigzag (mk i) (mk j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
inst✝¹ : Category.{v_3, u_3} C
inst✝ : Category.{v_4, u_4} D
F : A ⥤ B
G H : B ⥤ C
η : G ⟶ H
⊢ mapWhiskerRight (F.whiskerLeft η) (𝟭 D) =
    (mapCompLeft D F G).hom ≫ (mapPair F (𝟭 D)).whiskerLeft (mapWhiskerRight η (𝟭 D)) ≫ (mapCompLeft D F H).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
inst✝¹ : Category.{v_3, u_3} C
inst✝ : Category.{v_4, u_4} D
F G : B ⥤ C
η : F ⟶ G
H : C ⥤ D
⊢ mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H) =
    (mapCompRight A F H).hom ≫
      Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ (mapCompRight A G H).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
inst✝¹ : Category.{v_3, u_3} C
inst✝ : Category.{v_4, u_4} D
F G : A ⥤ B
η : F ⟶ G
H : B ⥤ C
⊢ mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D) =
    (mapCompLeft D F H).hom ≫ Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
E : Type u_5
inst✝ : Category.{v_5, u_5} E
F : B ⥤ C
G : C ⥤ D
H : D ⥤ E
⊢ mapWhiskerLeft (𝟭 A) (F.associator G H).hom =
    (mapCompRight A (F ⋙ G) H).hom ≫
      Functor.whiskerRight (mapCompRight A F G).hom (mapPair (𝟭 A) H) ≫
        ((mapPair (𝟭 A) F).associator (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)).hom ≫
          (mapPair (𝟭 A) F).whiskerLeft (mapCompRight A G H).inv ≫ (mapCompRight A F (G ⋙ H)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
x y : C ⋆ D
f : x.Hom y
⊢ comp x.id f = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
E : Type u_5
inst✝ : Category.{v_5, u_5} E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
⊢ mapWhiskerRight (F.associator G H).hom (𝟭 E) =
    (mapCompLeft E (F ⋙ G) H).hom ≫
      Functor.whiskerRight (mapCompLeft E F G).hom (mapPair H (𝟭 E)) ≫
        ((mapPair F (𝟭 E)).associator (mapPair G (𝟭 E)) (mapPair H (𝟭 E))).hom ≫
          (mapPair F (𝟭 E)).whiskerLeft (mapCompLeft E G H).inv ≫ (mapCompLeft E F (G ⋙ H)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ mapWhiskerLeft (𝟭 A) F.leftUnitor.hom =
    (mapCompRight A (𝟭 B) F).hom ≫
      Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
j' : J
i y : j ⟶ j'
g : (ConcreteCategory.hom (F.map i)) x = (ConcreteCategory.hom (F.map y)) 0
⊢ (ConcreteCategory.hom (F.map y)) 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
x y : C ⋆ D
f : x.Hom y
⊢ comp f y.id = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
hx : (ConcreteCategory.hom (colimit.ι F j)) x = 0
⊢ ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ mapWhiskerRight F.leftUnitor.hom (𝟭 C) =
    (mapCompLeft C (𝟭 A) F).hom ≫
      Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ j ∈ {j, j', j''}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ j' ∈ {j, j', j''}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ j'' ∈ {j, j', j''}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ ⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩ ∈ {⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ mapWhiskerLeft (𝟭 A) F.rightUnitor.hom =
    (mapCompRight A F (𝟭 C)).hom ≫ (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ r • (ConcreteCategory.hom (F.map (IsFiltered.toSup {j, j', j''} {⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩} ⋯))) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ mapWhiskerRight F.rightUnitor.hom (𝟭 C) =
    (mapCompLeft C F (𝟭 B)).hom ≫ (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b c : Cat} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (f ◁ η).toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C f.toFunctor g.toFunctor)).hom ≫
        (mapPair (𝟭 C) f.toFunctor).toCatHom ◁ NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η.toNatTrans) ≫
          (Cat.Hom.isoMk (mapCompRight C f.toFunctor h.toFunctor)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b c : Cat} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (η ▷ h).toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C f.toFunctor h.toFunctor)).hom ≫
        NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η.toNatTrans) ▷ (mapPair (𝟭 C) h.toFunctor).toCatHom ≫
          (Cat.Hom.isoMk (mapCompRight C g.toFunctor h.toFunctor)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (α_ f g h).hom.toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C (f ≫ g).toFunctor h.toFunctor)).hom ≫
        (Cat.Hom.isoMk (mapCompRight C f.toFunctor g.toFunctor)).hom ▷ (mapPair (𝟭 C) h.toFunctor).toCatHom ≫
          (α_ (mapPair (𝟭 C) f.toFunctor).toCatHom (mapPair (𝟭 C) g.toFunctor).toCatHom
                (mapPair (𝟭 C) h.toFunctor).toCatHom).hom ≫
            (mapPair (𝟭 C) f.toFunctor).toCatHom ◁ (Cat.Hom.isoMk (mapCompRight C g.toFunctor h.toFunctor)).inv ≫
              (Cat.Hom.isoMk (mapCompRight C f.toFunctor (g ≫ h).toFunctor)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (λ_ f).hom.toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C (𝟙 a).toFunctor f.toFunctor)).hom ≫
        (Cat.Hom.isoMk mapPairId).hom ▷ (mapPair (𝟭 C) f.toFunctor).toCatHom ≫
          (λ_ (mapPair (𝟭 C) f.toFunctor).toCatHom).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (ρ_ f).hom.toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C f.toFunctor (𝟙 b).toFunctor)).hom ≫
        (mapPair (𝟭 C) f.toFunctor).toCatHom ◁ (Cat.Hom.isoMk mapPairId).hom ≫
          (ρ_ (mapPair (𝟭 C) f.toFunctor).toCatHom).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J) (x : j' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
x : ToType (colimit F)
hx : r • x = 0
⊢ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b c : Cat} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    NatTrans.toCatHom₂ (mapWhiskerRight (f ◁ η).toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D f.toFunctor g.toFunctor)).hom ≫
        (mapPair f.toFunctor (𝟭 D)).toCatHom ◁ NatTrans.toCatHom₂ (mapWhiskerRight η.toNatTrans (𝟭 D)) ≫
          (Cat.Hom.isoMk (mapCompLeft D f.toFunctor h.toFunctor)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b c : Cat} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    NatTrans.toCatHom₂ (mapWhiskerRight (η ▷ h).toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D f.toFunctor h.toFunctor)).hom ≫
        NatTrans.toCatHom₂ (mapWhiskerRight η.toNatTrans (𝟭 D)) ▷ (mapPair h.toFunctor (𝟭 D)).toCatHom ≫
          (Cat.Hom.isoMk (mapCompLeft D g.toFunctor h.toFunctor)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    NatTrans.toCatHom₂ (mapWhiskerRight (α_ f g h).hom.toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D (f ≫ g).toFunctor h.toFunctor)).hom ≫
        (Cat.Hom.isoMk (mapCompLeft D f.toFunctor g.toFunctor)).hom ▷ (mapPair h.toFunctor (𝟭 D)).toCatHom ≫
          (α_ (mapPair f.toFunctor (𝟭 D)).toCatHom (mapPair g.toFunctor (𝟭 D)).toCatHom
                (mapPair h.toFunctor (𝟭 D)).toCatHom).hom ≫
            (mapPair f.toFunctor (𝟭 D)).toCatHom ◁ (Cat.Hom.isoMk (mapCompLeft D g.toFunctor h.toFunctor)).inv ≫
              (Cat.Hom.isoMk (mapCompLeft D f.toFunctor (g ≫ h).toFunctor)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    NatTrans.toCatHom₂ (mapWhiskerRight (λ_ f).hom.toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D (𝟙 a).toFunctor f.toFunctor)).hom ≫
        (Cat.Hom.isoMk mapPairId).hom ▷ (mapPair f.toFunctor (𝟭 D)).toCatHom ≫
          (λ_ (mapPair f.toFunctor (𝟭 D)).toCatHom).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    NatTrans.toCatHom₂ (mapWhiskerRight (ρ_ f).hom.toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D f.toFunctor (𝟙 b).toFunctor)).hom ≫
        (mapPair f.toFunctor (𝟭 D)).toCatHom ◁ (Cat.Hom.isoMk mapPairId).hom ≫
          (ρ_ (mapPair f.toFunctor (𝟭 D)).toCatHom).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
n : ℕ
⊢ HasWidePullback (Arrow.mk ((isTerminalIncl T hT).from U)).right
    (fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).left) fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
n : SimplexCategoryᵒᵖ
i : ToType (Opposite.unop n)
⊢ (U.cechIsoCechNerveApp hT n).inv ≫ U.powerπ i = WidePullback.π (fun x ↦ (isTerminalIncl T hT).from U) i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
⊢ ∀ (j : Fin ((Opposite.unop Y✝).len + 1)),
    (U.cech.map f ≫ (U.cechIsoCechNerveApp hT Y✝).hom) ≫
        WidePullback.π (fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom) j =
      ((U.cechIsoCechNerveApp hT X✝).hom ≫ (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.map f) ≫
        WidePullback.π (fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom) j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
⊢ (𝟭 (SimplicialObject (FormalCoproduct C))).map (U.cechIsoCechNerve hT).hom ≫
      (Arrow.mk ((isTerminalIncl T hT).from U)).augmentedCechNerve.hom =
    (U.cech.augmentOfIsTerminal (isTerminalIncl T hT)).hom ≫
      (SimplicialObject.const (FormalCoproduct C)).map
        (Iso.refl (U.cech.augmentOfIsTerminal (isTerminalIncl T hT)).right).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ∀ (j : Discrete WalkingPair),
    ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).π.app
        j =
      (Iso.refl
            ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
                (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).pt).hom ≫
        (((evaluation D C).obj d).mapCone (pointwiseBinaryBicone F G).toCone).π.app j

Tactic:
by

Goal state after: