mathlib-initiative/mathlib-tactics huggingface dataset:
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₂]

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 (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₂]

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

Tactic:
dsimp [liftHom₂]

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

Tactic:
dsimp [liftHom₂]

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

Tactic:
dsimp [liftHom₂]

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

Tactic:
dsimp [liftHom₂]

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 (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₂]

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 (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₂]

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 ((Hom₂.whisker_left f✝ θ✝).vcomp (Hom₂.whisker_right i✝ η✝)) =
    liftHom₂ F ((Hom₂.whisker_right h✝ η✝).vcomp (Hom₂.whisker_left g✝ θ✝))

Tactic:
dsimp [liftHom₂]

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

Tactic:
dsimp [liftHom₂]

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

Tactic:
dsimp [liftHom₂]

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 ((Hom₂.left_unitor f✝).vcomp (Hom₂.left_unitor_inv f✝)) = liftHom₂ F (Hom₂.id ((Hom.id a✝).comp f✝))

Tactic:
dsimp [liftHom₂]

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 ((Hom₂.left_unitor_inv f✝).vcomp (Hom₂.left_unitor f✝)) = liftHom₂ F (Hom₂.id f✝)

Tactic:
dsimp [liftHom₂]

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

Tactic:
dsimp [liftHom₂]

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 ((Hom₂.right_unitor_inv f✝).vcomp (Hom₂.right_unitor f✝)) = liftHom₂ F (Hom₂.id f✝)

Tactic:
dsimp [liftHom₂]

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
      ((Hom₂.whisker_right i✝ (Hom₂.associator f✝ g✝ h✝)).vcomp
        ((Hom₂.associator f✝ (g✝.comp h✝) i✝).vcomp (Hom₂.whisker_left f✝ (Hom₂.associator g✝ h✝ i✝)))) =
    liftHom₂ F ((Hom₂.associator (f✝.comp g✝) h✝ i✝).vcomp (Hom₂.associator f✝ g✝ (h✝.comp i✝)))

Tactic:
dsimp [liftHom₂]

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 ((Hom₂.associator f✝ (Hom.id b✝) g✝).vcomp (Hom₂.whisker_left f✝ (Hom₂.left_unitor g✝))) =
    liftHom₂ F (Hom₂.whisker_right g✝ (Hom₂.right_unitor f✝))

Tactic:
dsimp [liftHom₂]

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✝
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
g : a ⟶ b
base✝ : a.base ⟶ b.base
fiber✝ : (F.map base✝.toLoc).toFunctor.obj a.fiber ⟶ b.fiber
hfg₁ : { base := base✝, fiber := fiber✝ }.base = g.base
hfg₂ : eqToHom ⋯ ≫ { base := base✝, fiber := fiber✝ }.fiber = g.fiber
⊢ { base := base✝, fiber := fiber✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : (F.map base✝¹.toLoc).toFunctor.obj a.fiber ⟶ b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : (F.map base✝.toLoc).toFunctor.obj a.fiber ⟶ b.fiber
hfg₁ : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
hfg₂ : eqToHom ⋯ ≫ { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
g : a ⟶ b
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).toFunctor.obj b.fiber
hfg₁ : { base := base✝, fiber := fiber✝ }.base = g.base
hfg₂ : { base := base✝, fiber := fiber✝ }.fiber = g.fiber ≫ eqToHom ⋯
⊢ { base := base✝, fiber := fiber✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).toFunctor.obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).toFunctor.obj b.fiber
hfg₁ : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }
Module: Mathlib.CategoryTheory.Bicategory.Span.Basic

Goal state before:
pp: case mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Wₗ Wᵣ : MorphismProperty C
c c' : C
S S' : Span Wₗ Wᵣ c c'
g : S ⟶ S'
hom✝ : S.apex ⟶ S'.apex
hom_l✝ : hom✝ ≫ S'.l = S.l
hom_r✝ : hom✝ ≫ S'.r = S.r
h : { hom := hom✝, hom_l := hom_l✝, hom_r := hom_r✝ }.hom = g.hom
⊢ { hom := hom✝, hom_l := hom_l✝, hom_r := hom_r✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Wₗ Wᵣ : MorphismProperty C
c c' : C
S S' : Span Wₗ Wᵣ c c'
hom✝¹ : S.apex ⟶ S'.apex
hom_l✝¹ : hom✝¹ ≫ S'.l = S.l
hom_r✝¹ : hom✝¹ ≫ S'.r = S.r
hom✝ : S.apex ⟶ S'.apex
hom_l✝ : hom✝ ≫ S'.l = S.l
hom_r✝ : hom✝ ≫ S'.r = S.r
h : { hom := hom✝¹, hom_l := hom_l✝¹, hom_r := hom_r✝¹ }.hom = { hom := hom✝, hom_l := hom_l✝, hom_r := hom_r✝ }.hom
⊢ { hom := hom✝¹, hom_l := hom_l✝¹, hom_r := hom_r✝¹ } = { hom := hom✝, hom_l := hom_l✝, hom_r := hom_r✝ }
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case ofRel
X Y : RelCat
g : X ⟶ Y
rel✝ : SetRel X Y
h : { rel := rel✝ }.rel = g.rel
⊢ { rel := rel✝ } = g

Tactic:
cases g

Goal state after:
case ofRel.ofRel
X Y : RelCat
rel✝¹ rel✝ : SetRel X Y
h : { rel := rel✝¹ }.rel = { rel := rel✝ }.rel
⊢ { rel := rel✝¹ } = { rel := rel✝ }
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case mpr
X Y : RelCat
r : X ⟶ Y
⊢ (∃ f, graphFunctor.map f.hom = r) → IsIso r

Tactic:
rintro ⟨f, rfl⟩

Goal state after:
case mpr
X Y : RelCat
f : X ≅ Y
⊢ IsIso (graphFunctor.map f.hom)
Module: Mathlib.CategoryTheory.Widesubcategory

Goal state before:
pp: case mk
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C → D
P : MorphismProperty D
inst✝ : P.IsMultiplicative
X Y : InducedWideCategory D F P
g : X ⟶ Y
hom✝ : F X ⟶ F Y
property✝ : P hom✝
eq : (wideInducedFunctor F P).map { hom := hom✝, property := property✝ } = (wideInducedFunctor F P).map g
⊢ { hom := hom✝, property := property✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C → D
P : MorphismProperty D
inst✝ : P.IsMultiplicative
X Y : InducedWideCategory D F P
hom✝¹ : F X ⟶ F Y
property✝¹ : P hom✝¹
hom✝ : F X ⟶ F Y
property✝ : P hom✝
eq :
  (wideInducedFunctor F P).map { hom := hom✝¹, property := property✝¹ } =
    (wideInducedFunctor F P).map { hom := hom✝, property := property✝ }
⊢ { hom := hom✝¹, property := property✝¹ } = { hom := hom✝, property := property✝ }
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X : C
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
T : Over X
⊢ Hom.left ((pullbackIsoOverPullback g).inv.app T) ≫ fst T.hom g = pullback.fst T.hom g

Tactic:
by
  simp [← pullbackIsoOverPullback_hom_app_comp_fst, ← Over.comp_left_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: case inl
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
g : (Sum.inl_ C C').obj x✝ ⟶ (Sum.inl_ C C').obj y✝
⊢ (Sum.inl_ C C').map f✝ = g

Tactic:
cases g

Goal state after:
case inl.inl
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C
f✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inl_ C C').map f✝¹ = (Sum.inl_ C C').map f✝
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: case inr
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C'
f✝ : x✝ ⟶ y✝
g : (Sum.inr_ C C').obj x✝ ⟶ (Sum.inr_ C C').obj y✝
⊢ (Sum.inr_ C C').map f✝ = g

Tactic:
cases g

Goal state after:
case inr.inr
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C'
f✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inr_ C C').map f✝¹ = (Sum.inr_ C C').map f✝
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: case inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
z : A ⊕ B
x✝ y✝ : A
f✝ : x✝ ⟶ y✝
g : (Sum.inl_ A B).obj y✝ ⟶ z
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝ ≫ g) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) g

Tactic:
cases g

Goal state after:
case inl.inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
x✝ y✝¹ : A
f✝¹ : x✝ ⟶ y✝¹
y✝ : A
f✝ : y✝¹ ⟶ y✝
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝¹ ≫ (Sum.inl_ A B).map f✝) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝¹) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝)
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: case inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
z : A ⊕ B
x✝ y✝ : B
f✝ : x✝ ⟶ y✝
g : (Sum.inr_ A B).obj y✝ ⟶ z
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝ ≫ g) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) g

Tactic:
cases g

Goal state after:
case inr.inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
x✝ y✝¹ : B
f✝¹ : x✝ ⟶ y✝¹
y✝ : B
f✝ : y✝¹ ⟶ y✝
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝¹ ≫ (Sum.inr_ A B).map f✝) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝¹) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝)
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : HasBinaryCoproducts C
inst✝¹ : SymmetricCategory C
inst✝ : IsMonoidalDistrib C
X Y Z : C
⊢ ∂R X Y Z = coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ ∂L X Y Z ≪≫ β_ X (Y ⨿ Z)

Tactic:
by
  ext <;> simp [leftDistrib_hom, rightDistrib_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ F.map (h.to { a := F.obj A.a, str := F.map A.str }).f ≫ { a := F.obj A.a, str := F.map A.str }.str = 𝟙 (F.obj A.a)

Tactic:
← F.map_id,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ F.map (h.to { a := F.obj A.a, str := F.map A.str }).f ≫ { a := F.obj A.a, str := F.map A.str }.str = F.map (𝟙 A.a)
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ { V := F.obj A.V, str := F.map A.str }.str ≫ F.map (h.from { V := F.obj A.V, str := F.map A.str }).f = 𝟙 (F.obj A.V)

Tactic:
← F.map_id,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ { V := F.obj A.V, str := F.map A.str }.str ≫ F.map (h.from { V := F.obj A.V, str := F.map A.str }).f = F.map (𝟙 A.V)