awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c d : FreeBicategory B
f : a ⟶ b
g g' : b ⟶ c
η_1 : g ⟶ g'
η : Hom₂ g g'
h : c ⟶ d
⊢ Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right h) ⋯
      (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left f) ⋯ (Quot.mk Rel η)) =
    CategoryStruct.comp (Y := f ≫ g ≫ h)
      (Iso.hom
        { hom := Quot.mk Rel (Hom₂.associator f g h), inv := Quot.mk Rel (Hom₂.associator_inv f g h), hom_inv_id := ⋯,
          inv_hom_id := ⋯ })
      (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left f) ⋯
          (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right h) ⋯ (Quot.mk Rel η)) ≫
        Iso.inv
          { hom := Quot.mk Rel (Hom₂.associator f g' h), inv := Quot.mk Rel (Hom₂.associator_inv f g' h),
            hom_inv_id := ⋯, inv_hom_id := ⋯ })

Tactic:
Quot.sound (Rel.whisker_assoc f η h)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, Quot.map, CategoryTheory.FreeBicategory.Rel.whisker_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c d : FreeBicategory B
f : a ⟶ b
g g' : b ⟶ c
η_1 : g ⟶ g'
η : Hom₂ g g'
h : c ⟶ d
⊢ Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right h) ⋯
      (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left f) ⋯ (Quot.mk Rel η)) =
    CategoryStruct.comp (Y := f ≫ g ≫ h)
      (Iso.hom
        { hom := Quot.mk Rel (Hom₂.associator f g h), inv := Quot.mk Rel (Hom₂.associator_inv f g h), hom_inv_id := ⋯,
          inv_hom_id := ⋯ })
      (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left f) ⋯
          (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right h) ⋯ (Quot.mk Rel η)) ≫
        Iso.inv
          { hom := Quot.mk Rel (Hom₂.associator f g' h), inv := Quot.mk Rel (Hom₂.associator_inv f g' h),
            hom_inv_id := ⋯, inv_hom_id := ⋯ })

Tactic:
exact Quot.sound (Rel.whisker_assoc f η h)

Premises used: Quot.sound, CategoryTheory.FreeBicategory.Rel.whisker_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : FreeBicategory B
f g : a ⟶ b
h i : b ⟶ c
η_1 : f ⟶ g
η : Hom₂ f g
θ_1 : h ⟶ i
θ : Hom₂ h i
⊢ Eq (α := f ≫ h ⟶ g ≫ i)
    (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left f) ⋯ (Quot.mk Rel θ) ≫
      Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right i) ⋯ (Quot.mk Rel η))
    (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right h) ⋯ (Quot.mk Rel η) ≫
      Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left g) ⋯ (Quot.mk Rel θ))

Tactic:
Quot.sound (Rel.whisker_exchange η θ)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, CategoryTheory.FreeBicategory.Rel.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : FreeBicategory B
f g : a ⟶ b
h i : b ⟶ c
η_1 : f ⟶ g
η : Hom₂ f g
θ_1 : h ⟶ i
θ : Hom₂ h i
⊢ Eq (α := f ≫ h ⟶ g ≫ i)
    (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left f) ⋯ (Quot.mk Rel θ) ≫
      Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right i) ⋯ (Quot.mk Rel η))
    (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right h) ⋯ (Quot.mk Rel η) ≫
      Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left g) ⋯ (Quot.mk Rel θ))

Tactic:
exact Quot.sound (Rel.whisker_exchange η θ)

Premises used: Quot.sound, CategoryTheory.FreeBicategory.Rel.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g h : a ⟶ b
η : Hom₂ f g
θ : Hom₂ g h
⊢ (η.vcomp θ).mk = η.mk ≫ θ.mk

Tactic:
rfl

Premises used: Quot.map₂, Quot.lift₂, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : Hom₂ g h
⊢ (Hom₂.whisker_left f η).mk = whiskerLeft (B := FreeBicategory B) (a := a) (b := b) (c := c) f (g := g) (h := h) η.mk

Tactic:
rfl

Premises used: Quot.map, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : FreeBicategory B
f g : a ⟶ b
η : Hom₂ f g
h : b ⟶ c
⊢ (Hom₂.whisker_right h η).mk = whiskerRight (B := FreeBicategory B) (a := a) (b := b) (c := c) (f := f) (g := g) η.mk h

