[GOAL]
B : Type u
inst✝ : Quiver B
a b : B
f g : Discrete (Path a b)
η : f ⟶ g
⊢ PrelaxFunctor.map₂ (preinclusion B) η = eqToHom (_ : (↑(preinclusion B)).map f = (↑(preinclusion B)).map g)
[PROOFSTEP]
rcases η with ⟨⟨⟩⟩
[GOAL]
case up.up
B : Type u
inst✝ : Quiver B
a b : B
f g : Discrete (Path a b)
down✝ : f.as = g.as
⊢ PrelaxFunctor.map₂ (preinclusion B) { down := { down := down✝ } } =
    eqToHom (_ : (↑(preinclusion B)).map f = (↑(preinclusion B)).map g)
[PROOFSTEP]
cases Discrete.ext _ _ (by assumption)
[GOAL]
B : Type u
inst✝ : Quiver B
a b : B
f g : Discrete (Path a b)
down✝ : f.as = g.as
⊢ ?m.4748.as = ?m.4749.as
[PROOFSTEP]
assumption
[GOAL]
case up.up.refl
B : Type u
inst✝ : Quiver B
a b : B
f : Discrete (Path a b)
down✝ : f.as = f.as
⊢ PrelaxFunctor.map₂ (preinclusion B) { down := { down := down✝ } } =
    eqToHom (_ : (↑(preinclusion B)).map f = (↑(preinclusion B)).map f)
[PROOFSTEP]
convert (inclusionPath a b).map_id _
[GOAL]
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
⊢ normalizeAux p f = normalizeAux p g
[PROOFSTEP]
rcases η with ⟨η'⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
η' : Hom₂ f g
⊢ normalizeAux p f = normalizeAux p g
[PROOFSTEP]
apply @congr_fun _ _ fun p => normalizeAux p f
[GOAL]
case mk.h
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
η' : Hom₂ f g
⊢ (fun p => normalizeAux p f) = fun p => normalizeAux p g
[PROOFSTEP]
clear p η
[GOAL]
case mk.h
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
η' : Hom₂ f g
⊢ (fun p => normalizeAux p f) = fun p => normalizeAux p g
[PROOFSTEP]
induction η' with
| vcomp _ _ _ _ => apply Eq.trans <;> assumption
| whisker_left _ _ ih => funext; apply congr_fun ih
| whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
| _ => funext; rfl
[GOAL]
case mk.h
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
η' : Hom₂ f g
⊢ (fun p => normalizeAux p f) = fun p => normalizeAux p g
[PROOFSTEP]
induction η' with
| vcomp _ _ _ _ => apply Eq.trans <;> assumption
| whisker_left _ _ ih => funext; apply congr_fun ih
| whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
| _ => funext; rfl
[GOAL]
case mk.h.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p => normalizeAux p f✝) = fun p => normalizeAux p g✝
θ_ih✝ : (fun p => normalizeAux p g✝) = fun p => normalizeAux p h✝
⊢ (fun p => normalizeAux p f✝) = fun p => normalizeAux p h✝
[PROOFSTEP]

| vcomp _ _ _ _ => apply Eq.trans <;> assumption
[GOAL]
case mk.h.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p => normalizeAux p f✝) = fun p => normalizeAux p g✝
θ_ih✝ : (fun p => normalizeAux p g✝) = fun p => normalizeAux p h✝
⊢ (fun p => normalizeAux p f✝) = fun p => normalizeAux p h✝
[PROOFSTEP]
apply Eq.trans
[GOAL]
case mk.h.vcomp.h₁
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p => normalizeAux p f✝) = fun p => normalizeAux p g✝
θ_ih✝ : (fun p => normalizeAux p g✝) = fun p => normalizeAux p h✝
⊢ (fun p => normalizeAux p f✝) = ?mk.h.vcomp.b
[PROOFSTEP]
assumption
[GOAL]
case mk.h.vcomp.h₂
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
η_ih✝ : (fun p => normalizeAux p f✝) = fun p => normalizeAux p g✝
θ_ih✝ : (fun p => normalizeAux p g✝) = fun p => normalizeAux p h✝
⊢ (fun p => normalizeAux p g✝) = fun p => normalizeAux p h✝
[PROOFSTEP]
assumption
[GOAL]
case mk.h.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih : (fun p => normalizeAux p g✝) = fun p => normalizeAux p h✝
⊢ (fun p => normalizeAux p (f✝ ≫ g✝)) = fun p => normalizeAux p (f✝ ≫ h✝)
[PROOFSTEP]

| whisker_left _ _ ih => funext; apply congr_fun ih
[GOAL]
case mk.h.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih : (fun p => normalizeAux p g✝) = fun p => normalizeAux p h✝
⊢ (fun p => normalizeAux p (f✝ ≫ g✝)) = fun p => normalizeAux p (f✝ ≫ h✝)
[PROOFSTEP]
funext
[GOAL]
case mk.h.whisker_left.h
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih : (fun p => normalizeAux p g✝) = fun p => normalizeAux p h✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (f✝ ≫ g✝) = normalizeAux x✝ (f✝ ≫ h✝)
[PROOFSTEP]
apply congr_fun ih
[GOAL]
case mk.h.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h✝ : b✝ ⟶ c✝
η✝ : Hom₂ f✝ g✝
ih : (fun p => normalizeAux p f✝) = fun p => normalizeAux p g✝
⊢ (fun p => normalizeAux p (Hom.comp f✝ h✝)) = fun p => normalizeAux p (Hom.comp g✝ h✝)
[PROOFSTEP]

| whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
[GOAL]
case mk.h.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h✝ : b✝ ⟶ c✝
η✝ : Hom₂ f✝ g✝
ih : (fun p => normalizeAux p f✝) = fun p => normalizeAux p g✝
⊢ (fun p => normalizeAux p (Hom.comp f✝ h✝)) = fun p => normalizeAux p (Hom.comp g✝ h✝)
[PROOFSTEP]
funext
[GOAL]
case mk.h.whisker_right.h
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h✝ : b✝ ⟶ c✝
η✝ : Hom₂ f✝ g✝
ih : (fun p => normalizeAux p f✝) = fun p => normalizeAux p g✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (Hom.comp f✝ h✝) = normalizeAux x✝ (Hom.comp g✝ h✝)
[PROOFSTEP]
apply congr_arg₂ _ (congr_fun ih _) rfl
[GOAL]
case mk.h.id
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p => normalizeAux p f✝) = fun p => normalizeAux p f✝
[PROOFSTEP]

