[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)
[PROOFSTEP]
rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
⊢ η.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h)
[PROOFSTEP]
rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)
[PROOFSTEP]
rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
⊢ η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h)
[PROOFSTEP]
rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]
[GOAL]
B : Type u
inst✝¹ : Bicategory B
a b c d e : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst✝ : IsIso η
⊢ inv (f ◁ η) = f ◁ inv η
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case hom_inv_id
B : Type u
inst : Bicategory B
a b c d e : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst_1 : IsIso η
⊢ f ◁ η ≫ f ◁ inv η = 𝟙 (f ≫ g)
[PROOFSTEP]
simp only [← whiskerLeft_comp, whiskerLeft_id, IsIso.hom_inv_id]
[GOAL]
B : Type u
inst✝¹ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst✝ : IsIso η
⊢ inv (η ▷ h) = inv η ▷ h
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case hom_inv_id
B : Type u
inst : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst_1 : IsIso η
⊢ η ▷ h ≫ inv η ▷ h = 𝟙 (f ≫ h)
[PROOFSTEP]
simp only [← comp_whiskerRight, id_whiskerRight, IsIso.hom_inv_id]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i) =
    inv ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom = f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv
[PROOFSTEP]
rw [← cancel_epi (f ◁ (α_ g h i).inv), ← cancel_mono (α_ (f ≫ g) h i).inv]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom) ≫ (α_ (f ≫ g) h i).inv =
    (f ◁ (α_ g h i).inv ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) ≫ (α_ (f ≫ g) h i).inv
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom) =
    inv ((α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv = (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i
[PROOFSTEP]
simp [← cancel_epi (f ◁ (α_ g h i).inv)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv) =
    inv ((α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv = (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i
[PROOFSTEP]
rw [← cancel_epi (α_ f g (h ≫ i)).inv, ← cancel_mono ((α_ f g h).inv ▷ i)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ ((α_ f g (h ≫ i)).inv ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv) ≫ (α_ f g h).inv ▷ i =
    ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) ≫ (α_ f g h).inv ▷ i
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) =
    inv ((α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom = (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom
[PROOFSTEP]
simp [← cancel_epi ((α_ f g h).hom ▷ i)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) =
    inv (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom
[PROOFSTEP]
rw [← triangle, inv_hom_id_assoc]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv
[PROOFSTEP]
simp [← cancel_mono (f ◁ (λ_ g).hom)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g
[PROOFSTEP]
simp [← cancel_mono ((ρ_ f).hom ▷ g)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ (g ≫ h) ≫ (α_ f' g h).inv = (α_ f g h).inv ≫ η ▷ g ▷ h
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h = (α_ f g h).hom ≫ η ▷ (g ≫ h) ≫ (α_ f' g h).inv
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ η ▷ h
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h ≫ (α_ f g' h).inv = (α_ f g h).inv ≫ (f ◁ η) ▷ h
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h = (α_ f g h).inv ≫ (f ◁ η) ▷ h ≫ (α_ f g' h).hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ g ◁ η
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η ≫ (α_ f g h').inv = (α_ f g h).inv ≫ (f ≫ g) ◁ η
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η = (α_ f g h).inv ≫ (f ≫ g) ◁ η ≫ (α_ f g h').hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ 𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ≫ (λ_ g).inv = (λ_ f).inv ≫ 𝟙 a ◁ η
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ≫ (ρ_ g).inv = (ρ_ f).inv ≫ η ▷ 𝟙 b
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (ρ_ f).inv ≫ η ▷ 𝟙 b ≫ (ρ_ g).hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ 𝟙 a ◁ η = 𝟙 a ◁ θ ↔ η = θ
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ η ▷ 𝟙 b = θ ▷ 𝟙 b ↔ η = θ
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom
[PROOFSTEP]
rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ← cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc,
  triangle, ← associator_naturality_middle, ← comp_whiskerRight_assoc, triangle, associator_naturality_left]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ inv ((λ_ f).inv ▷ g) = inv ((λ_ (f ≫ g)).inv ≫ (α_ (𝟙 a) f g).inv)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom
[PROOFSTEP]
rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ← cancel_epi (f ◁ (α_ _ _ _).inv),
  pentagon_inv_assoc, triangle_assoc_comp_right, ← associator_inv_naturality_middle, ← whiskerLeft_comp_assoc,
  triangle_assoc_comp_right, associator_inv_naturality_right]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ inv (f ◁ (ρ_ g).inv) = inv ((ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom)
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).hom = (α_ (𝟙 a) f g).inv ≫ (λ_ f).hom ▷ g
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).inv = (λ_ f).inv ▷ g ≫ (α_ (𝟙 a) f g).hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ (f ≫ g)).hom = (α_ f g (𝟙 c)).hom ≫ f ◁ (ρ_ g).hom
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ (f ≫ g)).inv = f ◁ (ρ_ g).inv ≫ (α_ f g (𝟙 c)).inv
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
⊢ (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom
[PROOFSTEP]
rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ← rightUnitor_comp,
  rightUnitor_naturality]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
⊢ (λ_ (𝟙 a)).inv = (ρ_ (𝟙 a)).inv
[PROOFSTEP]
simp [Iso.inv_eq_inv]


[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ f ≫ cokernel.π f = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ kernel.ι f ≫ kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0) = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ (kernel.ι f ≫ kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0)) ≫ equalizer.ι (cokernel.π f) 0 =
    0 ≫ equalizer.ι (cokernel.π f) 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ kernel.ι f ≫ f = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ cokernel.desc (kernel.ι f) f (_ : kernel.ι f ≫ f = 0) ≫ cokernel.π f = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coequalizer.π (kernel.ι f) 0 ≫ cokernel.desc (kernel.ι f) f (_ : kernel.ι f ≫ f = 0) ≫ cokernel.π f =
    coequalizer.π (kernel.ι f) 0 ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coimageImageComparison f = coimageImageComparison' f
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0 =
    (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison' f) ≫ equalizer.ι (cokernel.π f) 0
[PROOFSTEP]
simp [coimageImageComparison, coimageImageComparison']
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coimage.π f ≫ coimageImageComparison f ≫ image.ι f = f
[PROOFSTEP]
simp [coimageImageComparison]


[GOAL]
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{?u.7905, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
E : ((Functor.leftDerived ((linearYoneda R C).obj Y).rightOp (n + 1)).obj X).unop ≅ 0.unop :=
  (Iso.unop (Functor.leftDerivedObjProjectiveSucc ((linearYoneda R C).obj Y).rightOp n X)).symm
⊢ 0 ≫ 0 = 𝟙 0.unop
[PROOFSTEP]
let Z : (ModuleCat R)ᵒᵖ := 0
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{?u.7905, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
E : ((Functor.leftDerived ((linearYoneda R C).obj Y).rightOp (n + 1)).obj X).unop ≅ 0.unop :=
  (Iso.unop (Functor.leftDerivedObjProjectiveSucc ((linearYoneda R C).obj Y).rightOp n X)).symm
Z : (ModuleCat R)ᵒᵖ := 0
⊢ 0 ≫ 0 = 𝟙 0.unop
[PROOFSTEP]
rw [← (0 : 0 ⟶ Z.unop).unop_op, ← (0 : Z.unop ⟶ 0).unop_op, ← unop_id, ← unop_comp]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{?u.10674, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
E : ((Functor.leftDerived ((linearYoneda R C).obj Y).rightOp (n + 1)).obj X).unop ≅ 0.unop :=
  (Iso.unop (Functor.leftDerivedObjProjectiveSucc ((linearYoneda R C).obj Y).rightOp n X)).symm
Z : (ModuleCat R)ᵒᵖ := 0
⊢ (0.op ≫ 0.op).unop = (𝟙 0).unop
[PROOFSTEP]
aesop


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : Injective J
⊢ PreservesFiniteColimits (preadditiveYonedaObj J)
[PROOFSTEP]
letI := (injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' J).mp hP
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : Injective J
this : Functor.PreservesEpimorphisms (preadditiveYonedaObj J) :=
  Iff.mp (injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' J) hP
⊢ PreservesFiniteColimits (preadditiveYonedaObj J)
[PROOFSTEP]
apply Functor.preservesFiniteColimitsOfPreservesEpisAndKernels
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
⊢ Injective J
[PROOFSTEP]
rw [injective_iff_preservesEpimorphisms_preadditive_yoneda_obj']
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
⊢ ∃ G, Injective G ∧ IsCoseparator G
[PROOFSTEP]
haveI : WellPowered C := wellPowered_of_isDetector G hG.isDetector
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this : WellPowered C
⊢ ∃ G, Injective G ∧ IsCoseparator G
[PROOFSTEP]
haveI : HasProductsOfShape (Subobject (op G)) C := hasProductsOfShape_of_small _ _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject (op G)) C
⊢ ∃ G, Injective G ∧ IsCoseparator G
[PROOFSTEP]
let T : C := Injective.under (piObj fun P : Subobject (op G) => unop P)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
⊢ ∃ G, Injective G ∧ IsCoseparator G
[PROOFSTEP]
refine' ⟨T, inferInstance, (Preadditive.isCoseparator_iff _).2 fun X Y f hf => _⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
⊢ f = 0
[PROOFSTEP]
refine' (Preadditive.isSeparator_iff _).1 hG _ fun h => _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
⊢ h ≫ f = 0
[PROOFSTEP]
suffices hh : factorThruImage (h ≫ f) = 0
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
hh : factorThruImage (h ≫ f) = 0
⊢ h ≫ f = 0
[PROOFSTEP]
rw [← Limits.image.fac (h ≫ f), hh, zero_comp]
[GOAL]
case hh
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
⊢ factorThruImage (h ≫ f) = 0
[PROOFSTEP]
let R := Subobject.mk (factorThruImage (h ≫ f)).op
[GOAL]
case hh
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject (op G) := Subobject.mk (factorThruImage (h ≫ f)).op
⊢ factorThruImage (h ≫ f) = 0
[PROOFSTEP]
let q₁ : image (h ≫ f) ⟶ unop R := (Subobject.underlyingIso (factorThruImage (h ≫ f)).op).unop.hom
[GOAL]
case hh
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject (op G) := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ (Subobject.underlying.obj R).unop :=
  (Iso.unop (Subobject.underlyingIso (factorThruImage (h ≫ f)).op)).hom
⊢ factorThruImage (h ≫ f) = 0
[PROOFSTEP]
let q₂ : unop (R : Cᵒᵖ) ⟶ piObj fun P : Subobject (op G) => unop P :=
  section_ (Pi.π (fun P : Subobject (op G) => (unop P : C)) R)
[GOAL]
case hh
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject (op G) := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ (Subobject.underlying.obj R).unop :=
  (Iso.unop (Subobject.underlyingIso (factorThruImage (h ≫ f)).op)).hom
q₂ : (Subobject.underlying.obj R).unop ⟶ ∏ fun P => (Subobject.underlying.obj P).unop :=
  section_ (Pi.π (fun P => (Subobject.underlying.obj P).unop) R)
⊢ factorThruImage (h ≫ f) = 0
[PROOFSTEP]
let q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι _
[GOAL]
case hh
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject (op G) := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ (Subobject.underlying.obj R).unop :=
  (Iso.unop (Subobject.underlyingIso (factorThruImage (h ≫ f)).op)).hom
q₂ : (Subobject.underlying.obj R).unop ⟶ ∏ fun P => (Subobject.underlying.obj P).unop :=
  section_ (Pi.π (fun P => (Subobject.underlying.obj P).unop) R)
q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι (∏ fun P => (Subobject.underlying.obj P).unop)
⊢ factorThruImage (h ≫ f) = 0
[PROOFSTEP]
exact
  zero_of_comp_mono q
    (by
      rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc, Category.assoc, hf,
        comp_zero])
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject (op G) := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ (Subobject.underlying.obj R).unop :=
  (Iso.unop (Subobject.underlyingIso (factorThruImage (h ≫ f)).op)).hom
q₂ : (Subobject.underlying.obj R).unop ⟶ ∏ fun P => (Subobject.underlying.obj P).unop :=
  section_ (Pi.π (fun P => (Subobject.underlying.obj P).unop) R)
q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι (∏ fun P => (Subobject.underlying.obj P).unop)
⊢ factorThruImage (h ≫ f) ≫ q = 0
[PROOFSTEP]
rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc, Category.assoc, hf, comp_zero]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasColimits C
inst✝ : EnoughProjectives C
G : C
hG : IsCoseparator G
⊢ ∃ G, Projective G ∧ IsSeparator G
[PROOFSTEP]
obtain ⟨T, hT₁, hT₂⟩ := has_injective_coseparator (op G) ((isSeparator_op_iff _).2 hG)
[GOAL]
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasColimits C
inst✝ : EnoughProjectives C
G : C
hG : IsCoseparator G
T : Cᵒᵖ
hT₁ : Injective T
hT₂ : IsCoseparator T
⊢ ∃ G, Projective G ∧ IsSeparator G
[PROOFSTEP]
exact ⟨unop T, inferInstance, (isSeparator_unop_iff _).2 hT₂⟩


[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.28, u_1} C
inst✝ : Abelian C
⊢ Abelian Cᵒᵖ
[PROOFSTEP]
exact
  { normalMonoOfMono := fun f => normalMonoOfNormalEpiUnop _ (normalEpiOfEpi f.unop)
    normalEpiOfEpi := fun f => normalEpiOfNormalMonoUnop _ (normalMonoOfMono f.unop) }
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f).op ≫ f.op = 0
[PROOFSTEP]
simp [← op_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ f ≫ (kernel.ι f.op).unop = 0
[PROOFSTEP]
rw [← f.unop_op, ← unop_comp, f.unop_op]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.ι f.op ≫ f.op).unop = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0)).unop ≫
      cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0) =
    𝟙 (kernel f.op).unop
[PROOFSTEP]
rw [← unop_id, ← (cokernel.desc f _ _).unop_op, ← unop_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ ((cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0)).op ≫
        kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0)).unop =
    (𝟙 (kernel f.op)).unop
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0)).op ≫
      kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0) =
    𝟙 (kernel f.op)
[PROOFSTEP]
ext
[GOAL]
case e_f.h
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ ((cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0)).op ≫
        kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0)) ≫
      equalizer.ι f.op 0 =
    𝟙 (kernel f.op) ≫ equalizer.ι f.op 0
[PROOFSTEP]
simp [← op_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0) ≫
      (kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0)).unop =
    𝟙 (cokernel f)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ coequalizer.π f 0 ≫
      cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0) ≫
        (kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0)).unop =
    coequalizer.π f 0 ≫ 𝟙 (cokernel f)
[PROOFSTEP]
simp [← unop_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f.op).unop ≫ f = 0
[PROOFSTEP]
rw [← f.unop_op, ← unop_comp, f.unop_op]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (f.op ≫ cokernel.π f.op).unop = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ f.op ≫ (kernel.ι f).op = 0
[PROOFSTEP]
simp [← op_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0) ≫
      (cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0)).unop =
    𝟙 (cokernel f.op).unop
[PROOFSTEP]
rw [← unop_id, ← (kernel.lift f _ _).unop_op, ← unop_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0) ≫
        (kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0)).op).unop =
    (𝟙 (cokernel f.op)).unop
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0) ≫
      (kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0)).op =
    𝟙 (cokernel f.op)