Tactic:
rfl

Premises used: Quot.map, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a : FreeBicategory B
⊢ Eq (α := Hom.{v, u} a a) (Hom.id a) (𝟙 a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : FreeBicategory B
f : a ⟶ b
g : b ⟶ c
⊢ Hom.comp f g = f ≫ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f : a ⟶ b
⊢ Quot.mk Rel (Hom₂.id f) = 𝟙 f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c d : FreeBicategory B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ Eq (α := Quot (α := Hom₂.{v, u} (B := B) (a := a) (b := d) ((f ≫ g) ≫ h) (f ≫ g ≫ h)) Rel)
    (Quot.mk Rel (Hom₂.associator f g h))
    (Iso.hom (α_ (B := FreeBicategory B) (a := a) (b := b) (c := c) (d := d) f g h))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c d : FreeBicategory B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ Eq (α := Quot (α := Hom₂.{v, u} (B := B) (a := a) (b := d) (f ≫ g ≫ h) ((f ≫ g) ≫ h)) Rel)
    (Quot.mk Rel (Hom₂.associator_inv f g h))
    (Iso.inv (α_ (B := FreeBicategory B) (a := a) (b := b) (c := c) (d := d) f g h))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f : a ⟶ b
⊢ Eq (α := Quot (α := Hom₂ (𝟙 a ≫ f) f) Rel) (Quot.mk Rel (Hom₂.left_unitor f)) (Iso.hom (λ_ f))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f : a ⟶ b
⊢ Eq (α := Quot (α := Hom₂ f (𝟙 a ≫ f)) Rel) (Quot.mk Rel (Hom₂.left_unitor_inv f)) (Iso.inv (λ_ f))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f : a ⟶ b
⊢ Eq (α := Quot (α := Hom₂ (f ≫ 𝟙 b) f) Rel) (Quot.mk Rel (Hom₂.right_unitor f))
    (Iso.hom (ρ_ (B := FreeBicategory B) (a := a) (b := b) f))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f : a ⟶ b
⊢ Eq (α := Quot (α := Hom₂ f (f ≫ 𝟙 b)) Rel) (Quot.mk Rel (Hom₂.right_unitor_inv f))
    (Iso.inv (ρ_ (B := FreeBicategory B) (a := a) (b := b) f))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : CategoryStruct.{v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a : FreeBicategory B
⊢ liftHom F (𝟙 a) = 𝟙 (F.obj a)

Tactic:
rfl

Premises used: CategoryTheory.FreeBicategory.liftHom, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : CategoryStruct.{v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b c : FreeBicategory B
f : a ⟶ b
g : b ⟶ c
⊢ liftHom F (f ≫ g) = liftHom F f ≫ liftHom F g

Tactic:
rfl

Premises used: CategoryTheory.FreeBicategory.liftHom, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 h : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
θ₁ θ₂ : Hom₂ g_1 h
h_1 : Rel θ₁ θ₂
a_ih : liftHom₂ F θ₁ = liftHom₂ F θ₂
vcomp_right : liftHom₂ F η_1 ≫ liftHom₂ F θ₁ = liftHom₂ F η_1 ≫ liftHom₂ F θ₂
⊢ liftHom₂ F (η_1.vcomp θ₁) = liftHom₂ F (η_1.vcomp θ₂)

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 h : Hom.{v₁, u₁} a_1 b_1
η₁ η₂ : Hom₂ f_1 g_1
θ_1 : Hom₂ g_1 h
h_1 : Rel η₁ η₂
a_ih : liftHom₂ F η₁ = liftHom₂ F η₂
vcomp_left : liftHom₂ F η₁ ≫ liftHom₂ F θ_1 = liftHom₂ F η₂ ≫ liftHom₂ F θ_1
⊢ liftHom₂ F (η₁.vcomp θ_1) = liftHom₂ F (η₂.vcomp θ_1)

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
id_comp : 𝟙 (liftHom F f_1) ≫ liftHom₂ F η_1 = liftHom₂ F η_1
⊢ liftHom₂ F ((Hom₂.id f_1).vcomp η_1) = liftHom₂ F η_1

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
comp_id : liftHom₂ F η_1 ≫ 𝟙 (liftHom F g_1) = liftHom₂ F η_1
⊢ liftHom₂ F (η_1.vcomp (Hom₂.id g_1)) = liftHom₂ F η_1

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 h i : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
θ_1 : Hom₂ g_1 h
ι : Hom₂ h i
assoc : (liftHom₂ F η_1 ≫ liftHom₂ F θ_1) ≫ liftHom₂ F ι = liftHom₂ F η_1 ≫ liftHom₂ F θ_1 ≫ liftHom₂ F ι
⊢ liftHom₂ F ((η_1.vcomp θ_1).vcomp ι) = liftHom₂ F (η_1.vcomp (θ_1.vcomp ι))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 h : Hom.{v₁, u₁} b_1 c
η_1 η' : Hom₂ g_1 h
h_1 : Rel η_1 η'
a_ih : liftHom₂ F η_1 = liftHom₂ F η'
whisker_left : liftHom F f_1 ◁ liftHom₂ F η_1 = liftHom F f_1 ◁ liftHom₂ F η'
⊢ liftHom₂ F (Hom₂.whisker_left f_1 η_1) = liftHom₂ F (Hom₂.whisker_left f_1 η')

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
whisker_left_id : liftHom F f_1 ◁ 𝟙 (liftHom F g_1) = 𝟙 (liftHom F f_1 ≫ liftHom F g_1)
⊢ liftHom₂ F (Hom₂.whisker_left f_1 (Hom₂.id g_1)) = liftHom₂ F (Hom₂.id (f_1.comp g_1))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 h i : Hom.{v₁, u₁} b_1 c
η_1 : Hom₂ g_1 h
θ_1 : Hom₂ h i
whisker_left_comp :
  liftHom F f_1 ◁ (liftHom₂ F η_1 ≫ liftHom₂ F θ_1) = liftHom F f_1 ◁ liftHom₂ F η_1 ≫ liftHom F f_1 ◁ liftHom₂ F θ_1
⊢ liftHom₂ F (Hom₂.whisker_left f_1 (η_1.vcomp θ_1)) =
    liftHom₂ F ((Hom₂.whisker_left f_1 η_1).vcomp (Hom₂.whisker_left f_1 θ_1))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
id_whisker_left : 𝟙 (F.obj a_1) ◁ liftHom₂ F η_1 = (λ_ (liftHom F f_1)).hom ≫ liftHom₂ F η_1 ≫ (λ_ (liftHom F g_1)).inv
⊢ liftHom₂ F (Hom₂.whisker_left (Hom.id a_1) η_1) =
    liftHom₂ F ((Hom₂.left_unitor f_1).vcomp (η_1.vcomp (Hom₂.left_unitor_inv g_1)))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
h h' : Hom.{v₁, u₁} c d
η_1 : Hom₂ h h'
comp_whisker_left :
  (liftHom F f_1 ≫ liftHom F g_1) ◁ liftHom₂ F η_1 =
    (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).hom ≫
      liftHom F f_1 ◁ liftHom F g_1 ◁ liftHom₂ F η_1 ≫ (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h')).inv
⊢ liftHom₂ F (Hom₂.whisker_left (f_1.comp g_1) η_1) =
    liftHom₂ F
      ((Hom₂.associator f_1 g_1 h).vcomp
        ((Hom₂.whisker_left f_1 (Hom₂.whisker_left g_1 η_1)).vcomp (Hom₂.associator_inv f_1 g_1 h')))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
h : Hom.{v₁, u₁} b_1 c
η_1 η' : Hom₂ f_1 g_1
h_1 : Rel η_1 η'
a_ih : liftHom₂ F η_1 = liftHom₂ F η'
whisker_right : liftHom₂ F η_1 ▷ liftHom F h = liftHom₂ F η' ▷ liftHom F h
⊢ liftHom₂ F (Hom₂.whisker_right h η_1) = liftHom₂ F (Hom₂.whisker_right h η')

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
id_whisker_right : 𝟙 (liftHom F f_1) ▷ liftHom F g_1 = 𝟙 (liftHom F f_1 ≫ liftHom F g_1)
⊢ liftHom₂ F (Hom₂.whisker_right g_1 (Hom₂.id f_1)) = liftHom₂ F (Hom₂.id (f_1.comp g_1))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 g_1 h : Hom.{v₁, u₁} a_1 b_1
i : Hom.{v₁, u₁} b_1 c
η_1 : Hom₂ f_1 g_1
θ_1 : Hom₂ g_1 h
comp_whisker_right :
  (liftHom₂ F η_1 ≫ liftHom₂ F θ_1) ▷ liftHom F i = liftHom₂ F η_1 ▷ liftHom F i ≫ liftHom₂ F θ_1 ▷ liftHom F i
⊢ liftHom₂ F (Hom₂.whisker_right i (η_1.vcomp θ_1)) =
    liftHom₂ F ((Hom₂.whisker_right i η_1).vcomp (Hom₂.whisker_right i θ_1))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
whisker_right_id : liftHom₂ F η_1 ▷ 𝟙 (F.obj b_1) = (ρ_ (liftHom F f_1)).hom ≫ liftHom₂ F η_1 ≫ (ρ_ (liftHom F g_1)).inv
⊢ liftHom₂ F (Hom₂.whisker_right (Hom.id b_1) η_1) =
    liftHom₂ F ((Hom₂.right_unitor f_1).vcomp (η_1.vcomp (Hom₂.right_unitor_inv g_1)))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d : B
f_1 f' : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
h : Hom.{v₁, u₁} c d
η_1 : Hom₂ f_1 f'
whisker_right_comp :
  liftHom₂ F η_1 ▷ (liftHom F g_1 ≫ liftHom F h) =
    (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).inv ≫
      liftHom₂ F η_1 ▷ liftHom F g_1 ▷ liftHom F h ≫ (α_ (liftHom F f') (liftHom F g_1) (liftHom F h)).hom
⊢ liftHom₂ F (Hom₂.whisker_right (g_1.comp h) η_1) =
    liftHom₂ F
      ((Hom₂.associator_inv f_1 g_1 h).vcomp
        ((Hom₂.whisker_right h (Hom₂.whisker_right g_1 η_1)).vcomp (Hom₂.associator f' g_1 h)))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 g' : Hom.{v₁, u₁} b_1 c
η_1 : Hom₂ g_1 g'
h : Hom.{v₁, u₁} c d
whisker_assoc :
  (liftHom F f_1 ◁ liftHom₂ F η_1) ▷ liftHom F h =
    (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).hom ≫
      liftHom F f_1 ◁ liftHom₂ F η_1 ▷ liftHom F h ≫ (α_ (liftHom F f_1) (liftHom F g') (liftHom F h)).inv
⊢ liftHom₂ F (Hom₂.whisker_right h (Hom₂.whisker_left f_1 η_1)) =
    liftHom₂ F
      ((Hom₂.associator f_1 g_1 h).vcomp
        ((Hom₂.whisker_left f_1 (Hom₂.whisker_right h η_1)).vcomp (Hom₂.associator_inv f_1 g' h)))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
h i : Hom.{v₁, u₁} b_1 c
η_1 : Hom₂ f_1 g_1
θ_1 : Hom₂ h i
whisker_exchange :
  liftHom F f_1 ◁ liftHom₂ F θ_1 ≫ liftHom₂ F η_1 ▷ liftHom F i =
    liftHom₂ F η_1 ▷ liftHom F h ≫ liftHom F g_1 ◁ liftHom₂ F θ_1
⊢ liftHom₂ F ((Hom₂.whisker_left f_1 θ_1).vcomp (Hom₂.whisker_right i η_1)) =
    liftHom₂ F ((Hom₂.whisker_right h η_1).vcomp (Hom₂.whisker_left g_1 θ_1))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
h : Hom.{v₁, u₁} c d
associator_hom_inv :
  (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).hom ≫ (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).inv =
    𝟙 ((liftHom F f_1 ≫ liftHom F g_1) ≫ liftHom F h)
⊢ liftHom₂ F ((Hom₂.associator f_1 g_1 h).vcomp (Hom₂.associator_inv f_1 g_1 h)) =
    liftHom₂ F (Hom₂.id ((f_1.comp g_1).comp h))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
h : Hom.{v₁, u₁} c d
associator_inv_hom :
  (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).inv ≫ (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).hom =
    𝟙 (liftHom F f_1 ≫ liftHom F g_1 ≫ liftHom F h)
⊢ liftHom₂ F ((Hom₂.associator_inv f_1 g_1 h).vcomp (Hom₂.associator f_1 g_1 h)) =
    liftHom₂ F (Hom₂.id (f_1.comp (g_1.comp h)))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 : Hom.{v₁, u₁} a_1 b_1
left_unitor_hom_inv : (λ_ (liftHom F f_1)).hom ≫ (λ_ (liftHom F f_1)).inv = 𝟙 (𝟙 (F.obj a_1) ≫ liftHom F f_1)
⊢ liftHom₂ F ((Hom₂.left_unitor f_1).vcomp (Hom₂.left_unitor_inv f_1)) =
    liftHom₂ F (Hom₂.id (Hom.comp (Hom.id a_1) f_1))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 : Hom.{v₁, u₁} a_1 b_1
left_unitor_inv_hom : (λ_ (liftHom F f_1)).inv ≫ (λ_ (liftHom F f_1)).hom = 𝟙 (liftHom F f_1)
⊢ liftHom₂ F ((Hom₂.left_unitor_inv f_1).vcomp (Hom₂.left_unitor f_1)) = liftHom₂ F (Hom₂.id f_1)

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 : Hom.{v₁, u₁} a_1 b_1
right_unitor_hom_inv : (ρ_ (liftHom F f_1)).hom ≫ (ρ_ (liftHom F f_1)).inv = 𝟙 (liftHom F f_1 ≫ 𝟙 (F.obj b_1))
⊢ liftHom₂ F ((Hom₂.right_unitor f_1).vcomp (Hom₂.right_unitor_inv f_1)) = liftHom₂ F (Hom₂.id (f_1.comp (Hom.id b_1)))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 : Hom.{v₁, u₁} a_1 b_1
right_unitor_inv_hom : (ρ_ (liftHom F f_1)).inv ≫ (ρ_ (liftHom F f_1)).hom = 𝟙 (liftHom F f_1)
⊢ liftHom₂ F ((Hom₂.right_unitor_inv f_1).vcomp (Hom₂.right_unitor f_1)) = liftHom₂ F (Hom₂.id f_1)

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d e : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
h : Hom.{v₁, u₁} c d
i : Hom.{v₁, u₁} d e
pentagon :
  (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).hom ▷ liftHom F i ≫
      (α_ (liftHom F f_1) (liftHom F g_1 ≫ liftHom F h) (liftHom F i)).hom ≫
        liftHom F f_1 ◁ (α_ (liftHom F g_1) (liftHom F h) (liftHom F i)).hom =
    (α_ (liftHom F f_1 ≫ liftHom F g_1) (liftHom F h) (liftHom F i)).hom ≫
      (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h ≫ liftHom F i)).hom
⊢ liftHom₂ F
      ((Hom₂.whisker_right i (Hom₂.associator f_1 g_1 h)).vcomp
        ((Hom₂.associator f_1 (g_1.comp h) i).vcomp (Hom₂.whisker_left f_1 (Hom₂.associator g_1 h i)))) =
    liftHom₂ F ((Hom₂.associator (f_1.comp g_1) h i).vcomp (Hom₂.associator f_1 g_1 (h.comp i)))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
triangle :
  (α_ (liftHom F f_1) (𝟙 (F.obj b_1)) (liftHom F g_1)).hom ≫ liftHom F f_1 ◁ (λ_ (liftHom F g_1)).hom =
    (ρ_ (liftHom F f_1)).hom ▷ liftHom F g_1
⊢ liftHom₂ F ((Hom₂.associator f_1 (Hom.id b_1) g_1).vcomp (Hom₂.whisker_left f_1 (Hom₂.left_unitor g_1))) =
    liftHom₂ F (Hom₂.whisker_right g_1 (Hom₂.right_unitor f_1))

Tactic:
dsimp [liftHom₂]

Premises used: CategoryTheory.FreeBicategory.liftHom₂