| _ => funext; rfl
[GOAL]
case mk.h.id
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p => normalizeAux p f✝) = fun p => normalizeAux p f✝
[PROOFSTEP]
funext
[GOAL]
case mk.h.id.h
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
x✝ : Path a a✝
⊢ normalizeAux x✝ f✝ = normalizeAux x✝ f✝
[PROOFSTEP]
rfl
[GOAL]
case mk.h.associator
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (fun p => normalizeAux p ((f✝ ≫ g✝) ≫ h✝)) = fun p => normalizeAux p (f✝ ≫ g✝ ≫ h✝)
[PROOFSTEP]

| _ => funext; rfl
[GOAL]
case mk.h.associator
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (fun p => normalizeAux p ((f✝ ≫ g✝) ≫ h✝)) = fun p => normalizeAux p (f✝ ≫ g✝ ≫ h✝)
[PROOFSTEP]
funext
[GOAL]
case mk.h.associator.h
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
x✝ : Path a a✝
⊢ normalizeAux x✝ ((f✝ ≫ g✝) ≫ h✝) = normalizeAux x✝ (f✝ ≫ g✝ ≫ h✝)
[PROOFSTEP]
rfl
[GOAL]
case mk.h.associator_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (fun p => normalizeAux p (f✝ ≫ g✝ ≫ h✝)) = fun p => normalizeAux p ((f✝ ≫ g✝) ≫ h✝)
[PROOFSTEP]

| _ => funext; rfl
[GOAL]
case mk.h.associator_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (fun p => normalizeAux p (f✝ ≫ g✝ ≫ h✝)) = fun p => normalizeAux p ((f✝ ≫ g✝) ≫ h✝)
[PROOFSTEP]
funext
[GOAL]
case mk.h.associator_inv.h
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (f✝ ≫ g✝ ≫ h✝) = normalizeAux x✝ ((f✝ ≫ g✝) ≫ h✝)
[PROOFSTEP]
rfl
[GOAL]
case mk.h.right_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p => normalizeAux p (f✝ ≫ 𝟙 b✝)) = fun p => normalizeAux p f✝
[PROOFSTEP]

| _ => funext; rfl
[GOAL]
case mk.h.right_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p => normalizeAux p (f✝ ≫ 𝟙 b✝)) = fun p => normalizeAux p f✝
[PROOFSTEP]
funext
[GOAL]
case mk.h.right_unitor.h
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (f✝ ≫ 𝟙 b✝) = normalizeAux x✝ f✝
[PROOFSTEP]
rfl
[GOAL]
case mk.h.right_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p => normalizeAux p f✝) = fun p => normalizeAux p (f✝ ≫ 𝟙 b✝)
[PROOFSTEP]

| _ => funext; rfl
[GOAL]
case mk.h.right_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p => normalizeAux p f✝) = fun p => normalizeAux p (f✝ ≫ 𝟙 b✝)
[PROOFSTEP]
funext
[GOAL]
case mk.h.right_unitor_inv.h
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
x✝ : Path a a✝
⊢ normalizeAux x✝ f✝ = normalizeAux x✝ (f✝ ≫ 𝟙 b✝)
[PROOFSTEP]
rfl
[GOAL]
case mk.h.left_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p => normalizeAux p (𝟙 a✝ ≫ f✝)) = fun p => normalizeAux p f✝
[PROOFSTEP]

| _ => funext; rfl
[GOAL]
case mk.h.left_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p => normalizeAux p (𝟙 a✝ ≫ f✝)) = fun p => normalizeAux p f✝
[PROOFSTEP]
funext
[GOAL]
case mk.h.left_unitor.h
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (𝟙 a✝ ≫ f✝) = normalizeAux x✝ f✝
[PROOFSTEP]
rfl
[GOAL]
case mk.h.left_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p => normalizeAux p f✝) = fun p => normalizeAux p (𝟙 a✝ ≫ f✝)
[PROOFSTEP]

| _ => funext; rfl
[GOAL]
case mk.h.left_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p => normalizeAux p f✝) = fun p => normalizeAux p (𝟙 a✝ ≫ f✝)
[PROOFSTEP]
funext
[GOAL]
case mk.h.left_unitor_inv.h
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
x✝ : Path a a✝
⊢ normalizeAux x✝ f✝ = normalizeAux x✝ (𝟙 a✝ ≫ f✝)
[PROOFSTEP]
rfl
[GOAL]
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
⊢ (↑(preinclusion B)).map { as := p } ◁ η ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f } = { as := normalizeAux p g }))
[PROOFSTEP]
rcases η with ⟨η'⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
η' : Hom₂ f g
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f } = { as := normalizeAux p g }))
[PROOFSTEP]
clear η
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η' : Hom₂ f g
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f } = { as := normalizeAux p g }))
[PROOFSTEP]
induction η' with
| id => simp
| vcomp η θ ihf ihg =>
  simp only [mk_vcomp, Bicategory.whiskerLeft_comp]
  slice_lhs 2 3 => rw [ihg]
  slice_lhs 1 2 => rw [ihf]
  simp
    -- p ≠ nil required! See the docstring of `normalizeAux`.
| whisker_left _ _ ih =>
  dsimp
  rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
  simp
| whisker_right h η' ih =>
  dsimp
  rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih, comp_whiskerRight]
  have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))
  dsimp at this ; simp [this]
| _ => simp
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η' : Hom₂ f g
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f } = { as := normalizeAux p g }))
[PROOFSTEP]
induction η' with
| id => simp
| vcomp η θ ihf ihg =>
  simp only [mk_vcomp, Bicategory.whiskerLeft_comp]
  slice_lhs 2 3 => rw [ihg]
  slice_lhs 1 2 => rw [ihf]
  simp
    -- p ≠ nil required! See the docstring of `normalizeAux`.
| whisker_left _ _ ih =>
  dsimp
  rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
  simp
| whisker_right h η' ih =>
  dsimp
  rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih, comp_whiskerRight]
  have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))
  dsimp at this ; simp [this]
| _ => simp
[GOAL]
case mk.id
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.id f✝) ≫ (normalizeIso p f✝).hom =
    (normalizeIso p f✝).hom ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p f✝ }))
[PROOFSTEP]

| id => simp
[GOAL]
case mk.id
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.id f✝) ≫ (normalizeIso p f✝).hom =
    (normalizeIso p f✝).hom ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p f✝ }))
[PROOFSTEP]
simp
[GOAL]
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.vcomp η θ) ≫ (normalizeIso p h✝).hom =
    (normalizeIso p f✝).hom ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p h✝ }))
[PROOFSTEP]

| vcomp η θ ihf ihg =>
  simp only [mk_vcomp, Bicategory.whiskerLeft_comp]
  slice_lhs 2 3 => rw [ihg]
  slice_lhs 1 2 => rw [ihf]
  simp
    -- p ≠ nil required! See the docstring of `normalizeAux`.
[GOAL]
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.vcomp η θ) ≫ (normalizeIso p h✝).hom =
    (normalizeIso p f✝).hom ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p h✝ }))
[PROOFSTEP]
simp only [mk_vcomp, Bicategory.whiskerLeft_comp]
[GOAL]
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
⊢ ((↑(preinclusion B)).map { as := p } ◁ Hom₂.mk η ≫ (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk θ) ≫
      (normalizeIso p h✝).hom =
    (normalizeIso p f✝).hom ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p h✝ }))
[PROOFSTEP]
slice_lhs 2 3 => rw [ihg]
[GOAL]
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk θ ≫ (normalizeIso p h✝).hom
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk η
[PROOFSTEP]
rw [ihg]
[GOAL]
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk θ ≫ (normalizeIso p h✝).hom
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk η
[PROOFSTEP]
rw [ihg]
[GOAL]
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk θ ≫ (normalizeIso p h✝).hom
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk η
[PROOFSTEP]
rw [ihg]
[GOAL]
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk η ≫
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ })) =
    (normalizeIso p f✝).hom ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p h✝ }))
[PROOFSTEP]
slice_lhs 1 2 => rw [ihf]
[GOAL]
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk η ≫ (normalizeIso p g✝).hom
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
[PROOFSTEP]
rw [ihf]
[GOAL]
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk η ≫ (normalizeIso p g✝).hom
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
[PROOFSTEP]
rw [ihf]
[GOAL]
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk η ≫ (normalizeIso p g✝).hom
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
| PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
[PROOFSTEP]
rw [ihf]
[GOAL]
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
ihg :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
⊢ ((normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))) ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ })) =
    (normalizeIso p f✝).hom ≫
      PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p h✝ }))
[PROOFSTEP]
simp
  -- p ≠ nil required! See the docstring of `normalizeAux`.
[GOAL]
case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih :
  ∀ (p : Path a b✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η✝ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.whisker_left f✝ η✝) ≫ (normalizeIso p (f✝ ≫ h✝)).hom =
    (normalizeIso p (f✝ ≫ g✝)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p (f✝ ≫ g✝) } = { as := normalizeAux p (f✝ ≫ h✝) }))
[PROOFSTEP]

| whisker_left _ _ ih =>
  dsimp
  rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
  simp
[GOAL]
case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih :
  ∀ (p : Path a b✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η✝ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.whisker_left f✝ η✝) ≫ (normalizeIso p (f✝ ≫ h✝)).hom =
    (normalizeIso p (f✝ ≫ g✝)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p (f✝ ≫ g✝) } = { as := normalizeAux p (f✝ ≫ h✝) }))
[PROOFSTEP]
dsimp
[GOAL]
case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih :
  ∀ (p : Path a b✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η✝ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ f✝ ◁ Hom₂.mk η✝ ≫
      (α_ ((↑(preinclusion B)).map { as := p }) f✝ h✝).inv ≫
        (normalizeIso p f✝).hom ▷ h✝ ≫ (normalizeIso (normalizeAux p f✝) h✝).hom =
    ((α_ ((↑(preinclusion B)).map { as := p }) f✝ g✝).inv ≫
        (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom) ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux (normalizeAux p f✝) g✝ } = { as := normalizeAux (normalizeAux p f✝) h✝ }))
[PROOFSTEP]
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
[GOAL]
case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih :
  ∀ (p : Path a b✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η✝ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p g✝ } = { as := normalizeAux p h✝ }))
p : Path a a✝
⊢ (α_ ((↑(preinclusion B)).map { as := p }) f✝ g✝).inv ≫
      (normalizeIso p f✝).hom ▷ g✝ ≫
        (normalizeIso (normalizeAux p f✝) g✝).hom ≫
          PrelaxFunctor.map₂ (preinclusion B)
            (eqToHom
              (_ : { as := normalizeAux (normalizeAux p f✝) g✝ } = { as := normalizeAux (normalizeAux p f✝) h✝ })) =
    ((α_ ((↑(preinclusion B)).map { as := p }) f✝ g✝).inv ≫
        (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom) ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux (normalizeAux p f✝) g✝ } = { as := normalizeAux (normalizeAux p f✝) h✝ }))
[PROOFSTEP]
simp
[GOAL]
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.whisker_right h η') ≫ (normalizeIso p (Hom.comp g✝ h)).hom =
    (normalizeIso p (Hom.comp f✝ h)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p (Hom.comp f✝ h) } = { as := normalizeAux p (Hom.comp g✝ h) }))
[PROOFSTEP]

| whisker_right h η' ih =>
  dsimp
  rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih, comp_whiskerRight]
  have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))
  dsimp at this ; simp [this]
[GOAL]
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.whisker_right h η') ≫ (normalizeIso p (Hom.comp g✝ h)).hom =
    (normalizeIso p (Hom.comp f✝ h)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p (Hom.comp f✝ h) } = { as := normalizeAux p (Hom.comp g✝ h) }))
[PROOFSTEP]
dsimp
[GOAL]
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Hom₂.mk η' ▷ h ≫
      (α_ ((↑(preinclusion B)).map { as := p }) g✝ h).inv ≫
        (normalizeIso p g✝).hom ▷ h ≫ (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((↑(preinclusion B)).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux (normalizeAux p f✝) h } = { as := normalizeAux (normalizeAux p g✝) h }))
[PROOFSTEP]
rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih, comp_whiskerRight]
[GOAL]
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
p : Path a a✝
⊢ (α_ ((↑(preinclusion B)).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫
          PrelaxFunctor.map₂ (preinclusion B)
              (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ })) ▷
            h) ≫
        (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((↑(preinclusion B)).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux (normalizeAux p f✝) h } = { as := normalizeAux (normalizeAux p g✝) h }))
[PROOFSTEP]
have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))
[GOAL]
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
p : Path a a✝
this :
  (normalizeIso (normalizeAux p f✝) h).hom =
    eqToHom
        (_ :
          (↑(preinclusion B)).map { as := normalizeAux p f✝ } ≫ h =
            (↑(preinclusion B)).map { as := normalizeAux p g✝ } ≫ h) ≫
      (normalizeIso (normalizeAux p g✝) h).hom ≫
        eqToHom
          (_ :
            (↑(preinclusion B)).map { as := normalizeAux (normalizeAux p g✝) h } =
              (↑(preinclusion B)).map { as := normalizeAux (normalizeAux p f✝) h })
⊢ (α_ ((↑(preinclusion B)).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫
          PrelaxFunctor.map₂ (preinclusion B)
              (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ })) ▷
            h) ≫
        (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((↑(preinclusion B)).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux (normalizeAux p f✝) h } = { as := normalizeAux (normalizeAux p g✝) h }))
