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

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'
⊢ η ▷ g = eqToHom ⋯ ≫ η ▷ g' ≫ eqToHom ⋯

Tactic:
by

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'
⊢ (λ_ f).hom = 𝟙 x ◁ eqToHom h ≫ (λ_ f').hom ≫ eqToHom ⋯

Tactic:
by

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'
⊢ (λ_ f).inv = eqToHom h ≫ (λ_ f').inv ≫ 𝟙 x ◁ eqToHom ⋯

Tactic:
by

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'
⊢ (ρ_ f).hom = eqToHom h ▷ 𝟙 y ≫ (ρ_ f').hom ≫ eqToHom ⋯

Tactic:
by

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'
⊢ (ρ_ f).inv = eqToHom h ≫ (ρ_ f').inv ≫ eqToHom ⋯ ▷ 𝟙 y

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
⊢ normalizeAux p f = normalizeAux p g

Tactic:
by

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

Goal state before:
pp: B : Type u
⊢ [Inhabited B] → Inhabited (FreeBicategory B)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : Quot Rel), Quot.map₂ Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel (Hom₂.id X)) f = f

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : Quot Rel), Quot.map₂ Hom₂.vcomp ⋯ ⋯ f (Quot.mk Rel (Hom₂.id Y)) = f

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {W X Y Z : a ⟶ b} (f : Quot Rel) (g : Quot Rel) (h : Quot Rel),
    Quot.map₂ Hom₂.vcomp ⋯ ⋯ (Quot.map₂ Hom₂.vcomp ⋯ ⋯ f g) h =
      Quot.map₂ Hom₂.vcomp ⋯ ⋯ f (Quot.map₂ Hom₂.vcomp ⋯ ⋯ g h)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g),
    Quot.map (Hom₂.whisker_left (𝟙 a)) ⋯ η =
      { hom := Quot.mk Rel (Hom₂.left_unitor f), inv := Quot.mk Rel (Hom₂.left_unitor_inv f), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        η ≫
          { hom := Quot.mk Rel (Hom₂.left_unitor g), inv := Quot.mk Rel (Hom₂.left_unitor_inv g), hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.inv

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
    Quot.map (Hom₂.whisker_left (f ≫ g)) ⋯ η =
      { 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 := ⋯ }.hom ≫
        Quot.map (Hom₂.whisker_left f) ⋯ (Quot.map (Hom₂.whisker_left g) ⋯ η) ≫
          { 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 := ⋯ }.inv

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g),
    Quot.map (Hom₂.whisker_right (𝟙 b)) ⋯ η =
      { hom := Quot.mk Rel (Hom₂.right_unitor f), inv := Quot.mk Rel (Hom₂.right_unitor_inv f), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        η ≫
          { hom := Quot.mk Rel (Hom₂.right_unitor g), inv := Quot.mk Rel (Hom₂.right_unitor_inv g), hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.inv

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
    Quot.map (Hom₂.whisker_right (g ≫ h)) ⋯ η =
      { 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 := ⋯ }.inv ≫
        Quot.map (Hom₂.whisker_right h) ⋯ (Quot.map (Hom₂.whisker_right g) ⋯ η) ≫
          { 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 := ⋯ }.hom

Tactic:
by

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

Goal state before:
pp: case mk
B : Type u
inst✝ : Quiver B
a b c d : FreeBicategory B
f : a ⟶ b
g g' : b ⟶ c
η✝ : g ⟶ g'
η : Hom₂ g g'
h : c ⟶ d
⊢ Quot.map (Hom₂.whisker_right h) ⋯ (Quot.map (Hom₂.whisker_left f) ⋯ (Quot.mk Rel η)) =
    { 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 := ⋯ }.hom ≫
      Quot.map (Hom₂.whisker_left f) ⋯ (Quot.map (Hom₂.whisker_right h) ⋯ (Quot.mk Rel η)) ≫
        { 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 := ⋯ }.inv

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

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
    Quot.map (Hom₂.whisker_right h) ⋯ (Quot.map (Hom₂.whisker_left f) ⋯ η) =
      { 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 := ⋯ }.hom ≫
        Quot.map (Hom₂.whisker_left f) ⋯ (Quot.map (Hom₂.whisker_right h) ⋯ η) ≫
          { 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 := ⋯ }.inv

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
⊢ (preinclusion B).map { as := p } ◁ η ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b c : B
f : Hom a b
g : Hom b c
⊢ normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : X ⟶ Y),
    (𝟭 (a ⟶ b)).map f ≫ ((λ_ Y).symm ≪≫ normalizeIso nil Y).hom =
      ((λ_ X).symm ≪≫ normalizeIso nil X).hom ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map f

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : B
f : Discrete (Path a b)
⊢ (inclusionPath a b ⋙ (normalize B).mapFunctor a b).obj f = (𝟭 (Discrete (Path a b))).obj f

Tactic:
by

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
x : B
h : c ⟶ x
X✝ Y✝ : LeftExtension f g
η : X✝ ⟶ Y✝
⊢ (X✝.whisker h).unit ≫ f ◁ StructuredArrow.Hom.right η ▷ h = (Y✝.whisker h).unit

Tactic:
by

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 =
    (s.unit ≫ f ◁ StructuredArrow.Hom.right i) ▷ h

Tactic:
by

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
⊢ t.unit ▷ h = StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv

Tactic:
by

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) =
    StructuredArrow.hom (t.whisker h)

Tactic:
by

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.right (whiskerHom i.hom h ≫ whiskerHom i.inv h) = StructuredArrow.Hom.right (i.hom ≫ i.inv) ▷ h

Tactic:
by

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.right (i.hom ≫ i.inv) ▷ h = 𝟙 (StructuredArrow.right s ≫ h)

Tactic:
by

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.right (whiskerHom i.inv h ≫ whiskerHom i.hom h) = StructuredArrow.Hom.right (i.inv ≫ i.hom) ▷ h

Tactic:
by

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.right (i.inv ≫ i.hom) ▷ h = 𝟙 (StructuredArrow.right t ≫ h)

Tactic:
by

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✝
⊢ (X✝.whisker h).unit ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f = (Y✝.whisker h).unit

Tactic:
by

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 =
    h ◁ (s.unit ≫ StructuredArrow.Hom.right i ▷ f)

Tactic:
by

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
⊢ h ◁ t.unit = StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom

Tactic:
by

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) =
    StructuredArrow.hom (t.whisker h)