[PROOFSTEP]
ext
[GOAL]
case e_f.h
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ coequalizer.π f.op 0 ≫
      cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0) ≫
        (kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0)).op =
    coequalizer.π f.op 0 ≫ 𝟙 (cokernel f.op)
[PROOFSTEP]
simp [← op_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0)).unop ≫
      kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0) =
    𝟙 (kernel f)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ ((cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0)).unop ≫
        kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0)) ≫
      equalizer.ι f 0 =
    𝟙 (kernel f) ≫ equalizer.ι f 0
[PROOFSTEP]
simp [← unop_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f.op).unop = (cokernelOpUnop f).hom ≫ kernel.ι f ≫ eqToHom (_ : X = (Opposite.op X).unop)
[PROOFSTEP]
simp [cokernelOpUnop]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.ι f.op).unop = eqToHom (_ : (Opposite.op Y).unop = Y) ≫ cokernel.π f ≫ (kernelOpUnop f).inv
[PROOFSTEP]
simp [kernelOpUnop]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.ι g.unop).op = eqToHom (_ : Opposite.op B.unop = B) ≫ cokernel.π g ≫ (kernelUnopOp g).inv
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π g.unop).op = (cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop)
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (image.ι g.unop).op ≫ (imageUnopOp g).hom = factorThruImage g
[PROOFSTEP]
simp only [imageUnopOp, Iso.trans, Iso.symm, Iso.op, cokernelOpOp_inv, cokernelEpiComp_hom, cokernelCompIsIso_hom,
  Abelian.coimageIsoImage'_hom, ← Category.assoc, ← op_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (((((kernel.lift (cokernel.π g.unop) (cokernel.π (cokernel.π g.unop).op).unop
                    (_ : (cokernel.π (cokernel.π g.unop).op).unop ≫ cokernel.π g.unop = 0) ≫
                  (Abelian.imageIsoImage g.unop).hom) ≫
                image.ι g.unop).op ≫
            (cokernelIsoOfEq
                (_ :
                  (cokernel.π g.unop).op =
                    (cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop))).hom) ≫
          cokernel.desc ((cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop))
            (cokernel.π (kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop)))
            (_ :
              ((cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop)) ≫
                  cokernel.π (kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop)) =
                0)) ≫
        cokernel.desc (kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop))
          (inv (eqToHom (_ : A = Opposite.op A.unop)) ≫ cokernel.π (kernel.ι g))
          (_ :
            (kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop)) ≫
                inv (eqToHom (_ : A = Opposite.op A.unop)) ≫ cokernel.π (kernel.ι g) =
              0)) ≫
      cokernel.desc (kernel.ι g) (factorThruImage g) (_ : kernel.ι g ≫ factorThruImage g = 0) =
    factorThruImage g
[PROOFSTEP]
simp only [Category.assoc, Abelian.imageIsoImage_hom_comp_image_ι, kernel.lift_ι, Quiver.Hom.op_unop,
  cokernelIsoOfEq_hom_comp_desc_assoc, cokernel.π_desc_assoc, cokernel.π_desc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (eqToHom (_ : A = Opposite.op A.unop)) ≫ factorThruImage g = factorThruImage g
[PROOFSTEP]
simp only [eqToHom_refl]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (𝟙 A) ≫ factorThruImage g = factorThruImage g
[PROOFSTEP]
erw [IsIso.inv_id, Category.id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (imageUnopOp g).hom ≫ image.ι g = (factorThruImage g.unop).op
[PROOFSTEP]
simp only [← cancel_epi (image.ι g.unop).op, ← Category.assoc, image_ι_op_comp_imageUnopOp_hom, ← op_comp, image.fac,
  Quiver.Hom.op_unop]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ factorThruImage g ≫ (imageUnopOp g).inv = (image.ι g.unop).op
[PROOFSTEP]
rw [Iso.comp_inv_eq, image_ι_op_comp_imageUnopOp_hom]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (imageUnopOp g).inv ≫ (factorThruImage g.unop).op = image.ι g
[PROOFSTEP]
rw [Iso.inv_comp_eq, imageUnopOp_hom_comp_image_ι]


[GOAL]
B : Type u
⊢ [inst : Inhabited B] → Inhabited (FreeBicategory B)
[PROOFSTEP]
intro h
[GOAL]
B : Type u
h : Inhabited B
⊢ Inhabited (FreeBicategory B)
[PROOFSTEP]
exact id h
[GOAL]
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : X ⟶ Y), 𝟙 X ≫ f = f
[PROOFSTEP]
rintro f g ⟨η⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
f✝ : f ⟶ g
η : Hom₂ f g
⊢ 𝟙 f ≫ Quot.mk Rel η = Quot.mk Rel η
[PROOFSTEP]
exact Quot.sound (Rel.id_comp η)
[GOAL]
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : X ⟶ Y), f ≫ 𝟙 Y = f
[PROOFSTEP]
rintro f g ⟨η⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
f✝ : f ⟶ g
η : Hom₂ f g
⊢ Quot.mk Rel η ≫ 𝟙 g = Quot.mk Rel η
[PROOFSTEP]
exact Quot.sound (Rel.comp_id η)
[GOAL]
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {W X Y Z : a ⟶ b} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
rintro f g h i ⟨η⟩ ⟨θ⟩ ⟨ι⟩
[GOAL]
case mk.mk.mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g h i : a ⟶ b
f✝ : f ⟶ g
η : Hom₂ f g
g✝ : g ⟶ h
θ : Hom₂ g h
h✝ : h ⟶ i
ι : Hom₂ h i
⊢ (Quot.mk Rel η ≫ Quot.mk Rel θ) ≫ Quot.mk Rel ι = Quot.mk Rel η ≫ Quot.mk Rel θ ≫ Quot.mk Rel ι
[PROOFSTEP]
exact Quot.sound (Rel.assoc η θ ι)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c : FreeBicategory B} (f : a ⟶ b) {g h i : b ⟶ c} (η : g ⟶ h) (θ : h ⟶ i),
    (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c f g i (η ≫ θ) =
      (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b c f g h η ≫
        (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b c f h i θ
[PROOFSTEP]
rintro a b c f g h i ⟨η⟩ ⟨θ⟩
[GOAL]
case mk.mk
B : Type u
inst✝ : Quiver B
a b c : FreeBicategory B
f : a ⟶ b
g h i : b ⟶ c
η✝ : g ⟶ h
η : Hom₂ g h
θ✝ : h ⟶ i
θ : Hom₂ h i
⊢ (fun a b c f g h η =>
        Quot.map (Hom₂.whisker_left f)
          (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
      a b c f g i (Quot.mk Rel η ≫ Quot.mk Rel θ) =
    (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c f g h (Quot.mk Rel η) ≫
      (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c f h i (Quot.mk Rel θ)
[PROOFSTEP]
exact Quot.sound (Rel.whisker_left_comp f η θ)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g),
    (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a a b (𝟙 a) f g η =
      ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.left_unitor f)) (Quot.mk Rel (Hom₂.left_unitor_inv f))) a b f).hom ≫
        η ≫ ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.left_unitor f)) (Quot.mk Rel (Hom₂.left_unitor_inv f))) a b g).inv