[PROOFSTEP]
dsimp at this
[GOAL]
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫
        PrelaxFunctor.map₂ (preinclusion B) (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ }))
p : Path a a✝
this :
  (normalizeIso (normalizeAux p f✝) h).hom =
    eqToHom
        (_ :
          (↑(preinclusion B)).map { as := normalizeAux p f✝ } ≫ h =
            (↑(preinclusion B)).map { as := normalizeAux p g✝ } ≫ h) ≫
      (normalizeIso (normalizeAux p g✝) h).hom ≫
        eqToHom
          (_ :
            (↑(preinclusion B)).map { as := normalizeAux (normalizeAux p g✝) h } =
              (↑(preinclusion B)).map { as := normalizeAux (normalizeAux p f✝) h })
⊢ (α_ ((↑(preinclusion B)).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫
          PrelaxFunctor.map₂ (preinclusion B)
              (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p g✝ })) ▷
            h) ≫
        (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((↑(preinclusion B)).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux (normalizeAux p f✝) h } = { as := normalizeAux (normalizeAux p g✝) h }))
[PROOFSTEP]
simp [this]
[GOAL]
case mk.associator
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.associator f✝ g✝ h✝) ≫ (normalizeIso p (f✝ ≫ g✝ ≫ h✝)).hom =
    (normalizeIso p ((f✝ ≫ g✝) ≫ h✝)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p ((f✝ ≫ g✝) ≫ h✝) } = { as := normalizeAux p (f✝ ≫ g✝ ≫ h✝) }))
[PROOFSTEP]

| _ => simp
[GOAL]
case mk.associator
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.associator f✝ g✝ h✝) ≫ (normalizeIso p (f✝ ≫ g✝ ≫ h✝)).hom =
    (normalizeIso p ((f✝ ≫ g✝) ≫ h✝)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p ((f✝ ≫ g✝) ≫ h✝) } = { as := normalizeAux p (f✝ ≫ g✝ ≫ h✝) }))
[PROOFSTEP]
simp
[GOAL]
case mk.associator_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.associator_inv f✝ g✝ h✝) ≫
      (normalizeIso p ((f✝ ≫ g✝) ≫ h✝)).hom =
    (normalizeIso p (f✝ ≫ g✝ ≫ h✝)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p (f✝ ≫ g✝ ≫ h✝) } = { as := normalizeAux p ((f✝ ≫ g✝) ≫ h✝) }))
[PROOFSTEP]

| _ => simp
[GOAL]
case mk.associator_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.associator_inv f✝ g✝ h✝) ≫
      (normalizeIso p ((f✝ ≫ g✝) ≫ h✝)).hom =
    (normalizeIso p (f✝ ≫ g✝ ≫ h✝)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p (f✝ ≫ g✝ ≫ h✝) } = { as := normalizeAux p ((f✝ ≫ g✝) ≫ h✝) }))
[PROOFSTEP]
simp
[GOAL]
case mk.right_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.right_unitor f✝) ≫ (normalizeIso p f✝).hom =
    (normalizeIso p (f✝ ≫ 𝟙 b✝)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p (f✝ ≫ 𝟙 b✝) } = { as := normalizeAux p f✝ }))
[PROOFSTEP]

| _ => simp
[GOAL]
case mk.right_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.right_unitor f✝) ≫ (normalizeIso p f✝).hom =
    (normalizeIso p (f✝ ≫ 𝟙 b✝)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p (f✝ ≫ 𝟙 b✝) } = { as := normalizeAux p f✝ }))
[PROOFSTEP]
simp
[GOAL]
case mk.right_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.right_unitor_inv f✝) ≫ (normalizeIso p (f✝ ≫ 𝟙 b✝)).hom =
    (normalizeIso p f✝).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p (f✝ ≫ 𝟙 b✝) }))
[PROOFSTEP]

| _ => simp
[GOAL]
case mk.right_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.right_unitor_inv f✝) ≫ (normalizeIso p (f✝ ≫ 𝟙 b✝)).hom =
    (normalizeIso p f✝).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p (f✝ ≫ 𝟙 b✝) }))
[PROOFSTEP]
simp
[GOAL]
case mk.left_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.left_unitor f✝) ≫ (normalizeIso p f✝).hom =
    (normalizeIso p (𝟙 a✝ ≫ f✝)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p (𝟙 a✝ ≫ f✝) } = { as := normalizeAux p f✝ }))
[PROOFSTEP]

| _ => simp
[GOAL]
case mk.left_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.left_unitor f✝) ≫ (normalizeIso p f✝).hom =
    (normalizeIso p (𝟙 a✝ ≫ f✝)).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p (𝟙 a✝ ≫ f✝) } = { as := normalizeAux p f✝ }))
[PROOFSTEP]
simp
[GOAL]
case mk.left_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.left_unitor_inv f✝) ≫ (normalizeIso p (𝟙 a✝ ≫ f✝)).hom =
    (normalizeIso p f✝).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p (𝟙 a✝ ≫ f✝) }))
[PROOFSTEP]

| _ => simp
[GOAL]
case mk.left_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (↑(preinclusion B)).map { as := p } ◁ Quot.mk Rel (Hom₂.left_unitor_inv f✝) ≫ (normalizeIso p (𝟙 a✝ ≫ f✝)).hom =
    (normalizeIso p f✝).hom ≫
      PrelaxFunctor.map₂ (preinclusion B)
        (eqToHom (_ : { as := normalizeAux p f✝ } = { as := normalizeAux p (𝟙 a✝ ≫ f✝) }))
[PROOFSTEP]
simp
[GOAL]
B : Type u
inst✝ : Quiver B
a b c : B
f : Hom a b
g : Hom b c
⊢ normalizeAux nil (Hom.comp f g) = comp (normalizeAux nil f) (normalizeAux nil g)
[PROOFSTEP]
induction g generalizing a with
| id => rfl
| of => rfl
| comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
[GOAL]
B : Type u
inst✝ : Quiver B
a b c : B
f : Hom a b
g : Hom b c
⊢ normalizeAux nil (Hom.comp f g) = comp (normalizeAux nil f) (normalizeAux nil g)
[PROOFSTEP]
induction g generalizing a with
| id => rfl
| of => rfl
| comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
[GOAL]
case id
B : Type u
inst✝ : Quiver B
b c a✝ a : B
f : Hom a a✝
⊢ normalizeAux nil (Hom.comp f (Hom.id a✝)) = comp (normalizeAux nil f) (normalizeAux nil (Hom.id a✝))
[PROOFSTEP]