Tactic:
by

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.right (whiskerHom i.hom h ≫ whiskerHom i.inv h) = h ◁ StructuredArrow.Hom.right (i.hom ≫ i.inv)

Tactic:
by

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
⊢ h ◁ StructuredArrow.Hom.right (i.hom ≫ i.inv) = 𝟙 (h ≫ StructuredArrow.right s)

Tactic:
by

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.right (whiskerHom i.inv h ≫ whiskerHom i.hom h) = h ◁ StructuredArrow.Hom.right (i.inv ≫ i.hom)

Tactic:
by

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
⊢ h ◁ StructuredArrow.Hom.right (i.inv ≫ i.hom) = 𝟙 (h ≫ StructuredArrow.right t)

Tactic:
by

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 ≫ (Y✝.whisker h).counit = (X✝.whisker h).counit

Tactic:
by

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 ◁ (i.left ▷ f ≫ t.counit)

Tactic:
by

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.counit = (α_ h s.lift f).inv ≫ CostructuredArrow.hom (s.whisker h)

Tactic:
by

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
⊢ (postcomp x f).map (h ◁ i.left) ≫ CostructuredArrow.hom (t.whisker h) = CostructuredArrow.hom (s.whisker h)

Tactic:
by

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
⊢ (whiskerHom i.hom h ≫ whiskerHom i.inv h).left = h ◁ (i.hom ≫ i.inv).left

Tactic:
by

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 ◁ (i.hom ≫ i.inv).left = 𝟙 (h ≫ s.left)

Tactic:
by

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
⊢ (whiskerHom i.inv h ≫ whiskerHom i.hom h).left = h ◁ (i.inv ≫ i.hom).left

Tactic:
by

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 ◁ (i.inv ≫ i.hom).left = 𝟙 (h ≫ t.left)

Tactic:
by

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

