awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : Bᵒᵖ
f : a ⟶ b
⊢ unop2 (𝟙 f) = 𝟙 f.unop

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
⊢ unop2 (𝟙 f.op) = 𝟙 f

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : Bᵒᵖ
f : a ⟶ b
⊢ op2 (𝟙 f.unop) = 𝟙 f

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, Bicategory.Opposite.op2, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : Bᵒᵖ
f g : a ⟶ b
η : f ≅ g
⊢ η.unop2.op2 = η

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, Bicategory.Opposite.op2, CategoryTheory.Functor.mapIso, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Bᵒᵖ
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
i : c ⟶ d
⊢ i.unop ◁ (op2 (η.unop2 ▷ f.unop)).unop2 =
    (α_ i.unop g.unop f.unop).op2_unop.symm.hom.unop2 ≫
      (op2 ((op2 (i.unop ◁ η.unop2)).unop2 ▷ f.unop) ≫ (α_ i.unop g'.unop f.unop).op2_unop.symm.inv).unop2

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e : Bᵒᵖ
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (op2 (i.unop ◁ (α_ h.unop g.unop f.unop).op2_unop.symm.hom.unop2)).unop2 ≫
      ((α_ i.unop (g ≫ h).unop f.unop).op2_unop.symm.hom ≫
          op2 ((α_ i.unop h.unop g.unop).op2_unop.symm.hom.unop2 ▷ f.unop)).unop2 =
    (α_ i.unop h.unop (f ≫ g).unop).op2_unop.symm.hom.unop2 ≫ (α_ (h ≫ i).unop g.unop f.unop).op2_unop.symm.hom.unop2

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : Bᵒᵖ
f : a ⟶ b
g : b ⟶ c
⊢ unop2 (Iso.hom (Iso.symm (Iso.op2_unop (α_ g.unop (Quiver.Hom.unop (𝟙 b)) f.unop)))) ≫
      (op2 ((ρ_ g.unop).op2_unop.hom.unop2 ▷ f.unop)).unop2 =
    g.unop ◁ (λ_ f.unop).op2_unop.hom.unop2

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
⊢ op2 (f ◁ η) =
    whiskerRight.{w, v, u} (B := Bᵒᵖ) (a := op c) (b := op b) (c := op a) (f := g.op) (g := g'.op) (op2 η) f.op

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f f' : a ⟶ b
g : b ⟶ c
η : f ⟶ f'
⊢ op2 (η ▷ g) =
    whiskerLeft.{w, v, u} (B := Bᵒᵖ) (a := op c) (b := op b) (c := op a) g.op (g := f.op) (h := f'.op) (op2 η)

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ (α_ f g h).op2 =
    Iso.symm (associator.{w, v, u} (B := Bᵒᵖ) (a := op d) (b := op c) (c := op b) (d := op a) h.op g.op f.op)

Tactic:
rfl

Premises used: Quiver.Hom.unop, Bicategory.Opposite.op2, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ op2 (α_ f g h).hom =
    Iso.hom (Iso.symm (associator.{w, v, u} (B := Bᵒᵖ) (a := op d) (b := op c) (c := op b) (d := op a) h.op g.op f.op))

Tactic:
rfl

Premises used: Quiver.Hom.unop, Bicategory.Opposite.op2, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ op2 (α_ f g h).inv =
    Iso.inv (Iso.symm (associator.{w, v, u} (B := Bᵒᵖ) (a := op d) (b := op c) (c := op b) (d := op a) h.op g.op f.op))

Tactic:
rfl

Premises used: Quiver.Hom.unop, Bicategory.Opposite.op2, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
⊢ (λ_ f).op2 = rightUnitor.{w, v, u} (B := Bᵒᵖ) (a := op b) (b := op a) f.op

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.Functor.mapIso, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
⊢ op2 (λ_ f).hom = Iso.hom (rightUnitor.{w, v, u} (B := Bᵒᵖ) (a := op b) (b := op a) f.op)

Tactic:
rfl

Premises used: Quiver.Hom.unop, Bicategory.Opposite.op2, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
⊢ op2 (λ_ f).inv = Iso.inv (rightUnitor.{w, v, u} (B := Bᵒᵖ) (a := op b) (b := op a) f.op)

Tactic:
rfl

Premises used: Quiver.Hom.unop, Bicategory.Opposite.op2, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
⊢ (ρ_ f).op2 = λ_ f.op

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.Functor.mapIso, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
⊢ op2 (ρ_ f).hom = Iso.hom (λ_ f.op)

Tactic:
rfl

Premises used: Quiver.Hom.unop, Bicategory.Opposite.op2, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
⊢ op2 (ρ_ f).inv = Iso.inv (λ_ f.op)

Tactic:
rfl

Premises used: Quiver.Hom.unop, Bicategory.Opposite.op2, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.SingleObj
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
⊢ Functor.IsEquivalence.{v, v, u, u} (C :=
    EndMonoidal.{v, u, 0} (C := MonoidalSingleObj.{v, u} C) (MonoidalSingleObj.star C)) (endMonoidalStarFunctor C)

Tactic:
(endMonoidalStarFunctorEquivalence C).isEquivalence_functor

Premises used: CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence, CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor, CategoryTheory.Equivalence.isEquivalence_functor
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g = h
refl : f ◁ eqToHom ⋯ = eqToHom ⋯
⊢ f ◁ eqToHom η = eqToHom ⋯

Tactic:
cases η
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [whiskerLeft_id, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Bicategory.whiskerLeft_id
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f = g
h : b ⟶ c
refl : eqToHom ⋯ ▷ h = eqToHom ⋯
⊢ eqToHom η ▷ h = eqToHom ⋯

Tactic:
cases η
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
h : b ⟶ c
⊢ eqToHom ⋯ ▷ h = eqToHom ⋯

Tactic:
simp only [id_whiskerRight, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Bicategory.id_whiskerRight
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w : (F.mapComp' f (𝟙 b₁) f ⋯).hom = ((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm).hom
⊢ F.mapComp' f (𝟙 b₁) f ⋯ = (ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w : F.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
⊢ (F.map₂Iso (eqToIso ⋯) ≪≫ F.mapComp f (𝟙 b₁)).hom = ((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₃ :
  F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₄ :
  F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₅ : F.map₂ (𝟙 f) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₆ : 𝟙 (F.map f) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₇ w₈ : (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv

Tactic:
rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]

Premises used: CategoryTheory.eqToIso.hom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom, CategoryTheory.Pseudofunctor.toPrelaxFunctor, CategoryTheory.eqToHom_refl, CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso, CategoryTheory.PrelaxFunctor.map₂_comp_assoc, CategoryTheory.PrelaxFunctor.map₂_id, CategoryTheory.eqToHom_trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' f (𝟙 b₁) f ⋯).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv

Tactic:
simp [mapComp'_comp_id]

Premises used: CategoryTheory.Pseudofunctor.mapComp'_comp_id
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' f (𝟙 b₁) f ⋯).inv = F.map f ◁ (F.mapId b₁).hom ≫ (ρ_ (F.map f)).hom

Tactic:
simp [mapComp'_comp_id]

Premises used: CategoryTheory.Pseudofunctor.mapComp'_comp_id
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w : (F.mapComp' (𝟙 b₀) f f ⋯).hom = ((λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f).hom
⊢ F.mapComp' (𝟙 b₀) f f ⋯ = (λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w : F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
⊢ (F.map₂Iso (eqToIso ⋯) ≪≫ F.mapComp (𝟙 b₀) f).hom = ((λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₃ :
  F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₄ :
  F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₅ : F.map₂ (𝟙 f) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₆ : 𝟙 (F.map f) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₇ w₈ : (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f

Tactic:
rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]

Premises used: CategoryTheory.eqToIso.hom, CategoryTheory.Pseudofunctor.toPrelaxFunctor, CategoryTheory.eqToHom_refl, CategoryTheory.PrelaxFunctor.map₂_comp_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom, CategoryTheory.PrelaxFunctor.map₂_id, CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso, CategoryTheory.eqToHom_trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' (𝟙 b₀) f f ⋯).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f

Tactic:
simp [mapComp'_id_comp]

Premises used: CategoryTheory.Pseudofunctor.mapComp'_id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' (𝟙 b₀) f f ⋯).inv = (F.mapId b₀).hom ▷ F.map f ≫ (λ_ (F.map f)).hom

Tactic:
simp [mapComp'_id_comp]

Premises used: CategoryTheory.Pseudofunctor.mapComp'_id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
subst :
  (F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯).hom =
    (F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯).hom ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom

Tactic:
subst h₀₂ h₁₃ hf
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
⊢ (F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯).hom =
    (F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯).hom ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom

Tactic:
simp [mapComp_assoc_right_hom, Strict.associator_eqToIso, mapComp']

Premises used: CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom, CategoryTheory.Pseudofunctor.mapComp', CategoryTheory.Bicategory.Strict.associator_eqToIso
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
rw :
  (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
          (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).inv ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃

Tactic:
rw [← cancel_epi (F.mapComp' f₀₁ f₁₃ f hf).hom, Iso.hom_inv_id_assoc,
    F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ _ h₀₂ h₁₃ hf]

Premises used: CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Pseudofunctor.mapComp', CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
          (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f hf).inv =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv

Tactic:
simp [← cancel_mono (F.mapComp' f₀₂ f₂₃ f).hom,
    F.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom _ _ _ _ _ _ h₀₂ h₁₃ hf]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Pseudofunctor.mapComp', CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
rw :
  (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ =
    (F.mapComp' f₀₁ f₁₃ f ⋯).hom ≫
      F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv

Tactic:
rw [F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ f h₀₂ h₁₃ (by cat_disch)]

Premises used: CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
rw :
  (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
        (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv
rw₁ rw₂ :
  (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv
⊢ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
      F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv

Tactic:
rw [whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv _ _ _ _ _ _ f h₀₂ h₁₃,
    Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).inv =
    F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
        (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv

Tactic:
simp [← whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv _ _ _ _ _ _ f h₀₂ h₁₃ hf]

Premises used: CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv
-- Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
rw :
  𝟙 (F.map f₀₁ ≫ F.map f₁₃) =
    (F.mapComp' f₀₁ f₁₃ f ⋯).inv ≫
      (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
        (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
          (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).hom =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv

Tactic:
rw [← cancel_epi (F.mapComp' f₀₁ f₁₃ f).inv, Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Pseudofunctor.mapComp', CategoryTheory.cancel_epi, CategoryTheory.Iso.inv