| id => rfl
[GOAL]
case id
B : Type u
inst✝ : Quiver B
b c a✝ a : B
f : Hom a a✝
⊢ normalizeAux nil (Hom.comp f (Hom.id a✝)) = comp (normalizeAux nil f) (normalizeAux nil (Hom.id a✝))
[PROOFSTEP]
rfl
[GOAL]
case of
B : Type u
inst✝ : Quiver B
b c a✝ b✝ : B
f✝ : a✝ ⟶ b✝
a : B
f : Hom a a✝
⊢ normalizeAux nil (Hom.comp f (Hom.of f✝)) = comp (normalizeAux nil f) (normalizeAux nil (Hom.of f✝))
[PROOFSTEP]

| of => rfl
[GOAL]
case of
B : Type u
inst✝ : Quiver B
b c a✝ b✝ : B
f✝ : a✝ ⟶ b✝
a : B
f : Hom a a✝
⊢ normalizeAux nil (Hom.comp f (Hom.of f✝)) = comp (normalizeAux nil f) (normalizeAux nil (Hom.of f✝))
[PROOFSTEP]
rfl
[GOAL]
case comp
B : Type u
inst✝ : Quiver B
b c a✝ b✝ c✝ : B
g : Hom a✝ b✝
g✝ : Hom b✝ c✝
ihf : ∀ {a : B} (f : Hom a a✝), normalizeAux nil (Hom.comp f g) = comp (normalizeAux nil f) (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (Hom.comp f g✝) = comp (normalizeAux nil f) (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ normalizeAux nil (Hom.comp f (Hom.comp g g✝)) = comp (normalizeAux nil f) (normalizeAux nil (Hom.comp g g✝))
[PROOFSTEP]

| comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
[GOAL]
case comp
B : Type u
inst✝ : Quiver B
b c a✝ b✝ c✝ : B
g : Hom a✝ b✝
g✝ : Hom b✝ c✝
ihf : ∀ {a : B} (f : Hom a a✝), normalizeAux nil (Hom.comp f g) = comp (normalizeAux nil f) (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (Hom.comp f g✝) = comp (normalizeAux nil f) (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ normalizeAux nil (Hom.comp f (Hom.comp g g✝)) = comp (normalizeAux nil f) (normalizeAux nil (Hom.comp g g✝))
[PROOFSTEP]
erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
[GOAL]
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : X ⟶ Y),
    (𝟭 (a ⟶ b)).map f ≫ ((fun f => (λ_ f).symm ≪≫ normalizeIso nil f) Y).hom =
      ((fun f => (λ_ f).symm ≪≫ normalizeIso nil f) X).hom ≫
        (Pseudofunctor.mapFunctor (normalize B) a b ⋙ inclusionPath a b).map f
[PROOFSTEP]
intro f g η
[GOAL]
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
⊢ (𝟭 (a ⟶ b)).map η ≫ ((fun f => (λ_ f).symm ≪≫ normalizeIso nil f) g).hom =
    ((fun f => (λ_ f).symm ≪≫ normalizeIso nil f) f).hom ≫
      (Pseudofunctor.mapFunctor (normalize B) a b ⋙ inclusionPath a b).map η
[PROOFSTEP]
erw [leftUnitor_inv_naturality_assoc, assoc]
[GOAL]
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
⊢ (λ_ ((𝟭 (a ⟶ b)).obj f)).inv ≫ 𝟙 a ◁ (𝟭 (a ⟶ b)).map η ≫ (normalizeIso nil g).hom =
    (λ_ f).symm.hom ≫ (normalizeIso nil f).hom ≫ (Pseudofunctor.mapFunctor (normalize B) a b ⋙ inclusionPath a b).map η
[PROOFSTEP]
congr 1
[GOAL]
case e_a
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
⊢ 𝟙 a ◁ (𝟭 (a ⟶ b)).map η ≫ (normalizeIso nil g).hom =
    (normalizeIso nil f).hom ≫ (Pseudofunctor.mapFunctor (normalize B) a b ⋙ inclusionPath a b).map η
[PROOFSTEP]
exact normalize_naturality nil η
[GOAL]
B : Type u
inst✝ : Quiver B
a b : B
f : Discrete (Path a b)
⊢ (inclusionPath a b ⋙ Pseudofunctor.mapFunctor (normalize B) a b).obj f = (𝟭 (Discrete (Path a b))).obj f
[PROOFSTEP]
induction' f with f
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b : B
f : Path a b
⊢ (inclusionPath a b ⋙ Pseudofunctor.mapFunctor (normalize B) a b).obj { as := f } =
    (𝟭 (Discrete (Path a b))).obj { as := f }
[PROOFSTEP]
induction' f with _ _ _ _ ih
[GOAL]
case mk.nil
B : Type u
inst✝ : Quiver B
a b : B
⊢ (inclusionPath a a ⋙ Pseudofunctor.mapFunctor (normalize B) a a).obj { as := nil } =
    (𝟭 (Discrete (Path a a))).obj { as := nil }
[PROOFSTEP]
rfl
[GOAL]
case mk.cons
B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih :
  (inclusionPath a b✝ ⋙ Pseudofunctor.mapFunctor (normalize B) a b✝).obj { as := a✝¹ } =
    (𝟭 (Discrete (Path a b✝))).obj { as := a✝¹ }
⊢ (inclusionPath a c✝ ⋙ Pseudofunctor.mapFunctor (normalize B) a c✝).obj { as := cons a✝¹ a✝ } =
    (𝟭 (Discrete (Path a c✝))).obj { as := cons a✝¹ a✝ }
[PROOFSTEP]
ext1
[GOAL]
case mk.cons.as
B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih :
  (inclusionPath a b✝ ⋙ Pseudofunctor.mapFunctor (normalize B) a b✝).obj { as := a✝¹ } =
    (𝟭 (Discrete (Path a b✝))).obj { as := a✝¹ }
⊢ ((inclusionPath a c✝ ⋙ Pseudofunctor.mapFunctor (normalize B) a c✝).obj { as := cons a✝¹ a✝ }).as =
    ((𝟭 (Discrete (Path a c✝))).obj { as := cons a✝¹ a✝ }).as
[PROOFSTEP]
injection ih with ih
[GOAL]
case mk.cons.as
B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih : normalizeAux nil ((inclusionPath a b✝).obj { as := a✝¹ }) = a✝¹
⊢ ((inclusionPath a c✝ ⋙ Pseudofunctor.mapFunctor (normalize B) a c✝).obj { as := cons a✝¹ a✝ }).as =
    ((𝟭 (Discrete (Path a c✝))).obj { as := cons a✝¹ a✝ }).as
[PROOFSTEP]
conv =>
  rhs
  rw [← ih]
[GOAL]
B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih : normalizeAux nil ((inclusionPath a b✝).obj { as := a✝¹ }) = a✝¹
| ((inclusionPath a c✝ ⋙ Pseudofunctor.mapFunctor (normalize B) a c✝).obj { as := cons a✝¹ a✝ }).as =
    ((𝟭 (Discrete (Path a c✝))).obj { as := cons a✝¹ a✝ }).as
[PROOFSTEP]
  rhs
  rw [← ih]
[GOAL]
B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih : normalizeAux nil ((inclusionPath a b✝).obj { as := a✝¹ }) = a✝¹
| ((inclusionPath a c✝ ⋙ Pseudofunctor.mapFunctor (normalize B) a c✝).obj { as := cons a✝¹ a✝ }).as =
    ((𝟭 (Discrete (Path a c✝))).obj { as := cons a✝¹ a✝ }).as
[PROOFSTEP]
  rhs
  rw [← ih]
[GOAL]
B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih : normalizeAux nil ((inclusionPath a b✝).obj { as := a✝¹ }) = a✝¹
| ((inclusionPath a c✝ ⋙ Pseudofunctor.mapFunctor (normalize B) a c✝).obj { as := cons a✝¹ a✝ }).as =
    ((𝟭 (Discrete (Path a c✝))).obj { as := cons a✝¹ a✝ }).as
[PROOFSTEP]
rhs
[GOAL]
B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih : normalizeAux nil ((inclusionPath a b✝).obj { as := a✝¹ }) = a✝¹
| ((𝟭 (Discrete (Path a c✝))).obj { as := cons a✝¹ a✝ }).as
[PROOFSTEP]
rw [← ih]


[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => (F.obj X.fst).obj X.snd,
          map := fun {X Y} f => NatTrans.app (F.map f.fst) X.snd ≫ (F.obj Y.fst).map f.snd }.map
      (f ≫ g) =
    { obj := fun X => (F.obj X.fst).obj X.snd,
            map := fun {X Y} f => NatTrans.app (F.map f.fst) X.snd ≫ (F.obj Y.fst).map f.snd }.map
        f ≫
      { obj := fun X => (F.obj X.fst).obj X.snd,
            map := fun {X Y} f => NatTrans.app (F.map f.fst) X.snd ≫ (F.obj Y.fst).map f.snd }.map
        g
[PROOFSTEP]
simp only [prod_comp_fst, prod_comp_snd, Functor.map_comp, NatTrans.comp_app, Category.assoc]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ NatTrans.app (F.map f.fst) X✝.snd ≫
      NatTrans.app (F.map g.fst) X✝.snd ≫ (F.obj Z✝.fst).map f.snd ≫ (F.obj Z✝.fst).map g.snd =
    NatTrans.app (F.map f.fst) X✝.snd ≫
      (F.obj Y✝.fst).map f.snd ≫ NatTrans.app (F.map g.fst) Y✝.snd ≫ (F.obj Z✝.fst).map g.snd
[PROOFSTEP]
slice_lhs 2 3 => rw [← NatTrans.naturality]
[GOAL]
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map g.fst) X✝.snd ≫ (F.obj Z✝.fst).map f.snd
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.obj Z✝.fst).map g.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map f.fst) X✝.snd
[PROOFSTEP]
rw [← NatTrans.naturality]
[GOAL]
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map g.fst) X✝.snd ≫ (F.obj Z✝.fst).map f.snd
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.obj Z✝.fst).map g.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map f.fst) X✝.snd
[PROOFSTEP]
rw [← NatTrans.naturality]
[GOAL]
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map g.fst) X✝.snd ≫ (F.obj Z✝.fst).map f.snd
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.obj Z✝.fst).map g.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map f.fst) X✝.snd
[PROOFSTEP]
rw [← NatTrans.naturality]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ NatTrans.app (F.map f.fst) X✝.snd ≫
      ((F.obj Y✝.fst).map f.snd ≫ NatTrans.app (F.map g.fst) Y✝.snd) ≫ (F.obj Z✝.fst).map g.snd =
    NatTrans.app (F.map f.fst) X✝.snd ≫
      (F.obj Y✝.fst).map f.snd ≫ NatTrans.app (F.map g.fst) Y✝.snd ≫ (F.obj Z✝.fst).map g.snd
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
⊢ ((fun F =>
              Functor.mk
                { obj := fun X => (F.obj X.fst).obj X.snd,
                  map := fun {X Y} f => NatTrans.app (F.map f.fst) X.snd ≫ (F.obj Y.fst).map f.snd })
            X✝).map
        f ≫
      (fun X => NatTrans.app (NatTrans.app T X.fst) X.snd) Y =
    (fun X => NatTrans.app (NatTrans.app T X.fst) X.snd) X ≫
      ((fun F =>
              Functor.mk
                { obj := fun X => (F.obj X.fst).obj X.snd,
                  map := fun {X Y} f => NatTrans.app (F.map f.fst) X.snd ≫ (F.obj Y.fst).map f.snd })
            Y✝).map
        f
[PROOFSTEP]
simp only [prod_comp_fst, prod_comp_snd, Category.comp_id, Category.assoc, Functor.map_id, Functor.map_comp,
  NatTrans.id_app, NatTrans.comp_app]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
⊢ NatTrans.app (X✝.map f.fst) X.snd ≫ (X✝.obj Y.fst).map f.snd ≫ NatTrans.app (NatTrans.app T Y.fst) Y.snd =
    NatTrans.app (NatTrans.app T X.fst) X.snd ≫ NatTrans.app (Y✝.map f.fst) X.snd ≫ (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
slice_lhs 2 3 => rw [NatTrans.naturality]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.obj Y.fst).map f.snd ≫ NatTrans.app (NatTrans.app T Y.fst) Y.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd
[PROOFSTEP]
rw [NatTrans.naturality]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.obj Y.fst).map f.snd ≫ NatTrans.app (NatTrans.app T Y.fst) Y.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd
[PROOFSTEP]
rw [NatTrans.naturality]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.obj Y.fst).map f.snd ≫ NatTrans.app (NatTrans.app T Y.fst) Y.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd
[PROOFSTEP]
rw [NatTrans.naturality]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
⊢ NatTrans.app (X✝.map f.fst) X.snd ≫ NatTrans.app (NatTrans.app T Y.fst) X.snd ≫ (Y✝.obj Y.fst).map f.snd =
    NatTrans.app (NatTrans.app T X.fst) X.snd ≫ NatTrans.app (Y✝.map f.fst) X.snd ≫ (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
slice_lhs 1 2 => rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd ≫ NatTrans.app (NatTrans.app T Y.fst) X.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd ≫ NatTrans.app (NatTrans.app T Y.fst) X.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd ≫ NatTrans.app (NatTrans.app T Y.fst) X.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
⊢ (NatTrans.app (NatTrans.app T X.fst) X.snd ≫ NatTrans.app (Y✝.map f.fst) X.snd) ≫ (Y✝.obj Y.fst).map f.snd =
    NatTrans.app (NatTrans.app T X.fst) X.snd ≫ NatTrans.app (Y✝.map f.fst) X.snd ≫ (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
Y : D
⊢ { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }.map (𝟙 Y) =
    𝟙 ({ obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }.obj Y)
[PROOFSTEP]
simp only [F.map_id]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
Y : D
⊢ F.map (𝟙 X, 𝟙 Y) = 𝟙 (F.obj (X, Y))
[PROOFSTEP]
rw [← prod_id]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
Y : D
⊢ F.map (𝟙 (X, Y)) = 𝟙 (F.obj (X, Y))
[PROOFSTEP]
exact F.map_id ⟨X, Y⟩
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }.map (f ≫ g) =
    { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }.map f ≫
      { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }.map g
[PROOFSTEP]
simp [← F.map_comp]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X✝ Y✝ : C
f : X✝ ⟶ Y✝
Y Y' : D
g : Y ⟶ Y'
⊢ ((fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }) X✝).map g ≫
      (fun Y => F.map (f, 𝟙 Y)) Y' =
    (fun Y => F.map (f, 𝟙 Y)) Y ≫
      ((fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }) Y✝).map g
[PROOFSTEP]
simp [← F.map_comp]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
⊢ { obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
          map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
            map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.obj
        X)
[PROOFSTEP]
ext Y
[GOAL]
case w.h
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
Y : D
⊢ NatTrans.app
      ({ obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
            map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
        (𝟙 X))
      Y =
    NatTrans.app
      (𝟙
        ({ obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
              map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.obj
          X))
      Y
[PROOFSTEP]
exact F.map_id _
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
          map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
      (f ≫ g) =
    { obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
            map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
        f ≫
      { obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
            map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
        g
[PROOFSTEP]
ext Y
[GOAL]
case w.h
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
Y : D
⊢ NatTrans.app
      ({ obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
            map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
        (f ≫ g))
      Y =
    NatTrans.app
      ({ obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
              map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
          f ≫
        { obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
              map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
          g)
      Y
[PROOFSTEP]
dsimp
[GOAL]
case w.h
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
Y : D
⊢ F.map (f ≫ g, 𝟙 Y) = F.map (f, 𝟙 Y) ≫ F.map (g, 𝟙 Y)
[PROOFSTEP]
simp [← F.map_comp]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X : C
Y Y' : D
g : Y ⟶ Y'
⊢ (((fun F => curryObj F) X✝).obj X).map g ≫ (fun Y => NatTrans.app T (X, Y)) Y' =
    (fun Y => NatTrans.app T (X, Y)) Y ≫ (((fun F => curryObj F) Y✝).obj X).map g
[PROOFSTEP]
dsimp [curryObj]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X : C
Y Y' : D
g : Y ⟶ Y'
⊢ X✝.map (𝟙 X, g) ≫ NatTrans.app T (X, Y') = NatTrans.app T (X, Y) ≫ Y✝.map (𝟙 X, g)
[PROOFSTEP]
rw [NatTrans.naturality]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X X' : C
f : X ⟶ X'
⊢ ((fun F => curryObj F) X✝).map f ≫ (fun X => NatTrans.mk fun Y => NatTrans.app T (X, Y)) X' =
    (fun X => NatTrans.mk fun Y => NatTrans.app T (X, Y)) X ≫ ((fun F => curryObj F) Y✝).map f
[PROOFSTEP]
ext
[GOAL]
case w.h
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X X' : C
f : X ⟶ X'
x✝ : D
⊢ NatTrans.app (((fun F => curryObj F) X✝).map f ≫ (fun X => NatTrans.mk fun Y => NatTrans.app T (X, Y)) X') x✝ =
    NatTrans.app ((fun X => NatTrans.mk fun Y => NatTrans.app T (X, Y)) X ≫ ((fun F => curryObj F) Y✝).map f) x✝
[PROOFSTEP]
dsimp [curryObj]
[GOAL]
case w.h
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X X' : C
f : X ⟶ X'
x✝ : D
⊢ X✝.map (f, 𝟙 x✝) ≫ NatTrans.app T (X', x✝) = NatTrans.app T (X, x✝) ≫ Y✝.map (f, 𝟙 x✝)
[PROOFSTEP]
rw [NatTrans.naturality]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C × D
⊢ ((curry ⋙ uncurry).obj F).obj X = ((𝟭 (C × D ⥤ E)).obj F).obj X
[PROOFSTEP]
simp
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
⊢ ∀ {X Y : C × D} (f : X ⟶ Y),
    ((curry ⋙ uncurry).obj F).map f ≫ ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) Y).hom =
      ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) X).hom ≫ ((𝟭 (C × D ⥤ E)).obj F).map f
[PROOFSTEP]
intros X Y f
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X Y : C × D
f : X ⟶ Y
⊢ ((curry ⋙ uncurry).obj F).map f ≫ ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) Y).hom =
    ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) X).hom ≫ ((𝟭 (C × D ⥤ E)).obj F).map f
[PROOFSTEP]
cases X
[GOAL]
case mk
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
Y : C × D
fst✝ : C
snd✝ : D
f : (fst✝, snd✝) ⟶ Y
⊢ ((curry ⋙ uncurry).obj F).map f ≫ ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) Y).hom =
    ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) (fst✝, snd✝)).hom ≫ ((𝟭 (C × D ⥤ E)).obj F).map f
[PROOFSTEP]
cases Y
[GOAL]
case mk.mk
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
fst✝¹ : C
snd✝¹ : D
fst✝ : C
snd✝ : D
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ ((curry ⋙ uncurry).obj F).map f ≫ ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) (fst✝, snd✝)).hom =
    ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) (fst✝¹, snd✝¹)).hom ≫ ((𝟭 (C × D ⥤ E)).obj F).map f
[PROOFSTEP]
cases f
[GOAL]
case mk.mk.mk
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
fst✝² : C
snd✝² : D
fst✝¹ : C
snd✝¹ : D
fst✝ : (fst✝², snd✝²).fst ⟶ (fst✝¹, snd✝¹).fst
snd✝ : (fst✝², snd✝²).snd ⟶ (fst✝¹, snd✝¹).snd
⊢ ((curry ⋙ uncurry).obj F).map (fst✝, snd✝) ≫
      ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) (fst✝¹, snd✝¹)).hom =
    ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) (fst✝², snd✝²)).hom ≫
      ((𝟭 (C × D ⥤ E)).obj F).map (fst✝, snd✝)
[PROOFSTEP]
dsimp at *
[GOAL]
case mk.mk.mk
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
fst✝² : C
snd✝² : D
fst✝¹ : C
snd✝¹ : D
fst✝ : (fst✝², snd✝²).fst ⟶ (fst✝¹, snd✝¹).fst
snd✝ : (fst✝², snd✝²).snd ⟶ (fst✝¹, snd✝¹).snd
⊢ (F.map (fst✝, 𝟙 snd✝²) ≫ F.map (𝟙 fst✝¹, snd✝)) ≫ 𝟙 (F.obj (fst✝¹, snd✝¹)) =
    𝟙 (F.obj (fst✝², snd✝²)) ≫ F.map (fst✝, snd✝)
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
case mk.mk.mk
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
fst✝² : C
snd✝² : D
fst✝¹ : C
snd✝¹ : D
fst✝ : (fst✝², snd✝²).fst ⟶ (fst✝¹, snd✝¹).fst
snd✝ : (fst✝², snd✝²).snd ⟶ (fst✝¹, snd✝¹).snd
⊢ F.map ((fst✝, 𝟙 snd✝²) ≫ (𝟙 fst✝¹, snd✝)) ≫ 𝟙 (F.obj (fst✝¹, snd✝¹)) = 𝟙 (F.obj (fst✝², snd✝²)) ≫ F.map (fst✝, snd✝)
[PROOFSTEP]
simp


[GOAL]
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalPreadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasEqualizers C
inst✝³ : HasCokernels C
inst✝² : HasImages C
inst✝¹ : HasImageMaps C
inst✝ : HasProjectiveResolutions C
n : ℕ
X Y : C
f : X ⟶ Y
Z : C
⊢ NatTrans.app ((Tor' C n).map f) Z = (Functor.leftDerived ((tensoringRight C).obj Z) n).map f
[PROOFSTEP]
rfl
  -- porting note: this specific lemma was added because otherwise the internals of
  -- `NatTrans.leftDerived` leaks into the RHS (it was already so in mathlib)
[GOAL]
C : Type u_1
inst✝¹⁰ : Category.{?u.11756, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalPreadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasEqualizers C
inst✝⁴ : HasCokernels C
inst✝³ : HasImages C
inst✝² : HasImageMaps C
inst✝¹ : HasProjectiveResolutions C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ ((Tor' C (n + 1)).obj X).obj Y ≅ 0
[PROOFSTEP]
dsimp only [Tor', Functor.flip]
[GOAL]
C : Type u_1
inst✝¹⁰ : Category.{?u.11756, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalPreadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasEqualizers C
inst✝⁴ : HasCokernels C
inst✝³ : HasImages C
inst✝² : HasImageMaps C
inst✝¹ : HasProjectiveResolutions C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ (Functor.leftDerived ((tensoringRight C).obj Y) (n + 1)).obj X ≅ 0
[PROOFSTEP]
exact ((tensoringRight C).obj Y).leftDerivedObjProjectiveSucc n X


[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r : R
α : F ⟶ G
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ (fun X => r • NatTrans.app α X) Y = (fun X => r • NatTrans.app α X) X ≫ G.map f
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r : R
α : F ⟶ G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ F.map f✝ ≫ (fun X => r • NatTrans.app α X) Y✝ = (fun X => r • NatTrans.app α X) X✝ ≫ G.map f✝
[PROOFSTEP]
rw [comp_smul, smul_comp, α.naturality]
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (b : F ⟶ G), 1 • b = b
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
b✝ : F ⟶ G
⊢ 1 • b✝ = b✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
b✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (1 • b✝) x✝ = NatTrans.app b✝ x✝
[PROOFSTEP]
apply one_smul
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (x y : R) (b : F ⟶ G), (x * y) • b = x • y • b
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
x✝ y✝ : R
b✝ : F ⟶ G
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
x✝¹ y✝ : R
b✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app ((x✝¹ * y✝) • b✝) x✝ = NatTrans.app (x✝¹ • y✝ • b✝) x✝
[PROOFSTEP]
apply mul_smul
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (a : R), a • 0 = 0
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
a✝ : R
⊢ a✝ • 0 = 0
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
a✝ : R
x✝ : C
⊢ NatTrans.app (a✝ • 0) x✝ = NatTrans.app 0 x✝
[PROOFSTEP]
apply smul_zero
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (a : R) (x y : F ⟶ G), a • (x + y) = a • x + a • y
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
a✝ : R
x✝ y✝ : F ⟶ G
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
a✝ : R
x✝¹ y✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (a✝ • (x✝¹ + y✝)) x✝ = NatTrans.app (a✝ • x✝¹ + a✝ • y✝) x✝
[PROOFSTEP]
apply smul_add
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (r s : R) (x : F ⟶ G), (r + s) • x = r • x + s • x
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r✝ s✝ : R
x✝ : F ⟶ G
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r✝ s✝ : R
x✝¹ : F ⟶ G
x✝ : C
⊢ NatTrans.app ((r✝ + s✝) • x✝¹) x✝ = NatTrans.app (r✝ • x✝¹ + s✝ • x✝¹) x✝
[PROOFSTEP]
apply add_smul
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (x : F ⟶ G), 0 • x = 0
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
x✝ : F ⟶ G
⊢ 0 • x✝ = 0
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
x✝¹ : F ⟶ G
x✝ : C
⊢ NatTrans.app (0 • x✝¹) x✝ = NatTrans.app 0 x✝
[PROOFSTEP]
apply zero_smul
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
⊢ ∀ (X Y Z : C ⥤ D) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
X✝ Y✝ Z✝ : C ⥤ D
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ (r✝ • f✝) ≫ g✝ = r✝ • f✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
X✝ Y✝ Z✝ : C ⥤ D
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : C
⊢ NatTrans.app ((r✝ • f✝) ≫ g✝) x✝ = NatTrans.app (r✝ • f✝ ≫ g✝) x✝
[PROOFSTEP]
apply smul_comp
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
⊢ ∀ (X Y Z : C ⥤ D) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
X✝ Y✝ Z✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ f✝ ≫ (r✝ • g✝) = r✝ • f✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{?u.87, u_2} C
inst✝² : Category.{?u.91, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
X✝ Y✝ Z✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
x✝ : C
⊢ NatTrans.app (f✝ ≫ (r✝ • g✝)) x✝ = NatTrans.app (r✝ • f✝ ≫ g✝) x✝
[PROOFSTEP]
apply comp_smul