mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
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
⊢ (inclLeft A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D)) =
    (inclLeft A D).whiskerLeft
      ((mapCompLeft D F H).hom ≫
        Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv)

pp: case h₂
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
⊢ (inclRight A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D)) =
    (inclRight A D).whiskerLeft
      ((mapCompLeft D F H).hom ≫
        Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv)

Tactic:
<;>

Goal state after:
case h₁
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
⊢ (inclLeft A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D)) =
    (inclLeft A D).whiskerLeft
      ((mapCompLeft D F H).hom ≫
        Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv)

case h₂
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
⊢ (inclRight A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D)) =
    (inclRight A D).whiskerLeft
      ((mapCompLeft D F H).hom ≫
        Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv)
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
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
x✝ : A
⊢ ((inclLeft A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))).app x✝ =
    ((inclLeft A D).whiskerLeft
          ((mapCompLeft D F H).hom ≫
            Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv)).app
      x✝

pp: case h₂
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
x✝ : D
⊢ ((inclRight A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))).app x✝ =
    ((inclRight A D).whiskerLeft
          ((mapCompLeft D F H).hom ≫
            Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv)).app
      x✝

Tactic:
<;>

Goal state after:
case h₁
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
x✝ : A
⊢ ((inclLeft A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))).app x✝ =
    ((inclLeft A D).whiskerLeft
          ((mapCompLeft D F H).hom ≫
            Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv)).app
      x✝

case h₂
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
x✝ : D
⊢ ((inclRight A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))).app x✝ =
    ((inclRight A D).whiskerLeft
          ((mapCompLeft D F H).hom ≫
            Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Basic

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

pp: case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
y : C ⋆ D
a✝ : D
f : (right a✝).Hom y
⊢ comp (right a✝).id f = f

Tactic:
<;>

Goal state after:
case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
y : C ⋆ D
a✝ : C
f : (left a✝).Hom y
⊢ comp (left a✝).id f = f

case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
y : C ⋆ D
a✝ : D
f : (right a✝).Hom y
⊢ comp (right a✝).id f = f
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
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
⊢ (inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom) =
    (inclLeft A B).whiskerLeft
      ((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)

pp: case h₂
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
⊢ (inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom) =
    (inclRight A B).whiskerLeft
      ((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:
<;>

Goal state after:
case h₁
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
⊢ (inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom) =
    (inclLeft A B).whiskerLeft
      ((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)

case h₂
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
⊢ (inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom) =
    (inclRight A B).whiskerLeft
      ((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)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : C
f : (left a✝¹).Hom (left a✝)
⊢ comp (left a✝¹).id f = f

pp: case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : C
a✝ : D
f : (left a✝¹).Hom (right a✝)
⊢ comp (left a✝¹).id f = f

pp: case right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : D
a✝ : C
f : (right a✝¹).Hom (left a✝)
⊢ comp (right a✝¹).id f = f

pp: case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : D
f : (right a✝¹).Hom (right a✝)
⊢ comp (right a✝¹).id f = f

Tactic:
<;>

Goal state after:
case left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : C
f : (left a✝¹).Hom (left a✝)
⊢ comp (left a✝¹).id f = f

case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : C
a✝ : D
f : (left a✝¹).Hom (right a✝)
⊢ comp (left a✝¹).id f = f

case right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : D
a✝ : C
f : (right a✝¹).Hom (left a✝)
⊢ comp (right a✝¹).id f = f

case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : D
f : (right a✝¹).Hom (right a✝)
⊢ comp (right a✝¹).id f = f
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
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
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((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)).app
      x✝

pp: case h₂
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
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)).app x✝ =
    ((inclRight A B).whiskerLeft
          ((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)).app
      x✝

Tactic:
<;>

Goal state after:
case h₁
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
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((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)).app
      x✝

case h₂
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
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)).app x✝ =
    ((inclRight A B).whiskerLeft
          ((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)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : C
f : (left a✝¹).Hom (left a✝)
⊢ { down := f.down } = f

pp: case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : C
a✝ : D
f : (left a✝¹).Hom (right a✝)
⊢ PUnit.unit = f

pp: case right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : D
a✝ : C
f : (right a✝¹).Hom (left a✝)
⊢ (match right a✝¹, right a✝¹, left a✝, { down := 𝟙 a✝¹ }, f with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    f

pp: case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : D
f : (right a✝¹).Hom (right a✝)
⊢ { down := f.down } = f

Tactic:
<;>

Goal state after:
case left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : C
f : (left a✝¹).Hom (left a✝)
⊢ { down := f.down } = f

case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : C
a✝ : D
f : (left a✝¹).Hom (right a✝)
⊢ PUnit.unit = f

case right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : D
a✝ : C
f : (right a✝¹).Hom (left a✝)
⊢ (match right a✝¹, right a✝¹, left a✝, { down := 𝟙 a✝¹ }, f with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    f

case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : D
f : (right a✝¹).Hom (right a✝)
⊢ { down := f.down } = f
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
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
⊢ (inclLeft A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E)) =
    (inclLeft A E).whiskerLeft
      ((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)

pp: case h₂
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
⊢ (inclRight A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E)) =
    (inclRight A E).whiskerLeft
      ((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:
<;>

Goal state after:
case h₁
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
⊢ (inclLeft A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E)) =
    (inclLeft A E).whiskerLeft
      ((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)

case h₂
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
⊢ (inclRight A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E)) =
    (inclRight A E).whiskerLeft
      ((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)
Module: Mathlib.CategoryTheory.Join.Basic

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

pp: case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
y : C ⋆ D
a✝ : D
f : (right a✝).Hom y
⊢ comp f y.id = f

Tactic:
<;>

Goal state after:
case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
y : C ⋆ D
a✝ : C
f : (left a✝).Hom y
⊢ comp f y.id = f

case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
y : C ⋆ D
a✝ : D
f : (right a✝).Hom y
⊢ comp f y.id = f
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
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
x✝ : A
⊢ ((inclLeft A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E))).app x✝ =
    ((inclLeft A E).whiskerLeft
          ((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)).app
      x✝

pp: case h₂
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
x✝ : E
⊢ ((inclRight A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E))).app x✝ =
    ((inclRight A E).whiskerLeft
          ((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)).app
      x✝

Tactic:
<;>

Goal state after:
case h₁
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
x✝ : A
⊢ ((inclLeft A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E))).app x✝ =
    ((inclLeft A E).whiskerLeft
          ((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)).app
      x✝

case h₂
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
x✝ : E
⊢ ((inclRight A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E))).app x✝ =
    ((inclRight A E).whiskerLeft
          ((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)).app
      x✝
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : C
f : (left a✝¹).Hom (left a✝)
⊢ comp f (left a✝).id = f

pp: case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : C
a✝ : D
f : (left a✝¹).Hom (right a✝)
⊢ comp f (right a✝).id = f

pp: case right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : D
a✝ : C
f : (right a✝¹).Hom (left a✝)
⊢ comp f (left a✝).id = f

pp: case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : D
f : (right a✝¹).Hom (right a✝)
⊢ comp f (right a✝).id = f

Tactic:
<;>

Goal state after:
case left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : C
f : (left a✝¹).Hom (left a✝)
⊢ comp f (left a✝).id = f

case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : C
a✝ : D
f : (left a✝¹).Hom (right a✝)
⊢ comp f (right a✝).id = f

case right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : D
a✝ : C
f : (right a✝¹).Hom (left a✝)
⊢ comp f (left a✝).id = f

case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : D
f : (right a✝¹).Hom (right a✝)
⊢ comp f (right a✝).id = f
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
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
⊢ (inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom) =
    (inclLeft A B).whiskerLeft
      ((mapCompRight A (𝟭 B) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)

pp: case h₂
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
⊢ (inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom) =
    (inclRight A B).whiskerLeft
      ((mapCompRight A (𝟭 B) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)

Tactic:
<;>

Goal state after:
case h₁
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
⊢ (inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom) =
    (inclLeft A B).whiskerLeft
      ((mapCompRight A (𝟭 B) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)

case h₂
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
⊢ (inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom) =
    (inclRight A B).whiskerLeft
      ((mapCompRight A (𝟭 B) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)
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:
show 0 = colimit.ι F j 0 by simp,

Goal state after:
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 = (ConcreteCategory.hom (colimit.ι F j)) 0
⊢ ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0