Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.left.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✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case left.left.left.right
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✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case left.left.right.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✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case left.left.right.right
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✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case left.right.left.left
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✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case left.right.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✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case left.right.right.left
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✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case left.right.right.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✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case right.left.left.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✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case right.left.left.right
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✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case right.left.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✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case right.left.right.right
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✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case right.right.left.left
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✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case right.right.left.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✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case right.right.right.left
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✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

pp: case right.right.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✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
<;>

Goal state after:
case left.left.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✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.left.left.right
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✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.left.right.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✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.left.right.right
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✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.right.left.left
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✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.right.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✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.right.right.left
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✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.right.right.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✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.left.left.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✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.left.left.right
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✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.left.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✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.left.right.right
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✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.right.left.left
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✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.right.left.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✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.right.right.left
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✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.right.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✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)