awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
rw :
  (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
    StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv
⊢ StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h) =
    StructuredArrow.hom (t.whisker h)

Tactic:
rw [← cancel_mono (α_ _ _ _).inv]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Bicategory.associator, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
⊢ (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
    (s.unit ≫ f ◁ StructuredArrow.Hom.right i) ▷ h

Tactic:
simp [-LeftExtension.w]

Premises used: CategoryTheory.Bicategory.LeftExtension.w
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
⊢ (s.unit ≫ f ◁ StructuredArrow.Hom.right i) ▷ h = t.unit ▷ h

Tactic:
congrArg (· ▷ h) (LeftExtension.w i)

Premises used: congrArg, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.Bicategory.LeftExtension.w
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
⊢ t.unit ▷ h = StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
_ :
  (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
    (s.unit ≫ f ◁ StructuredArrow.Hom.right i) ▷ h
_₁ : t.unit ▷ h = StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv
⊢ (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
    StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv

Tactic:
calc
      _ = (unit s ≫ f ◁ i.right) ▷ h := by simp [-LeftExtension.w]
      _ = unit t ▷ h := congrArg (· ▷ h) (LeftExtension.w i)
      _ = _ := by simp

Premises used: congrArg, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.Bicategory.LeftExtension.unit, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.Bicategory.LeftExtension.w, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ≅ t
x : B
h : c ⟶ x
⊢ StructuredArrow.Hom.right (whiskerHom i.hom h ≫ whiskerHom i.inv h) = StructuredArrow.Hom.right (i.hom ≫ i.inv) ▷ h

Tactic:
simp [-Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ≅ t
x : B
h : c ⟶ x
⊢ StructuredArrow.Hom.right (i.hom ≫ i.inv) ▷ h = 𝟙 (StructuredArrow.right s ≫ h)

Tactic:
simp [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ≅ t
x : B
h : c ⟶ x
⊢ StructuredArrow.Hom.right (whiskerHom i.inv h ≫ whiskerHom i.hom h) = StructuredArrow.Hom.right (i.inv ≫ i.hom) ▷ h

Tactic:
simp [-Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ≅ t
x : B
h : c ⟶ x
⊢ StructuredArrow.Hom.right (i.inv ≫ i.hom) ▷ h = 𝟙 (StructuredArrow.right t ≫ h)

Tactic:
simp [Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
h : s ⟶ t
⊢ s.unit ≫ StructuredArrow.Hom.right h ▷ f = t.unit

Tactic:
StructuredArrow.w h

Premises used: CategoryTheory.StructuredArrow.w
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
t : LeftLift f g
x : B
h : x ⟶ c
⊢ (t.whisker h).lift = h ≫ t.lift

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
t : LeftLift f g
x : B
h : x ⟶ c
⊢ (t.whisker h).unit = h ◁ t.unit ≫ (α_ h t.lift f).inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
x : B
h : x ⟶ c
X Y : LeftLift f g
η : X ⟶ Y
dsimp : (h ◁ X.unit ≫ (α_ h X.lift f).inv) ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f = h ◁ Y.unit ≫ (α_ h Y.lift f).inv
⊢ (X.whisker h).unit ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f = (Y.whisker h).unit

Tactic:
dsimp only [whisker_lift, whisker_unit]

Premises used: CategoryTheory.Bicategory.LeftLift.whisker_unit, CategoryTheory.Bicategory.LeftLift.whisker_lift
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
x : B
h : x ⟶ c
X Y : LeftLift f g
η : X ⟶ Y
rw :
  (h ◁ X.unit ≫ (α_ h X.lift f).inv) ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f =
    h ◁ (X.unit ≫ StructuredArrow.Hom.right η ▷ f) ≫ (α_ h Y.lift f).inv
⊢ (h ◁ X.unit ≫ (α_ h X.lift f).inv) ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f = h ◁ Y.unit ≫ (α_ h Y.lift f).inv

Tactic:
rw [← LeftLift.w η]

Premises used: CategoryTheory.Bicategory.LeftLift.w
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
x : B
h : x ⟶ c
X Y : LeftLift f g
η : X ⟶ Y
⊢ (h ◁ X.unit ≫ (α_ h X.lift f).inv) ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f =
    h ◁ (X.unit ≫ StructuredArrow.Hom.right η ▷ f) ≫ (α_ h Y.lift f).inv

Tactic:
simp [-LeftLift.w]

Premises used: CategoryTheory.Bicategory.LeftLift.w
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ⟶ t
x : B
h : x ⟶ c
rw :
  (StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i)) ≫ (α_ h t.lift f).hom =
    StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom
⊢ StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i) =
    StructuredArrow.hom (t.whisker h)

Tactic:
rw [← cancel_mono (α_ h _ _).hom]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Bicategory.associator, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ (StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i)) ≫ (α_ h t.lift f).hom =
    h ◁ (s.unit ≫ StructuredArrow.Hom.right i ▷ f)

Tactic:
simp [-LeftLift.w]

Premises used: CategoryTheory.Bicategory.LeftLift.w
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ h ◁ (s.unit ≫ StructuredArrow.Hom.right i ▷ f) = h ◁ t.unit

Tactic:
congrArg (h ◁ ·) (LeftLift.w i)

Premises used: congrArg, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.Bicategory.LeftLift.w
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ h ◁ t.unit = StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ⟶ t
x : B
h : x ⟶ c
_ :
  (StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i)) ≫ (α_ h t.lift f).hom =
    h ◁ (s.unit ≫ StructuredArrow.Hom.right i ▷ f)
_₁ : h ◁ t.unit = StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom
⊢ (StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i)) ≫ (α_ h t.lift f).hom =
    StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom

Tactic:
calc
      _ = h ◁ (unit s ≫ i.right ▷ f) := by simp [-LeftLift.w]
      _ = h ◁ unit t := congrArg (h ◁ ·) (LeftLift.w i)
      _ = _ := by simp

Premises used: congrArg, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.LeftLift.unit, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.StructuredArrow.Hom.right, CategoryTheory.Bicategory.LeftLift.w
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ StructuredArrow.Hom.right (whiskerHom i.hom h ≫ whiskerHom i.inv h) = h ◁ StructuredArrow.Hom.right (i.hom ≫ i.inv)

Tactic:
simp [-Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ h ◁ StructuredArrow.Hom.right (i.hom ≫ i.inv) = 𝟙 (h ≫ StructuredArrow.right s)

Tactic:
simp [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ StructuredArrow.Hom.right (whiskerHom i.inv h ≫ whiskerHom i.hom h) = h ◁ StructuredArrow.Hom.right (i.inv ≫ i.hom)

Tactic:
simp [-Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ h ◁ StructuredArrow.Hom.right (i.inv ≫ i.hom) = 𝟙 (h ≫ StructuredArrow.right t)

Tactic:
simp [Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : RightExtension f g
η : s ⟶ t
⊢ f ◁ η.left ≫ t.counit = s.counit

Tactic:
CostructuredArrow.w η

Premises used: CategoryTheory.CostructuredArrow.w
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
h : s ⟶ t
⊢ h.left ▷ f ≫ t.counit = s.counit

Tactic:
CostructuredArrow.w h

Premises used: CategoryTheory.CostructuredArrow.w
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
h : Inhabited B
⊢ Inhabited (FreeBicategory B)

Tactic:
exact id h

Premises used: id
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
f_1 : Quot (α := Hom₂ f g) Rel
η : Hom₂ f g
⊢ Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel (Hom₂.id f)) (Quot.mk Rel η) = Quot.mk Rel η

Tactic:
Quot.sound (Rel.id_comp η)

Premises used: CategoryTheory.FreeBicategory.Rel.id_comp, Quot.sound, Quot.map₂, Quot.lift₂
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
f_1 : Quot (α := Hom₂ f g) Rel
η : Hom₂ f g
⊢ Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel (Hom₂.id f)) (Quot.mk Rel η) = Quot.mk Rel η

Tactic:
exact Quot.sound (Rel.id_comp η)

Premises used: CategoryTheory.FreeBicategory.Rel.id_comp, Quot.sound
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
f_1 : Quot (α := Hom₂ f g) Rel
η : Hom₂ f g
⊢ Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel η) (Quot.mk Rel (Hom₂.id g)) = Quot.mk Rel η

Tactic:
Quot.sound (Rel.comp_id η)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, CategoryTheory.FreeBicategory.Rel.comp_id
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
f_1 : Quot (α := Hom₂ f g) Rel
η : Hom₂ f g
⊢ Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel η) (Quot.mk Rel (Hom₂.id g)) = Quot.mk Rel η

Tactic:
exact Quot.sound (Rel.comp_id η)

Premises used: Quot.sound, CategoryTheory.FreeBicategory.Rel.comp_id
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g h i : a ⟶ b
f_1 : Quot (α := Hom₂ f g) Rel
η : Hom₂ f g
g_1 : Quot (α := Hom₂ g h) Rel
θ : Hom₂ g h
h_1 : Quot (α := Hom₂ h i) Rel
ι : Hom₂ h i
⊢ Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯
      (Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel η) (Quot.mk Rel θ)) (Quot.mk Rel ι) =
    Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel η)
      (Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel θ) (Quot.mk Rel ι))

