mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map ((t.adj₂.counit.app ((𝟭 C).obj X) ≫ t.adj₁.unit.app X) ≫ G.map (t.adj₂.unit.app (F.obj X))) ≫
      t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map ((t.adj₂.counit.app ((𝟭 C).obj X) ≫ t.adj₁.unit.app X) ≫ G.map (t.adj₂.unit.app (F.obj X))) ≫
      t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X)) =
    t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (inv (t.adj₁.unit.app (G.obj X)))

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X)) =
    t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (inv (t.adj₁.unit.app (G.obj X)))
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
x✝ : Cᵒᵖ
⊢ (H.op.rightUnitor.inv ≫
          H.op.whiskerLeft t.op.adj₂.unit ≫
            (H.op.associator G.op F.op).inv ≫ inv (whiskerRight t.op.adj₁.unit F.op) ≫ F.op.leftUnitor.hom).app
      x✝ =
    (NatTrans.op
          (F.leftUnitor.inv ≫
            inv (whiskerRight t.adj₂.counit F) ≫
              (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom)).app
      x✝

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
x✝ : Cᵒᵖ
⊢ (H.op.rightUnitor.inv ≫
          H.op.whiskerLeft t.op.adj₂.unit ≫
            (H.op.associator G.op F.op).inv ≫ inv (whiskerRight t.op.adj₁.unit F.op) ≫ F.op.leftUnitor.hom).app
      x✝ =
    (NatTrans.op
          (F.leftUnitor.inv ≫
            inv (whiskerRight t.adj₂.counit F) ≫
              (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom)).app
      x✝
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
⊢ Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (X : C), Mono (t.leftToRight.app X)
X : D
⊢ Mono (t.leftToRight.app (G.obj X))

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (X : C), Mono (t.leftToRight.app X)
X : D
⊢ Mono (t.leftToRight.app (G.obj X))
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
X : C
⊢ Mono (t.adj₂.unit.app (F.obj X))

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
X : C
⊢ Mono (t.adj₂.unit.app (F.obj X))
Module: Mathlib.CategoryTheory.Bicategory.End

Goal state before:
pp: C : Type u
inst✝ : Bicategory C
X : C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : X ⟶ X
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ f₁✝ ▷ X₂✝ ≫ g₁✝ ▷ X₂✝ ≫ Z₁✝ ◁ f₂✝ ≫ Z₁✝ ◁ g₂✝ = f₁✝ ▷ X₂✝ ≫ g₁✝ ▷ X₂✝ ≫ Z₁✝ ◁ f₂✝ ≫ Z₁✝ ◁ g₂✝

Tactic:
]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f' ≫ g = f' ≫ g

Tactic:
]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f' ≫ g' = f' ≫ g'

Tactic:
]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ f ≫ g' = f ≫ g'

Tactic:
]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ f' ≫ g' = f' ≫ g'

Tactic:
]

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

Goal state before:
pp: 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 ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (η.vcomp θ) ≫ (normalizeIso p h✝).hom =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
| vcomp η θ ihf ihg =>

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

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

Tactic:
]

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

Goal state before:
pp: 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 (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (f.comp g✝) = (normalizeAux nil f).comp (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ (normalizeAux nil f).comp ((normalizeAux nil g).comp (normalizeAux nil g✝)) =
    (normalizeAux nil f).comp ((normalizeAux nil g).comp (normalizeAux nil g✝))

Tactic:
]

Goal state after:
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 (η✝.vcomp θ₁✝) = liftHom₂ F (η✝.vcomp θ₂✝)

Tactic:
(dsimp [liftHom₂]; cat_disch)

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

Goal state before:
pp: 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 ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map η

Tactic:
]

Goal state after:
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 ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map η
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 (η₁✝.vcomp θ✝) = liftHom₂ F (η₂✝.vcomp θ✝)

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 ((Hom₂.id f✝).vcomp η✝) = liftHom₂ F η✝

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 (η✝.vcomp (Hom₂.id g✝)) = liftHom₂ F η✝

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 ((η✝.vcomp θ✝).vcomp ι✝) = liftHom₂ F (η✝.vcomp (θ✝.vcomp ι✝))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 (Hom₂.whisker_left f✝ η✝) = liftHom₂ F (Hom₂.whisker_left f✝ η'✝)

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 (Hom₂.whisker_left f✝ (Hom₂.id g✝)) = liftHom₂ F (Hom₂.id (f✝.comp g✝))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 (Hom₂.whisker_left f✝ (η✝.vcomp θ✝)) =
    liftHom₂ F ((Hom₂.whisker_left f✝ η✝).vcomp (Hom₂.whisker_left f✝ θ✝))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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✝
⊢ liftHom₂ F (Hom₂.whisker_left (Hom.id a✝) η✝) =
    liftHom₂ F ((Hom₂.left_unitor f✝).vcomp (η✝.vcomp (Hom₂.left_unitor_inv g✝)))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 (Hom₂.whisker_left (f✝.comp g✝) η✝) =
    liftHom₂ F
      ((Hom₂.associator f✝ g✝ h✝).vcomp
        ((Hom₂.whisker_left f✝ (Hom₂.whisker_left g✝ η✝)).vcomp (Hom₂.associator_inv f✝ g✝ h'✝)))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 (Hom₂.whisker_right h✝ η✝) = liftHom₂ F (Hom₂.whisker_right h✝ η'✝)

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 (Hom₂.whisker_right g✝ (Hom₂.id f✝)) = liftHom₂ F (Hom₂.id (f✝.comp g✝))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 (Hom₂.whisker_right i✝ (η✝.vcomp θ✝)) =
    liftHom₂ F ((Hom₂.whisker_right i✝ η✝).vcomp (Hom₂.whisker_right i✝ θ✝))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 (Hom₂.whisker_right (Hom.id b✝) η✝) =
    liftHom₂ F ((Hom₂.right_unitor f✝).vcomp (η✝.vcomp (Hom₂.right_unitor_inv g✝)))

Tactic:
(dsimp [liftHom₂]; cat_disch)

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory 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 =
    StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory 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 =
    StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).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 (Hom₂.whisker_right (g✝.comp h✝) η✝) =
    liftHom₂ F
      ((Hom₂.associator_inv f✝ g✝ h✝).vcomp
        ((Hom₂.whisker_right h✝ (Hom₂.whisker_right g✝ η✝)).vcomp (Hom₂.associator f'✝ g✝ h✝)))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 (Hom₂.whisker_right h✝ (Hom₂.whisker_left f✝ η✝)) =
    liftHom₂ F
      ((Hom₂.associator f✝ g✝ h✝).vcomp
        ((Hom₂.whisker_left f✝ (Hom₂.whisker_right h✝ η✝)).vcomp (Hom₂.associator_inv f✝ g'✝ h✝)))

Tactic:
(dsimp [liftHom₂]; cat_disch)

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory 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:
]

Goal state after:
B : Type u
inst✝ : Bicategory 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
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 ((Hom₂.whisker_left f✝ θ✝).vcomp (Hom₂.whisker_right i✝ η✝)) =
    liftHom₂ F ((Hom₂.whisker_right h✝ η✝).vcomp (Hom₂.whisker_left g✝ θ✝))

Tactic:
(dsimp [liftHom₂]; cat_disch)

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory 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 =
    StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory 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 =
    StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom
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 ((Hom₂.associator f✝ g✝ h✝).vcomp (Hom₂.associator_inv f✝ g✝ h✝)) =
    liftHom₂ F (Hom₂.id ((f✝.comp g✝).comp h✝))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 ((Hom₂.associator_inv f✝ g✝ h✝).vcomp (Hom₂.associator f✝ g✝ h✝)) =
    liftHom₂ F (Hom₂.id (f✝.comp (g✝.comp h✝)))

Tactic:
(dsimp [liftHom₂]; cat_disch)

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
x : B
h : x ⟶ c
X✝ Y✝ : RightLift f g
η : X✝ ⟶ Y✝
⊢ (h ◁ η.left) ▷ f ≫ (α_ h Y✝.lift f).hom ≫ h ◁ Y✝.counit = (α_ h X✝.lift f).hom ≫ h ◁ (η.left ▷ f ≫ Y✝.counit)

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
x : B
h : x ⟶ c
X✝ Y✝ : RightLift f g
η : X✝ ⟶ Y✝
⊢ (h ◁ η.left) ▷ f ≫ (α_ h Y✝.lift f).hom ≫ h ◁ Y✝.counit = (α_ h X✝.lift f).hom ≫ h ◁ (η.left ▷ f ≫ Y✝.counit)
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 ((Hom₂.left_unitor f✝).vcomp (Hom₂.left_unitor_inv f✝)) = liftHom₂ F (Hom₂.id ((Hom.id a✝).comp f✝))

Tactic:
(dsimp [liftHom₂]; cat_disch)

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ (α_ h s.lift f).inv ≫ (postcomp x f).map (h ◁ i.left) ≫ CostructuredArrow.hom (t.whisker h) =
    (α_ h s.lift f).inv ≫ CostructuredArrow.hom (s.whisker h)

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ (α_ h s.lift f).inv ≫ (postcomp x f).map (h ◁ i.left) ≫ CostructuredArrow.hom (t.whisker h) =
    (α_ h s.lift f).inv ≫ CostructuredArrow.hom (s.whisker h)
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 ((Hom₂.left_unitor_inv f✝).vcomp (Hom₂.left_unitor f✝)) = liftHom₂ F (Hom₂.id f✝)

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
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 ((Hom₂.right_unitor f✝).vcomp (Hom₂.right_unitor_inv f✝)) = liftHom₂ F (Hom₂.id (f✝.comp (Hom.id b✝)))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after: