mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: 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✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (f✝ ≫ g✝ ≫ h✝) = normalizeAux x✝ ((f✝ ≫ g✝) ≫ h✝)

Tactic:
;

Goal state after:
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✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (f✝ ≫ g✝ ≫ h✝) = normalizeAux x✝ ((f✝ ≫ g✝) ≫ h✝)
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: 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✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (f✝ ≫ 𝟙 b✝) = normalizeAux x✝ f✝

Tactic:
;

Goal state after:
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✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (f✝ ≫ 𝟙 b✝) = normalizeAux x✝ f✝
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: 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✝
x✝ : Path a a✝
⊢ normalizeAux x✝ f✝ = normalizeAux x✝ (f✝ ≫ 𝟙 b✝)

Tactic:
;

Goal state after:
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✝
x✝ : Path a a✝
⊢ normalizeAux x✝ f✝ = normalizeAux x✝ (f✝ ≫ 𝟙 b✝)
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: 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✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (𝟙 a✝ ≫ f✝) = normalizeAux x✝ f✝

Tactic:
;

Goal state after:
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✝
x✝ : Path a a✝
⊢ normalizeAux x✝ (𝟙 a✝ ≫ f✝) = normalizeAux x✝ f✝
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: 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✝
x✝ : Path a a✝
⊢ normalizeAux x✝ f✝ = normalizeAux x✝ (𝟙 a✝ ≫ f✝)

Tactic:
;

Goal state after:
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✝
x✝ : Path a a✝
⊢ normalizeAux x✝ f✝ = normalizeAux x✝ (𝟙 a✝ ≫ f✝)
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: 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 ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
;

Goal state after:
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 ≫ (preinclusion B).map₂ (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c : FreeBicategory B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c),
    Quot.map (Hom₂.whisker_right i) ⋯ (η ≫ θ) =
      Quot.map (Hom₂.whisker_right i) ⋯ η ≫ Quot.map (Hom₂.whisker_right i) ⋯ θ

Tactic:
by
    rintro a b c f g h ⟨η⟩ ⟨θ⟩ i
    exact Quot.sound (Rel.comp_whisker_right i η θ)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: 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 ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
this : (normalizeIso (normalizeAux p f✝) h).hom = eqToHom ⋯ ≫ (normalizeIso (normalizeAux p g✝) h).hom ≫ eqToHom ⋯
⊢ (α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫ (preinclusion B).map₂ (eqToHom ⋯) ▷ 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) ≫
      eqToHom ⋯

Tactic:
;

Goal state after:
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 ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
this : (normalizeIso (normalizeAux p f✝) h).hom = eqToHom ⋯ ≫ (normalizeIso (normalizeAux p g✝) h).hom ≫ eqToHom ⋯
⊢ (α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫ (preinclusion B).map₂ (eqToHom ⋯) ▷ 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) ≫
      eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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 θ₂✝

Tactic:
;

Goal state after:
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 θ₂✝
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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 θ✝

Tactic:
;

Goal state after:
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 θ✝
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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 η✝

Tactic:
;

Goal state after:
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 η✝
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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 η✝

Tactic:
;

Goal state after:
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 η✝
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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 ι✝

Tactic:
;

Goal state after:
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 ι✝
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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 η'✝

Tactic:
;

Goal state after:
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 η'✝
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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✝)

Tactic:
;

Goal state after:
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✝)
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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 θ✝

Tactic:
;

Goal state after:
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 θ✝
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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

Tactic:
;

Goal state after:
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
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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

Tactic:
;

Goal state after:
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
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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✝

Tactic:
;

Goal state after:
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✝
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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✝)

Tactic:
;

Goal state after:
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✝)
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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✝

Tactic:
;

Goal state after:
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✝
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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

Tactic:
;

Goal state after:
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
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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

Tactic:
;

Goal state after:
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
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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

Tactic:
;

Goal state after:
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
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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 θ✝

Tactic:
;

Goal state after:
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 θ✝
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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✝)

Tactic:
;

Goal state after:
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✝)
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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✝)

Tactic:
;

Goal state after:
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✝)
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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✝)

Tactic:
;

Goal state after:
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✝)
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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✝)

Tactic:
;

Goal state after:
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✝)
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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✝))

Tactic:
;

Goal state after:
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✝))
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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✝)

Tactic:
;

Goal state after:
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✝)
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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

Tactic:
;

Goal state after:
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
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: 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✝

Tactic:
;

Goal state after:
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✝