[GOAL]
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
a : B
⊢ leftZigzag (ρ_ (𝟙 a)).inv (ρ_ (𝟙 a)).hom = (λ_ (𝟙 a)).hom ≫ (ρ_ (𝟙 a)).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
a : B
⊢ (ρ_ (𝟙 a)).inv ▷ 𝟙 a ⊗≫ 𝟙 a ◁ (ρ_ (𝟙 a)).hom = (λ_ (𝟙 a)).hom ≫ (ρ_ (𝟙 a)).inv
[PROOFSTEP]
coherence
[GOAL]
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
a : B
⊢ rightZigzag (ρ_ (𝟙 a)).inv (ρ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom ≫ (λ_ (𝟙 a)).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
a : B
⊢ 𝟙 a ◁ (ρ_ (𝟙 a)).inv ⊗≫ (ρ_ (𝟙 a)).hom ▷ 𝟙 a = (ρ_ (𝟙 a)).hom ≫ (λ_ (𝟙 a)).inv
[PROOFSTEP]
coherence
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (leftZigzagIso η ε).inv = rightZigzag ε.inv η.inv
[PROOFSTEP]
simp [bicategoricalComp, bicategoricalIsoComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (rightZigzagIso η ε).inv = leftZigzag ε.inv η.inv
[PROOFSTEP]
simp [bicategoricalComp, bicategoricalIsoComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ leftZigzagIso η (adjointifyCounit η ε) = λ_ f ≪≫ (ρ_ f).symm
[PROOFSTEP]
apply Iso.ext
[GOAL]
case w
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (leftZigzagIso η (adjointifyCounit η ε)).hom = (λ_ f ≪≫ (ρ_ f).symm).hom
[PROOFSTEP]
dsimp [adjointifyCounit, bicategoricalIsoComp]
[GOAL]
case w
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ η.hom ▷ f ≫
      ((α_ f g f).hom ≫ 𝟙 f ▷ (g ≫ f)) ≫
        f ◁ (g ◁ ((ρ_ f).inv ≫ (f ◁ ε.inv ≫ (𝟙 f ▷ (g ≫ f) ≫ (α_ f g f).inv) ≫ η.inv ▷ f) ≫ (λ_ f).hom) ≫ ε.hom) =
    (λ_ f).hom ≫ (ρ_ f).inv
[PROOFSTEP]
calc
  _ = 𝟙 _ ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := by simp [bicategoricalComp];
    coherence
  _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := by
    rw [← whisker_exchange η.hom (f ◁ ε.inv)]; simp [bicategoricalComp]; coherence
  _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := by rw [← whisker_exchange η.hom η.inv]; coherence
  _ = 𝟙 _ ⊗≫ f ◁ (ε.inv ≫ ε.hom) := by rw [Iso.inv_hom_id]; simp [bicategoricalComp]
  _ = _ := by rw [Iso.inv_hom_id]; simp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ η.hom ▷ f ≫
      ((α_ f g f).hom ≫ 𝟙 f ▷ (g ≫ f)) ≫
        f ◁ (g ◁ ((ρ_ f).inv ≫ (f ◁ ε.inv ≫ (𝟙 f ▷ (g ≫ f) ≫ (α_ f g f).inv) ≫ η.inv ▷ f) ≫ (λ_ f).hom) ≫ ε.hom) =
    𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom
[PROOFSTEP]
simp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ η.hom ▷ f ≫
      (α_ f g f).hom ≫
        (ρ_ (f ≫ g ≫ f)).inv ≫
          (α_ f (g ≫ f) (𝟙 b)).hom ≫
            f ◁ (α_ g f (𝟙 b)).hom ≫
              f ◁ g ◁ f ◁ ε.inv ≫ f ◁ g ◁ (α_ f g f).inv ≫ f ◁ g ◁ η.inv ▷ f ≫ f ◁ g ◁ (λ_ f).hom ≫ f ◁ ε.hom =
    (λ_ f).hom ≫
      (ρ_ f).inv ≫
        (λ_ (f ≫ 𝟙 b)).inv ≫
          (α_ (𝟙 a) f (𝟙 b)).inv ≫
            (ρ_ (𝟙 a ≫ f)).hom ≫
              η.hom ▷ f ≫
                (ρ_ ((f ≫ g) ≫ f)).inv ≫
                  (α_ (f ≫ g) f (𝟙 b)).hom ≫
                    (α_ f g (f ≫ 𝟙 b)).hom ≫
                      f ◁ g ◁ f ◁ ε.inv ≫ f ◁ g ◁ (α_ f g f).inv ≫ f ◁ g ◁ η.inv ▷ f ≫ f ◁ g ◁ (λ_ f).hom ≫ f ◁ ε.hom
[PROOFSTEP]
coherence
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
[PROOFSTEP]
rw [← whisker_exchange η.hom (f ◁ ε.inv)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ (𝟙 a ◁ f ◁ ε.inv ≫ η.hom ▷ (f ≫ g ≫ f)) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
[PROOFSTEP]
simp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ f ◁ ε.inv ≫
      (λ_ (f ≫ g ≫ f)).inv ≫
        (α_ (𝟙 a) f (g ≫ f)).inv ≫
          (α_ (𝟙 a ≫ f) g f).inv ≫
            η.hom ▷ f ▷ g ▷ f ≫
              (α_ ((f ≫ g) ≫ f) g f).hom ≫
                (α_ (f ≫ g) f (g ≫ f)).hom ≫
                  (α_ f g (f ≫ g ≫ f)).hom ≫
                    f ◁ g ◁ (α_ f g f).inv ≫ f ◁ g ◁ η.inv ▷ f ≫ f ◁ g ◁ (λ_ f).hom ≫ f ◁ ε.hom =
    f ◁ ε.inv ≫
      (α_ f g f).inv ≫
        (λ_ ((f ≫ g) ≫ f)).inv ≫
          (α_ (𝟙 a) (f ≫ g) f).inv ≫
            (α_ (𝟙 a) f g).inv ▷ f ≫
              η.hom ▷ f ▷ g ▷ f ≫
                (α_ (f ≫ g) f g).hom ▷ f ≫
                  (α_ (f ≫ g) (f ≫ g) f).hom ≫
                    (α_ f g ((f ≫ g) ≫ f)).hom ≫ f ◁ g ◁ η.inv ▷ f ≫ f ◁ g ◁ (λ_ f).hom ≫ f ◁ ε.hom
[PROOFSTEP]
coherence
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
[PROOFSTEP]
rw [← whisker_exchange η.hom η.inv]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (𝟙 a ◁ η.inv ≫ η.hom ▷ 𝟙 a) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
[PROOFSTEP]
coherence
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
[PROOFSTEP]
rw [Iso.inv_hom_id]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ 𝟙 (f ≫ g) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
[PROOFSTEP]
simp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
[PROOFSTEP]
rw [Iso.inv_hom_id]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ 𝟙 (𝟙 b) = (λ_ f).hom ≫ (ρ_ f).inv
[PROOFSTEP]
simp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
η : 𝟙 a✝ ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
a : B
⊢ leftZigzagIso (ρ_ (𝟙 a)).symm (ρ_ (𝟙 a)) = λ_ (𝟙 a) ≪≫ (ρ_ (𝟙 a)).symm
[PROOFSTEP]
ext
[GOAL]
case w
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
η : 𝟙 a✝ ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
a : B
⊢ (leftZigzagIso (ρ_ (𝟙 a)).symm (ρ_ (𝟙 a))).hom = (λ_ (𝟙 a) ≪≫ (ρ_ (𝟙 a)).symm).hom
[PROOFSTEP]
simp [bicategoricalIsoComp]
