Module: Mathlib.CategoryTheory.Join.Basic

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

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

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

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

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

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

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

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

Tactic:
<;>

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

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

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

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

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

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

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

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