[PROOFSTEP]
rintro a b f g ⟨η⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η✝ : f ⟶ g
η : Hom₂ f g
⊢ (fun a b c f g h η =>
        Quot.map (Hom₂.whisker_left f)
          (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
      a a b (𝟙 a) f g (Quot.mk Rel η) =
    ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.left_unitor f)) (Quot.mk Rel (Hom₂.left_unitor_inv f))) a b f).hom ≫
      Quot.mk Rel η ≫
        ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.left_unitor f)) (Quot.mk Rel (Hom₂.left_unitor_inv f))) a b g).inv
[PROOFSTEP]
exact Quot.sound (Rel.id_whisker_left η)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
    (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a c d (f ≫ g) h h' η =
      ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b
            c d f g h).hom ≫
        (fun a b c f g h η =>
              Quot.map (Hom₂.whisker_left f)
                (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
            a b d f (g ≫ h) (g ≫ h')
            ((fun a b c f g h η =>
                Quot.map (Hom₂.whisker_left f)
                  (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
              b c d g h h' η) ≫
          ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h)))
              a b c d f g h').inv
[PROOFSTEP]
rintro a b c d f g h h' ⟨η⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b c d : FreeBicategory B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η✝ : h ⟶ h'
η : Hom₂ h h'
⊢ (fun a b c f g h η =>
        Quot.map (Hom₂.whisker_left f)
          (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
      a c d (f ≫ g) h h' (Quot.mk Rel η) =
    ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b c
          d f g h).hom ≫
      (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b d f (g ≫ h) (g ≫ h')
          ((fun a b c f g h η =>
              Quot.map (Hom₂.whisker_left f)
                (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
            b c d g h h' (Quot.mk Rel η)) ≫
        ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a
            b c d f g h').inv
[PROOFSTEP]
exact Quot.sound (Rel.comp_whisker_left f g η)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c : FreeBicategory B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c),
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b c f h (η ≫ θ) i =
      (fun a b c f g η h =>
            Quot.map (Hom₂.whisker_right h)
              (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
          a b c f g η i ≫
        (fun a b c f g η h =>
            Quot.map (Hom₂.whisker_right h)
              (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
          a b c g h θ i
[PROOFSTEP]
rintro a b c f g h ⟨η⟩ ⟨θ⟩ i
[GOAL]
case mk.mk
B : Type u
inst✝ : Quiver B
a b c : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
η : Hom₂ f g
θ✝ : g ⟶ h
θ : Hom₂ g h
i : b ⟶ c
⊢ (fun a b c f g η h =>
        Quot.map (Hom₂.whisker_right h)
          (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
      a b c f h (Quot.mk Rel η ≫ Quot.mk Rel θ) i =
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b c f g (Quot.mk Rel η) i ≫
      (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b c g h (Quot.mk Rel θ) i
[PROOFSTEP]
exact Quot.sound (Rel.comp_whisker_right i η θ)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g),
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b b f g η (𝟙 b) =
      ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.right_unitor f)) (Quot.mk Rel (Hom₂.right_unitor_inv f))) a b f).hom ≫
        η ≫
          ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.right_unitor f)) (Quot.mk Rel (Hom₂.right_unitor_inv f))) a b g).inv
[PROOFSTEP]
rintro a b f g ⟨η⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η✝ : f ⟶ g
η : Hom₂ f g
⊢ (fun a b c f g η h =>
        Quot.map (Hom₂.whisker_right h)
          (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
      a b b f g (Quot.mk Rel η) (𝟙 b) =
    ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.right_unitor f)) (Quot.mk Rel (Hom₂.right_unitor_inv f))) a b f).hom ≫
      Quot.mk Rel η ≫
        ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.right_unitor f)) (Quot.mk Rel (Hom₂.right_unitor_inv f))) a b g).inv
[PROOFSTEP]
exact Quot.sound (Rel.whisker_right_id η)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b d f f' η (g ≫ h) =
      ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b
            c d f g h).inv ≫
        (fun a b c f g η h =>
              Quot.map (Hom₂.whisker_right h)
                (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
            a c d (f ≫ g) (f' ≫ g)
            ((fun a b c f g η h =>
                Quot.map (Hom₂.whisker_right h)
                  (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
              a b c f f' η g)
            h ≫
          ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h)))
              a b c d f' g h).hom
[PROOFSTEP]
rintro a b c d f f' ⟨η⟩ g h
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b c d : FreeBicategory B
f f' : a ⟶ b
η✝ : f ⟶ f'
η : Hom₂ f f'
g : b ⟶ c
h : c ⟶ d
⊢ (fun a b c f g η h =>
        Quot.map (Hom₂.whisker_right h)
          (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
      a b d f f' (Quot.mk Rel η) (g ≫ h) =
    ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b c
          d f g h).inv ≫
      (fun a b c f g η h =>
            Quot.map (Hom₂.whisker_right h)
              (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
          a c d (f ≫ g) (f' ≫ g)
          ((fun a b c f g η h =>
              Quot.map (Hom₂.whisker_right h)
                (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
            a b c f f' (Quot.mk Rel η) g)
          h ≫
        ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a
            b c d f' g h).hom
[PROOFSTEP]
exact Quot.sound (Rel.whisker_right_comp g h η)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a c d (f ≫ g) (f ≫ g')
        ((fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b c f g g' η)
        h =
      ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b
            c d f g h).hom ≫
        (fun a b c f g h η =>
              Quot.map (Hom₂.whisker_left f)
                (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
            a b d f (g ≫ h) (g' ≫ h)
            ((fun a b c f g η h =>
                Quot.map (Hom₂.whisker_right h)
                  (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
              b c d g g' η h) ≫
          ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h)))
              a b c d f g' h).inv
[PROOFSTEP]
rintro a b c d f g g' ⟨η⟩ h
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b c d : FreeBicategory B
f : a ⟶ b
g g' : b ⟶ c
η✝ : g ⟶ g'
η : Hom₂ g g'
h : c ⟶ d
⊢ (fun a b c f g η h =>
        Quot.map (Hom₂.whisker_right h)
          (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
      a c d (f ≫ g) (f ≫ g')
      ((fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c f g g' (Quot.mk Rel η))
      h =
    ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b c
          d f g h).hom ≫
      (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b d f (g ≫ h) (g' ≫ h)
          ((fun a b c f g η h =>
              Quot.map (Hom₂.whisker_right h)
                (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
            b c d g g' (Quot.mk Rel η) h) ≫
        ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a
            b c d f g' h).inv
[PROOFSTEP]
exact Quot.sound (Rel.whisker_assoc f η h)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c : FreeBicategory B} {f g : a ⟶ b} {h i : b ⟶ c} (η : f ⟶ g) (θ : h ⟶ i),
    (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b c f h i θ ≫
        (fun a b c f g η h =>
            Quot.map (Hom₂.whisker_right h)
              (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
          a b c f g η i =
      (fun a b c f g η h =>
            Quot.map (Hom₂.whisker_right h)
              (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
          a b c f g η h ≫
        (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b c g h i θ
[PROOFSTEP]
rintro a b c f g h i ⟨η⟩ ⟨θ⟩
[GOAL]
case mk.mk
B : Type u
inst✝ : Quiver B
a b c : FreeBicategory B
f g : a ⟶ b
h i : b ⟶ c
η✝ : f ⟶ g
η : Hom₂ f g
θ✝ : h ⟶ i
θ : Hom₂ h i
⊢ (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c f h i (Quot.mk Rel θ) ≫
      (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b c f g (Quot.mk Rel η) i =
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b c f g (Quot.mk Rel η) h ≫
      (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c g h i (Quot.mk Rel θ)
[PROOFSTEP]
exact Quot.sound (Rel.whisker_exchange η θ)
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
H : Rel η θ
⊢ liftHom₂ F η = liftHom₂ F θ
[PROOFSTEP]
induction H
[GOAL]
case vcomp_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ : B
f✝ g✝ h✝ : Hom a✝¹ b✝
η✝ : Hom₂ f✝ g✝
θ₁✝ θ₂✝ : Hom₂ g✝ h✝
a✝ : Rel θ₁✝ θ₂✝
a_ih✝ : liftHom₂ F θ₁✝ = liftHom₂ F θ₂✝
⊢ liftHom₂ F (Hom₂.vcomp η✝ θ₁✝) = liftHom₂ F (Hom₂.vcomp η✝ θ₂✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case vcomp_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ : B
f✝ g✝ h✝ : Hom a✝¹ b✝
η✝ : Hom₂ f✝ g✝
θ₁✝ θ₂✝ : Hom₂ g✝ h✝
a✝ : Rel θ₁✝ θ₂✝
a_ih✝ : liftHom₂ F θ₁✝ = liftHom₂ F θ₂✝
⊢ liftHom₂ F η✝ ≫ liftHom₂ F θ₁✝ = liftHom₂ F η✝ ≫ liftHom₂ F θ₂✝
[PROOFSTEP]
aesop_cat
[GOAL]
case vcomp_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ : B
f✝ g✝ h✝ : Hom a✝¹ b✝
η₁✝ η₂✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
a✝ : Rel η₁✝ η₂✝
a_ih✝ : liftHom₂ F η₁✝ = liftHom₂ F η₂✝
⊢ liftHom₂ F (Hom₂.vcomp η₁✝ θ✝) = liftHom₂ F (Hom₂.vcomp η₂✝ θ✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case vcomp_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ : B
f✝ g✝ h✝ : Hom a✝¹ b✝
η₁✝ η₂✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
a✝ : Rel η₁✝ η₂✝
a_ih✝ : liftHom₂ F η₁✝ = liftHom₂ F η₂✝
⊢ liftHom₂ F η₁✝ ≫ liftHom₂ F θ✝ = liftHom₂ F η₂✝ ≫ liftHom₂ F θ✝
[PROOFSTEP]
aesop_cat
[GOAL]
case id_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.id f✝) η✝) = liftHom₂ F η✝
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case id_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ 𝟙 (liftHom F f✝) ≫ liftHom₂ F η✝ = liftHom₂ F η✝
[PROOFSTEP]
aesop_cat
[GOAL]
case comp_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F (Hom₂.vcomp η✝ (Hom₂.id g✝)) = liftHom₂ F η✝
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case comp_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F η✝ ≫ 𝟙 (liftHom F g✝) = liftHom₂ F η✝
[PROOFSTEP]
aesop_cat
[GOAL]
case assoc
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ h✝ i✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
ι✝ : Hom₂ h✝ i✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.vcomp η✝ θ✝) ι✝) = liftHom₂ F (Hom₂.vcomp η✝ (Hom₂.vcomp θ✝ ι✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case assoc
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ h✝ i✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
ι✝ : Hom₂ h✝ i✝
⊢ (liftHom₂ F η✝ ≫ liftHom₂ F θ✝) ≫ liftHom₂ F ι✝ = liftHom₂ F η✝ ≫ liftHom₂ F θ✝ ≫ liftHom₂ F ι✝
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ c✝ : B
f✝ : Hom a✝¹ b✝
g✝ h✝ : Hom b✝ c✝
η✝ η'✝ : Hom₂ g✝ h✝
a✝ : Rel η✝ η'✝
a_ih✝ : liftHom₂ F η✝ = liftHom₂ F η'✝
⊢ liftHom₂ F (Hom₂.whisker_left f✝ η✝) = liftHom₂ F (Hom₂.whisker_left f✝ η'✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ c✝ : B
f✝ : Hom a✝¹ b✝
g✝ h✝ : Hom b✝ c✝
η✝ η'✝ : Hom₂ g✝ h✝
a✝ : Rel η✝ η'✝
a_ih✝ : liftHom₂ F η✝ = liftHom₂ F η'✝
⊢ liftHom F f✝ ◁ liftHom₂ F η✝ = liftHom F f✝ ◁ liftHom₂ F η'✝
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_left_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom₂ F (Hom₂.whisker_left f✝ (Hom₂.id g✝)) = liftHom₂ F (Hom₂.id (Hom.comp f✝ g✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_left_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom F f✝ ◁ 𝟙 (liftHom F g✝) = 𝟙 (liftHom F f✝ ≫ liftHom F g✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_left_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ h✝ i✝ : Hom b✝ c✝
η✝ : Hom₂ g✝ h✝
θ✝ : Hom₂ h✝ i✝
⊢ liftHom₂ F (Hom₂.whisker_left f✝ (Hom₂.vcomp η✝ θ✝)) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.whisker_left f✝ η✝) (Hom₂.whisker_left f✝ θ✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_left_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ h✝ i✝ : Hom b✝ c✝
η✝ : Hom₂ g✝ h✝
θ✝ : Hom₂ h✝ i✝
⊢ liftHom F f✝ ◁ (liftHom₂ F η✝ ≫ liftHom₂ F θ✝) = liftHom F f✝ ◁ liftHom₂ F η✝ ≫ liftHom F f✝ ◁ liftHom₂ F θ✝
[PROOFSTEP]
aesop_cat
[GOAL]
case id_whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F (Hom₂.whisker_left (Hom.id a✝) η✝) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.left_unitor f✝) (Hom₂.vcomp η✝ (Hom₂.left_unitor_inv g✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case id_whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ 𝟙 (F.obj a✝) ◁ liftHom₂ F η✝ = (λ_ (liftHom F f✝)).hom ≫ liftHom₂ F η✝ ≫ (λ_ (liftHom F g✝)).inv
[PROOFSTEP]
aesop_cat
[GOAL]
case comp_whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ h'✝ : Hom c✝ d✝
η✝ : Hom₂ h✝ h'✝
⊢ liftHom₂ F (Hom₂.whisker_left (Hom.comp f✝ g✝) η✝) =
    liftHom₂ F
      (Hom₂.vcomp (Hom₂.associator f✝ g✝ h✝)
        (Hom₂.vcomp (Hom₂.whisker_left f✝ (Hom₂.whisker_left g✝ η✝)) (Hom₂.associator_inv f✝ g✝ h'✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case comp_whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ h'✝ : Hom c✝ d✝
η✝ : Hom₂ h✝ h'✝
⊢ (liftHom F f✝ ≫ liftHom F g✝) ◁ liftHom₂ F η✝ =
    (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ≫
      liftHom F f✝ ◁ liftHom F g✝ ◁ liftHom₂ F η✝ ≫ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h'✝)).inv
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ c✝ : B
f✝ g✝ : Hom a✝¹ b✝
h✝ : Hom b✝ c✝
η✝ η'✝ : Hom₂ f✝ g✝
a✝ : Rel η✝ η'✝
a_ih✝ : liftHom₂ F η✝ = liftHom₂ F η'✝
⊢ liftHom₂ F (Hom₂.whisker_right h✝ η✝) = liftHom₂ F (Hom₂.whisker_right h✝ η'✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ c✝ : B
f✝ g✝ : Hom a✝¹ b✝
h✝ : Hom b✝ c✝
η✝ η'✝ : Hom₂ f✝ g✝
a✝ : Rel η✝ η'✝
a_ih✝ : liftHom₂ F η✝ = liftHom₂ F η'✝
⊢ liftHom₂ F η✝ ▷ liftHom F h✝ = liftHom₂ F η'✝ ▷ liftHom F h✝
[PROOFSTEP]
aesop_cat
[GOAL]
case id_whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom₂ F (Hom₂.whisker_right g✝ (Hom₂.id f✝)) = liftHom₂ F (Hom₂.id (Hom.comp f✝ g✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case id_whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ 𝟙 (liftHom F f✝) ▷ liftHom F g✝ = 𝟙 (liftHom F f✝ ≫ liftHom F g✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case comp_whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ h✝ : Hom a✝ b✝
i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
⊢ liftHom₂ F (Hom₂.whisker_right i✝ (Hom₂.vcomp η✝ θ✝)) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.whisker_right i✝ η✝) (Hom₂.whisker_right i✝ θ✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case comp_whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ h✝ : Hom a✝ b✝
i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
⊢ (liftHom₂ F η✝ ≫ liftHom₂ F θ✝) ▷ liftHom F i✝ = liftHom₂ F η✝ ▷ liftHom F i✝ ≫ liftHom₂ F θ✝ ▷ liftHom F i✝
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_right_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F (Hom₂.whisker_right (Hom.id b✝) η✝) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.right_unitor f✝) (Hom₂.vcomp η✝ (Hom₂.right_unitor_inv g✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_right_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F η✝ ▷ 𝟙 (F.obj b✝) = (ρ_ (liftHom F f✝)).hom ≫ liftHom₂ F η✝ ≫ (ρ_ (liftHom F g✝)).inv
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_right_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ f'✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
η✝ : Hom₂ f✝ f'✝
⊢ liftHom₂ F (Hom₂.whisker_right (Hom.comp g✝ h✝) η✝) =
    liftHom₂ F
      (Hom₂.vcomp (Hom₂.associator_inv f✝ g✝ h✝)
        (Hom₂.vcomp (Hom₂.whisker_right h✝ (Hom₂.whisker_right g✝ η✝)) (Hom₂.associator f'✝ g✝ h✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_right_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ f'✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
η✝ : Hom₂ f✝ f'✝
⊢ liftHom₂ F η✝ ▷ (liftHom F g✝ ≫ liftHom F h✝) =
    (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).inv ≫
      liftHom₂ F η✝ ▷ liftHom F g✝ ▷ liftHom F h✝ ≫ (α_ (liftHom F f'✝) (liftHom F g✝) (liftHom F h✝)).hom
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_assoc
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ g'✝ : Hom b✝ c✝
η✝ : Hom₂ g✝ g'✝
h✝ : Hom c✝ d✝
⊢ liftHom₂ F (Hom₂.whisker_right h✝ (Hom₂.whisker_left f✝ η✝)) =
    liftHom₂ F
      (Hom₂.vcomp (Hom₂.associator f✝ g✝ h✝)
        (Hom₂.vcomp (Hom₂.whisker_left f✝ (Hom₂.whisker_right h✝ η✝)) (Hom₂.associator_inv f✝ g'✝ h✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_assoc
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ g'✝ : Hom b✝ c✝
η✝ : Hom₂ g✝ g'✝
h✝ : Hom c✝ d✝
⊢ (liftHom F f✝ ◁ liftHom₂ F η✝) ▷ liftHom F h✝ =
    (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ≫
      liftHom F f✝ ◁ liftHom₂ F η✝ ▷ liftHom F h✝ ≫ (α_ (liftHom F f✝) (liftHom F g'✝) (liftHom F h✝)).inv
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_exchange
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ : Hom a✝ b✝
h✝ i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ h✝ i✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.whisker_left f✝ θ✝) (Hom₂.whisker_right i✝ η✝)) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.whisker_right h✝ η✝) (Hom₂.whisker_left g✝ θ✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_exchange
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ : Hom a✝ b✝
h✝ i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ h✝ i✝
⊢ liftHom F f✝ ◁ liftHom₂ F θ✝ ≫ liftHom₂ F η✝ ▷ liftHom F i✝ =
    liftHom₂ F η✝ ▷ liftHom F h✝ ≫ liftHom F g✝ ◁ liftHom₂ F θ✝
[PROOFSTEP]
aesop_cat
[GOAL]
case associator_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.associator f✝ g✝ h✝) (Hom₂.associator_inv f✝ g✝ h✝)) =
    liftHom₂ F (Hom₂.id (Hom.comp (Hom.comp f✝ g✝) h✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case associator_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ≫ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).inv =
    𝟙 ((liftHom F f✝ ≫ liftHom F g✝) ≫ liftHom F h✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case associator_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.associator_inv f✝ g✝ h✝) (Hom₂.associator f✝ g✝ h✝)) =
    liftHom₂ F (Hom₂.id (Hom.comp f✝ (Hom.comp g✝ h✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case associator_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).inv ≫ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom =
    𝟙 (liftHom F f✝ ≫ liftHom F g✝ ≫ liftHom F h✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case left_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.left_unitor f✝) (Hom₂.left_unitor_inv f✝)) =
    liftHom₂ F (Hom₂.id (Hom.comp (Hom.id a✝) f✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case left_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (λ_ (liftHom F f✝)).hom ≫ (λ_ (liftHom F f✝)).inv = 𝟙 (𝟙 (F.obj a✝) ≫ liftHom F f✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case left_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.left_unitor_inv f✝) (Hom₂.left_unitor f✝)) = liftHom₂ F (Hom₂.id f✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case left_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (λ_ (liftHom F f✝)).inv ≫ (λ_ (liftHom F f✝)).hom = 𝟙 (liftHom F f✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case right_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.right_unitor f✝) (Hom₂.right_unitor_inv f✝)) =
    liftHom₂ F (Hom₂.id (Hom.comp f✝ (Hom.id b✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case right_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (ρ_ (liftHom F f✝)).hom ≫ (ρ_ (liftHom F f✝)).inv = 𝟙 (liftHom F f✝ ≫ 𝟙 (F.obj b✝))
[PROOFSTEP]
aesop_cat
[GOAL]
case right_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.right_unitor_inv f✝) (Hom₂.right_unitor f✝)) = liftHom₂ F (Hom₂.id f✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case right_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (ρ_ (liftHom F f✝)).inv ≫ (ρ_ (liftHom F f✝)).hom = 𝟙 (liftHom F f✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case pentagon
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ e✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
i✝ : Hom d✝ e✝
⊢ liftHom₂ F
      (Hom₂.vcomp (Hom₂.whisker_right i✝ (Hom₂.associator f✝ g✝ h✝))
        (Hom₂.vcomp (Hom₂.associator f✝ (Hom.comp g✝ h✝) i✝) (Hom₂.whisker_left f✝ (Hom₂.associator g✝ h✝ i✝)))) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.associator (Hom.comp f✝ g✝) h✝ i✝) (Hom₂.associator f✝ g✝ (Hom.comp h✝ i✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case pentagon
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ e✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
i✝ : Hom d✝ e✝
⊢ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ▷ liftHom F i✝ ≫
      (α_ (liftHom F f✝) (liftHom F g✝ ≫ liftHom F h✝) (liftHom F i✝)).hom ≫
        liftHom F f✝ ◁ (α_ (liftHom F g✝) (liftHom F h✝) (liftHom F i✝)).hom =
    (α_ (liftHom F f✝ ≫ liftHom F g✝) (liftHom F h✝) (liftHom F i✝)).hom ≫
      (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝ ≫ liftHom F i✝)).hom
[PROOFSTEP]
aesop_cat
[GOAL]
case triangle
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.associator f✝ (Hom.id b✝) g✝) (Hom₂.whisker_left f✝ (Hom₂.left_unitor g✝))) =
    liftHom₂ F (Hom₂.whisker_right g✝ (Hom₂.right_unitor f✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case triangle
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ (α_ (liftHom F f✝) (𝟙 (F.obj b✝)) (liftHom F g✝)).hom ≫ liftHom F f✝ ◁ (λ_ (liftHom F g✝)).hom =
    (ρ_ (liftHom F f✝)).hom ▷ liftHom F g✝
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b : FreeBicategory B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (η ≫ θ) =
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          η ≫
        PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          θ
[PROOFSTEP]
intros a b f g h η θ
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (η ≫ θ) =
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        η ≫
      PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        θ
[PROOFSTEP]
apply Quot.rec _ _ η
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ ∀ (a_1 : Hom₂ f g),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (Quot.mk Rel a_1 ≫ θ) =
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel a_1) ≫
        PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          θ
[PROOFSTEP]
intro η
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
θ : g ⟶ h
η : Hom₂ f g
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (Quot.mk Rel η ≫ θ) =
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (Quot.mk Rel η) ≫
      PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        θ
[PROOFSTEP]
apply Quot.rec _ _ θ
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
θ : g ⟶ h
η : Hom₂ f g
⊢ ∀ (a_1 : Hom₂ g h),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (Quot.mk Rel η ≫ Quot.mk Rel a_1) =
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel η) ≫
        PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel a_1)
[PROOFSTEP]
intro θ
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
θ✝ : g ⟶ h
η : Hom₂ f g
θ : Hom₂ g h
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (Quot.mk Rel η ≫ Quot.mk Rel θ) =
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (Quot.mk Rel η) ≫
      PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (Quot.mk Rel θ)
[PROOFSTEP]
rfl
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
θ : g ⟶ h
η : Hom₂ f g
⊢ ∀ (a_1 b_1 : Hom₂ g h) (p : Rel a_1 b_1),
    (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel η ≫ Quot.mk Rel b_1) =
          PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              (Quot.mk Rel η) ≫
            PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              (Quot.mk Rel b_1)) =
      (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel η ≫ Quot.mk Rel b_1) =
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel η ≫ Quot.mk Rel b_1))
[PROOFSTEP]
intros
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
θ : g ⟶ h
η : Hom₂ f g
a✝ b✝ : Hom₂ g h
p✝ : Rel a✝ b✝
⊢ (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel η ≫ Quot.mk Rel b✝) =
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel η) ≫
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel b✝)) =
    (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel η ≫ Quot.mk Rel b✝) =
        PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel η ≫ Quot.mk Rel b✝))
[PROOFSTEP]
rfl
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ ∀ (a_1 b_1 : Hom₂ f g) (p : Rel a_1 b_1),
    (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel b_1 ≫ θ) =
          PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              (Quot.mk Rel b_1) ≫
            PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              θ) =
      (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel b_1 ≫ θ) =
          PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              (Quot.mk Rel b_1) ≫
            PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              θ)
[PROOFSTEP]
intros
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
a✝ b✝ : Hom₂ f g
p✝ : Rel a✝ b✝
⊢ (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel b✝ ≫ θ) =
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel b✝) ≫
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            θ) =
    (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel b✝ ≫ θ) =
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel b✝) ≫
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            θ)
[PROOFSTEP]
rfl
  -- Porting note: still borked from here. The infoview doesn't update properly for me.
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b c : FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (f ◁ η) =
      ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            f g).hom ≫
        (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                    map₂ := fun {a b} {f g} =>
                      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
              f ◁
            PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              η ≫
          ((fun {a b c} f g =>
                Iso.refl
                  ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                          map₂ := fun {a b} {f g} =>
                            Quot.lift (liftHom₂ F)
                              (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                    (f ≫ g)))
              f h).inv
[PROOFSTEP]
intro a b c f g h η
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (f ◁ η) =
    ((fun {a b c} f g =>
            Iso.refl
              ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                      map₂ := fun {a b} {f g} =>
                        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                (f ≫ g)))
          f g).hom ≫
      (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                  map₂ := fun {a b} {f g} =>
                    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
            f ◁
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            η ≫
        ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            f h).inv
[PROOFSTEP]
apply Quot.rec _ _ η
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ ∀ (a_1 : Hom₂ g h),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (f ◁ Quot.mk Rel a_1) =
      ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            f g).hom ≫
        (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                    map₂ := fun {a b} {f g} =>
                      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
              f ◁
            PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              (Quot.mk Rel a_1) ≫
          ((fun {a b c} f g =>
                Iso.refl
                  ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                          map₂ := fun {a b} {f g} =>
                            Quot.lift (liftHom₂ F)
                              (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                    (f ≫ g)))
              f h).inv
[PROOFSTEP]
intros
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
a✝ : Hom₂ g h
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (f ◁ Quot.mk Rel a✝) =
    ((fun {a b c} f g =>
            Iso.refl
              ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                      map₂ := fun {a b} {f g} =>
                        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                (f ≫ g)))
          f g).hom ≫
      (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                  map₂ := fun {a b} {f g} =>
                    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
            f ◁
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel a✝) ≫
        ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            f h).inv
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ ∀ (a_1 b_1 : Hom₂ g h) (p : Rel a_1 b_1),
    (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (f ◁ Quot.mk Rel b_1) =
          ((fun {a b c} f g =>
                  Iso.refl
                    ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                            map₂ := fun {a b} {f g} =>
                              Quot.lift (liftHom₂ F)
                                (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                      (f ≫ g)))
                f g).hom ≫
            (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  f ◁
                PrelaxFunctor.map₂
                  { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                    map₂ := fun {a b} {f g} =>
                      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
                  (Quot.mk Rel b_1) ≫
              ((fun {a b c} f g =>
                    Iso.refl
                      ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                              map₂ := fun {a b} {f g} =>
                                Quot.lift (liftHom₂ F)
                                  (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                        (f ≫ g)))
                  f h).inv) =
      (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (f ◁ Quot.mk Rel b_1) =
          ((fun {a b c} f g =>
                  Iso.refl
                    ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                            map₂ := fun {a b} {f g} =>
                              Quot.lift (liftHom₂ F)
                                (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                      (f ≫ g)))
                f g).hom ≫
            (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  f ◁
                PrelaxFunctor.map₂
                  { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                    map₂ := fun {a b} {f g} =>
                      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
                  (Quot.mk Rel b_1) ≫
              ((fun {a b c} f g =>
                    Iso.refl
                      ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                              map₂ := fun {a b} {f g} =>
                                Quot.lift (liftHom₂ F)
                                  (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                        (f ≫ g)))
                  f h).inv)
[PROOFSTEP]
intros
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
a✝ b✝ : Hom₂ g h
p✝ : Rel a✝ b✝
⊢ (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (f ◁ Quot.mk Rel b✝) =
        ((fun {a b c} f g =>
                Iso.refl
                  ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                          map₂ := fun {a b} {f g} =>
                            Quot.lift (liftHom₂ F)
                              (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                    (f ≫ g)))
              f g).hom ≫
          (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                      map₂ := fun {a b} {f g} =>
                        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                f ◁
              PrelaxFunctor.map₂
                { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                  map₂ := fun {a b} {f g} =>
                    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
                (Quot.mk Rel b✝) ≫
            ((fun {a b c} f g =>
                  Iso.refl
                    ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                            map₂ := fun {a b} {f g} =>
                              Quot.lift (liftHom₂ F)
                                (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                      (f ≫ g)))
                f h).inv) =
    (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (f ◁ Quot.mk Rel b✝) =
        ((fun {a b c} f g =>
                Iso.refl
                  ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                          map₂ := fun {a b} {f g} =>
                            Quot.lift (liftHom₂ F)
                              (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                    (f ≫ g)))
              f g).hom ≫
          (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                      map₂ := fun {a b} {f g} =>
                        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                f ◁
              PrelaxFunctor.map₂
                { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                  map₂ := fun {a b} {f g} =>
                    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
                (Quot.mk Rel b✝) ≫
            ((fun {a b c} f g =>
                  Iso.refl
                    ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                            map₂ := fun {a b} {f g} =>
                              Quot.lift (liftHom₂ F)
                                (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                      (f ≫ g)))
                f h).inv)
[PROOFSTEP]
rfl
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b c : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (η ▷ h) =
      ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            f h).hom ≫
        PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              η ▷
            (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                    map₂ := fun {a b} {f g} =>
                      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
              h ≫
          ((fun {a b c} f g =>
                Iso.refl
                  ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                          map₂ := fun {a b} {f g} =>
                            Quot.lift (liftHom₂ F)
                              (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                    (f ≫ g)))
              g h).inv
[PROOFSTEP]
intro _ _ _ _ _ η h
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (η ▷ h) =
    ((fun {a b c} f g =>
            Iso.refl
              ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                      map₂ := fun {a b} {f g} =>
                        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                (f ≫ g)))
          f✝ h).hom ≫
      PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            η ▷
          (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                  map₂ := fun {a b} {f g} =>
                    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
            h ≫
        ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            g✝ h).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ (f✝ ≫ h) (g✝ ≫ h)), Rel η θ → liftHom₂ F η = liftHom₂ F θ) (η ▷ h) =
    𝟙 (liftHom F f✝ ≫ liftHom F h) ≫
      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f✝ g✝), Rel η θ → liftHom₂ F η = liftHom₂ F θ) η ▷ liftHom F h ≫
        𝟙 (liftHom F g✝ ≫ liftHom F h)
[PROOFSTEP]
apply Quot.rec _ _ η
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ ∀ (a : Hom₂ f✝ g✝),
    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ (f✝ ≫ h) (g✝ ≫ h)), Rel η θ → liftHom₂ F η = liftHom₂ F θ)
        (Quot.mk Rel a ▷ h) =
      𝟙 (liftHom F f✝ ≫ liftHom F h) ≫
        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f✝ g✝), Rel η θ → liftHom₂ F η = liftHom₂ F θ) (Quot.mk Rel a) ▷
            liftHom F h ≫
          𝟙 (liftHom F g✝ ≫ liftHom F h)
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ ∀ (a b : Hom₂ f✝ g✝) (p : Rel a b),
    (_ :
        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ (f✝ ≫ h) (g✝ ≫ h)), Rel η θ → liftHom₂ F η = liftHom₂ F θ)
            (Quot.mk Rel b ▷ h) =
          𝟙 (liftHom F f✝ ≫ liftHom F h) ≫
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f✝ g✝), Rel η θ → liftHom₂ F η = liftHom₂ F θ) (Quot.mk Rel b) ▷
                liftHom F h ≫
              𝟙 (liftHom F g✝ ≫ liftHom F h)) =
      (_ :
        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ (f✝ ≫ h) (g✝ ≫ h)), Rel η θ → liftHom₂ F η = liftHom₂ F θ)
            (Quot.mk Rel b ▷ h) =
          𝟙 (liftHom F f✝ ≫ liftHom F h) ≫
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f✝ g✝), Rel η θ → liftHom₂ F η = liftHom₂ F θ) (Quot.mk Rel b) ▷
                liftHom F h ≫
              𝟙 (liftHom F g✝ ≫ liftHom F h))
[PROOFSTEP]
aesop_cat