Goal state before:
pp: 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
H : Rel η θ
⊢ liftHom₂ F η = liftHom₂ F θ

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b : FreeBicategory B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b c : FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (f ◁ η) =
      (Iso.refl (liftHom F (f ≫ g))).hom ≫ liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ η ≫ (Iso.refl (liftHom F (f ≫ h))).inv

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b c : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g ≫ h))).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Modification.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), (app a).hom ▷ G.map f ≫ θ.naturality f = η.naturality f ≫ F.map f ◁ (app b).hom
a b : B
f : a ⟶ b
⊢ (app a).inv ▷ G.map f ≫ η.naturality f = θ.naturality f ≫ F.map f ◁ (app b).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Modification.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ θ.naturality f = η.naturality f ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ η.naturality f = θ.naturality f ≫ (app a).inv ▷ G.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a : B
⊢ (α.naturality (𝟙 a)).hom =
    (F.mapId a).hom ▷ α.app a ≫ (λ_ (α.app a)).hom ≫ (ρ_ (α.app a)).inv ≫ α.app a ◁ (G.mapId a).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a : B
⊢ α.naturality (𝟙 a) = F.mapId a ▷ᵢ α.app a ≪≫ λ_ (α.app a) ≪≫ (ρ_ (α.app a)).symm ≪≫ α.app a ◁ᵢ (G.mapId a).symm

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a : B
⊢ (α.naturality (𝟙 a)).inv =
    α.app a ◁ (G.mapId a).hom ≫ (ρ_ (α.app a)).hom ≫ (λ_ (α.app a)).inv ≫ (F.mapId a).inv ▷ α.app a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ (α.naturality g).hom = F.map₂ η.inv ▷ α.app b ≫ (α.naturality f).hom ≫ α.app a ◁ G.map₂ η.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ α.naturality g = F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ (α.naturality g).inv = α.app a ◁ G.map₂ η.inv ≫ (α.naturality f).inv ≫ F.map₂ η.hom ▷ α.app b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α.naturality (f ≫ g)).hom =
    (F.mapComp f g).hom ▷ α.app c ≫
      (α_ (F.map f) (F.map g) (α.app c)).hom ≫
        F.map f ◁ (α.naturality g).hom ≫
          (α_ (F.map f) (α.app b) (G.map g)).inv ≫
            (α.naturality f).hom ▷ G.map g ≫ (α_ (α.app a) (G.map f) (G.map g)).hom ≫ α.app a ◁ (G.mapComp f g).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ α.naturality (f ≫ g) =
    F.mapComp f g ▷ᵢ α.app c ≪≫
      α_ (F.map f) (F.map g) (α.app c) ≪≫
        F.map f ◁ᵢ α.naturality g ≪≫
          (α_ (F.map f) (α.app b) (G.map g)).symm ≪≫
            α.naturality f ▷ᵢ G.map g ≪≫ α_ (α.app a) (G.map f) (G.map g) ≪≫ α.app a ◁ᵢ (G.mapComp f g).symm

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α.naturality (f ≫ g)).inv =
    α.app a ◁ (G.mapComp f g).hom ≫
      (α_ (α.app a) (G.map f) (G.map g)).inv ≫
        (α.naturality f).inv ▷ G.map g ≫
          (α_ (F.map f) (α.app b) (G.map g)).hom ≫
            F.map f ◁ (α.naturality g).inv ≫ (α_ (F.map f) (F.map g) (α.app c)).inv ≫ (F.mapComp f g).inv ▷ α.app c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ η.vCompNaturality θ f ≫ F.map₂ β ▷ η.vCompApp θ b =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫ (η.naturality f ≫ F.map₂ β ▷ η.app b) ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
Γ : Modification η θ
a b : B
a' : C
f : a' ⟶ F.obj a
g : a ⟶ b
⊢ f ◁ Γ.app a ▷ G.map g ≫ f ◁ θ.naturality g = f ◁ η.naturality g ≫ f ◁ F.map g ◁ Γ.app b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫ (η.naturality f ≫ F.map₂ β ▷ η.app b) ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.naturality f ≫ G.map₂ β ▷ θ.app b) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
Γ : Modification η θ
a b : B
a' : C
f : a ⟶ b
g : G.obj b ⟶ a'
⊢ Γ.app a ▷ G.map f ▷ g ≫ θ.naturality f ▷ g = η.naturality f ▷ g ≫ (F.map f ◁ Γ.app b) ▷ g

Tactic:
by

Goal state after: