mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹, left a✝, left a✝, f, { down := 𝟙 a✝ } 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✝¹, left a✝, left a✝, f, { down := 𝟙 a✝ } 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
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A (𝟭 B) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)).app
      x✝

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

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
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A (𝟭 B) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)).app
      x✝

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
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom)).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A (𝟭 B) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)).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
b c d : C ⋆ D
g : b.Hom c
h : c.Hom d
a✝ : C
f : (left a✝).Hom b
⊢ comp (comp f g) h = comp f (comp g h)

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

Tactic:
<;>

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

case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
b c d : C ⋆ D
g : b.Hom c
h : c.Hom d
a✝ : D
f : (right a✝).Hom b
⊢ comp (comp f g) h = comp f (comp g h)
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 : A ⥤ B
⊢ (inclLeft A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C)) =
    (inclLeft A C).whiskerLeft
      ((mapCompLeft C (𝟭 A) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).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 : A ⥤ B
⊢ (inclRight A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C)) =
    (inclRight A C).whiskerLeft
      ((mapCompLeft C (𝟭 A) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).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 : A ⥤ B
⊢ (inclLeft A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C)) =
    (inclLeft A C).whiskerLeft
      ((mapCompLeft C (𝟭 A) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).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 : A ⥤ B
⊢ (inclRight A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C)) =
    (inclRight A C).whiskerLeft
      ((mapCompLeft C (𝟭 A) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)
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
c d : C ⋆ D
h : c.Hom d
a✝¹ a✝ : C
g : (left a✝).Hom c
f : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

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

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

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

Tactic:
<;>

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

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

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

case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
c d : C ⋆ D
h : c.Hom d
a✝¹ a✝ : D
g : (right a✝).Hom c
f : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
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 : A ⥤ B
x✝ : A
⊢ ((inclLeft A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C))).app x✝ =
    ((inclLeft A C).whiskerLeft
          ((mapCompLeft C (𝟭 A) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)).app
      x✝

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 : A ⥤ B
x✝ : C
⊢ ((inclRight A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C))).app x✝ =
    ((inclRight A C).whiskerLeft
          ((mapCompLeft C (𝟭 A) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)).app
      x✝

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 : A ⥤ B
x✝ : A
⊢ ((inclLeft A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C))).app x✝ =
    ((inclLeft A C).whiskerLeft
          ((mapCompLeft C (𝟭 A) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)).app
      x✝

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 : A ⥤ B
x✝ : C
⊢ ((inclRight A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C))).app x✝ =
    ((inclRight A C).whiskerLeft
          ((mapCompLeft C (𝟭 A) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)).app
      x✝
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.rightUnitor.hom) =
    (inclLeft A B).whiskerLeft
      ((mapCompRight A F (𝟭 C)).hom ≫ (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.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.rightUnitor.hom) =
    (inclRight A B).whiskerLeft
      ((mapCompRight A F (𝟭 C)).hom ≫ (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.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.rightUnitor.hom) =
    (inclLeft A B).whiskerLeft
      ((mapCompRight A F (𝟭 C)).hom ≫ (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.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.rightUnitor.hom) =
    (inclRight A B).whiskerLeft
      ((mapCompRight A F (𝟭 C)).hom ≫ (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)
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
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A F (𝟭 C)).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)).app
      x✝

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
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A F (𝟭 C)).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)).app
      x✝

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
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A F (𝟭 C)).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)).app
      x✝

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
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A F (𝟭 C)).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)).app
      x✝
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 : A ⥤ B
⊢ (inclLeft A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C)) =
    (inclLeft A C).whiskerLeft
      ((mapCompLeft C F (𝟭 B)).hom ≫ (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.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 : A ⥤ B
⊢ (inclRight A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C)) =
    (inclRight A C).whiskerLeft
      ((mapCompLeft C F (𝟭 B)).hom ≫ (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.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 : A ⥤ B
⊢ (inclLeft A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C)) =
    (inclLeft A C).whiskerLeft
      ((mapCompLeft C F (𝟭 B)).hom ≫ (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.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 : A ⥤ B
⊢ (inclRight A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C)) =
    (inclRight A C).whiskerLeft
      ((mapCompLeft C F (𝟭 B)).hom ≫ (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)
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 : A ⥤ B
x✝ : A
⊢ ((inclLeft A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C))).app x✝ =
    ((inclLeft A C).whiskerLeft
          ((mapCompLeft C F (𝟭 B)).hom ≫
            (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)).app
      x✝

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 : A ⥤ B
x✝ : C
⊢ ((inclRight A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C))).app x✝ =
    ((inclRight A C).whiskerLeft
          ((mapCompLeft C F (𝟭 B)).hom ≫
            (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)).app
      x✝

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 : A ⥤ B
x✝ : A
⊢ ((inclLeft A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C))).app x✝ =
    ((inclLeft A C).whiskerLeft
          ((mapCompLeft C F (𝟭 B)).hom ≫
            (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)).app
      x✝

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 : A ⥤ B
x✝ : C
⊢ ((inclRight A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C))).app x✝ =
    ((inclRight A C).whiskerLeft
          ((mapCompLeft C F (𝟭 B)).hom ≫
            (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)).app
      x✝
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: case left
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
⊢ ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
            (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).π.app
      { as := WalkingPair.left } =
    (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 { as := WalkingPair.left }

pp: case right
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
⊢ ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
            (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).π.app
      { as := WalkingPair.right } =
    (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 { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
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
⊢ ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
            (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).π.app
      { as := WalkingPair.left } =
    (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 { as := WalkingPair.left }

case right
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
⊢ ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
            (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).π.app
      { as := WalkingPair.right } =
    (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 { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: case left
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
⊢ ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).ι.app
        { as := WalkingPair.left } ≫
      (Iso.refl
          ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt).hom =
    (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone).ι.app { as := WalkingPair.left }

pp: case right
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
⊢ ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).ι.app
        { as := WalkingPair.right } ≫
      (Iso.refl
          ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt).hom =
    (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone).ι.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
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
⊢ ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).ι.app
        { as := WalkingPair.left } ≫
      (Iso.refl
          ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt).hom =
    (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone).ι.app { as := WalkingPair.left }

case right
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
⊢ ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).ι.app
        { as := WalkingPair.right } ≫
      (Iso.refl
          ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt).hom =
    (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone).ι.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
x✝² : Fan fun x ↦ U
x✝¹ : α
x✝ : x✝².pt.I
⊢ ({ f := fun i a ↦ (x✝².proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (x✝².proj a).φ i } ≫ (U.powerFan α).proj x✝¹).f x✝ =
    (x✝².proj x✝¹).f x✝

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
x✝¹ : Fan fun x ↦ U
x✝ : α
i✝ : x✝¹.pt.I
⊢ ({ f := fun i a ↦ (x✝¹.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (x✝¹.proj a).φ i } ≫ (U.powerFan α).proj x✝).φ i✝ ≫
      eqToHom ⋯ =
    (x✝¹.proj x✝).φ i✝

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
x✝² : Fan fun x ↦ U
x✝¹ : α
x✝ : x✝².pt.I
⊢ ({ f := fun i a ↦ (x✝².proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (x✝².proj a).φ i } ≫ (U.powerFan α).proj x✝¹).f x✝ =
    (x✝².proj x✝¹).f x✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
x✝¹ : Fan fun x ↦ U
x✝ : α
i✝ : x✝¹.pt.I
⊢ ({ f := fun i a ↦ (x✝¹.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (x✝¹.proj a).φ i } ≫ (U.powerFan α).proj x✝).φ i✝ ≫
      eqToHom ⋯ =
    (x✝¹.proj x✝).φ i✝