Tactic:
Quot.sound (Rel.assoc η θ ι)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, CategoryTheory.FreeBicategory.Rel.assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g h i : a ⟶ b
f_1 : Quot (α := Hom₂ f g) Rel
η : Hom₂ f g
g_1 : Quot (α := Hom₂ g h) Rel
θ : Hom₂ g h
h_1 : Quot (α := Hom₂ h i) Rel
ι : Hom₂ h i
⊢ Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯
      (Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel η) (Quot.mk Rel θ)) (Quot.mk Rel ι) =
    Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel η)
      (Quot.map₂ (r := Rel) (s := Rel) (t := Rel) Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel θ) (Quot.mk Rel ι))

Tactic:
exact Quot.sound (Rel.assoc η θ ι)

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

Tactic:
Quot.sound (Rel.whisker_left_comp f η θ)

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

Tactic:
exact Quot.sound (Rel.whisker_left_comp f η θ)

Premises used: Quot.sound, CategoryTheory.FreeBicategory.Rel.whisker_left_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
η_1 : f ⟶ g
η : Hom₂ f g
⊢ Eq (α := 𝟙 a ≫ f ⟶ 𝟙 a ≫ g) (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left (𝟙 a)) ⋯ (Quot.mk Rel η))
    (CategoryStruct.comp (Y := f)
      (Iso.hom
        { hom := Quot.mk Rel (Hom₂.left_unitor f), inv := Quot.mk Rel (Hom₂.left_unitor_inv f), hom_inv_id := ⋯,
          inv_hom_id := ⋯ })
      (Quot.mk Rel η ≫
        Iso.inv
          { hom := Quot.mk Rel (Hom₂.left_unitor g), inv := Quot.mk Rel (Hom₂.left_unitor_inv g), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }))

Tactic:
Quot.sound (Rel.id_whisker_left η)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, CategoryTheory.FreeBicategory.Rel.id_whisker_left, Quot.map
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
η_1 : f ⟶ g
η : Hom₂ f g
⊢ Eq (α := 𝟙 a ≫ f ⟶ 𝟙 a ≫ g) (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left (𝟙 a)) ⋯ (Quot.mk Rel η))
    (CategoryStruct.comp (Y := f)
      (Iso.hom
        { hom := Quot.mk Rel (Hom₂.left_unitor f), inv := Quot.mk Rel (Hom₂.left_unitor_inv f), hom_inv_id := ⋯,
          inv_hom_id := ⋯ })
      (Quot.mk Rel η ≫
        Iso.inv
          { hom := Quot.mk Rel (Hom₂.left_unitor g), inv := Quot.mk Rel (Hom₂.left_unitor_inv g), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }))

Tactic:
exact Quot.sound (Rel.id_whisker_left η)

Premises used: Quot.sound, CategoryTheory.FreeBicategory.Rel.id_whisker_left
-- 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 h' : c ⟶ d
η_1 : h ⟶ h'
η : Hom₂ h h'
⊢ Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left (f ≫ g)) ⋯ (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_left g) ⋯ (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.comp_whisker_left f g η)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, CategoryTheory.FreeBicategory.Rel.comp_whisker_left, Quot.map
-- 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 h' : c ⟶ d
η_1 : h ⟶ h'
η : Hom₂ h h'
⊢ Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_left (f ≫ g)) ⋯ (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_left g) ⋯ (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.comp_whisker_left f g η)

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

Tactic:
Quot.sound (Rel.comp_whisker_right i η θ)

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

Tactic:
exact Quot.sound (Rel.comp_whisker_right i η θ)

Premises used: Quot.sound, CategoryTheory.FreeBicategory.Rel.comp_whisker_right
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
η_1 : f ⟶ g
η : Hom₂ f g
⊢ Eq (α := f ≫ 𝟙 b ⟶ g ≫ 𝟙 b) (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right (𝟙 b)) ⋯ (Quot.mk Rel η))
    (CategoryStruct.comp (Y := f)
      (Iso.hom
        { hom := Quot.mk Rel (Hom₂.right_unitor f), inv := Quot.mk Rel (Hom₂.right_unitor_inv f), hom_inv_id := ⋯,
          inv_hom_id := ⋯ })
      (Quot.mk Rel η ≫
        Iso.inv
          { hom := Quot.mk Rel (Hom₂.right_unitor g), inv := Quot.mk Rel (Hom₂.right_unitor_inv g), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }))

Tactic:
Quot.sound (Rel.whisker_right_id η)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, CategoryTheory.FreeBicategory.Rel.whisker_right_id, Quot.map
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
η_1 : f ⟶ g
η : Hom₂ f g
⊢ Eq (α := f ≫ 𝟙 b ⟶ g ≫ 𝟙 b) (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right (𝟙 b)) ⋯ (Quot.mk Rel η))
    (CategoryStruct.comp (Y := f)
      (Iso.hom
        { hom := Quot.mk Rel (Hom₂.right_unitor f), inv := Quot.mk Rel (Hom₂.right_unitor_inv f), hom_inv_id := ⋯,
          inv_hom_id := ⋯ })
      (Quot.mk Rel η ≫
        Iso.inv
          { hom := Quot.mk Rel (Hom₂.right_unitor g), inv := Quot.mk Rel (Hom₂.right_unitor_inv g), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }))

Tactic:
exact Quot.sound (Rel.whisker_right_id η)

Premises used: Quot.sound, CategoryTheory.FreeBicategory.Rel.whisker_right_id
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c d : FreeBicategory B
f f' : a ⟶ b
η_1 : f ⟶ f'
η : Hom₂ f f'
g : b ⟶ c
h : c ⟶ d
⊢ Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right (g ≫ h)) ⋯ (Quot.mk Rel η) =
    CategoryStruct.comp (Y := (f ≫ g) ≫ h)
      (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 := ⋯ })
      (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right h) ⋯
          (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right g) ⋯ (Quot.mk Rel η)) ≫
        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 := ⋯ })

Tactic:
Quot.sound (Rel.whisker_right_comp g h η)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, Quot.map, CategoryTheory.FreeBicategory.Rel.whisker_right_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Free
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c d : FreeBicategory B
f f' : a ⟶ b
η_1 : f ⟶ f'
η : Hom₂ f f'
g : b ⟶ c
h : c ⟶ d
⊢ Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right (g ≫ h)) ⋯ (Quot.mk Rel η) =
    CategoryStruct.comp (Y := (f ≫ g) ≫ h)
      (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 := ⋯ })
      (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right h) ⋯
          (Quot.map (ra := Rel) (rb := Rel) (Hom₂.whisker_right g) ⋯ (Quot.mk Rel η)) ≫
        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 := ⋯ })

Tactic:
exact Quot.sound (Rel.whisker_right_comp g h η)

Premises used: Quot.sound, CategoryTheory.FreeBicategory.Rel.whisker_right_comp