awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
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
rw :
  (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom) ≫ (α_ (f ≫ g) h i).inv =
    (f ◁ (α_ g h i).inv ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) ≫ (α_ (f ≫ g) h i).inv
⊢ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom = f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv

Tactic:
rw [← cancel_epi (f ◁ (α_ g h i).inv), ← cancel_mono (α_ (f ≫ g) h i).inv]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Bicategory.associator, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
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
⊢ (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom) ≫ (α_ (f ≫ g) h i).inv =
    (f ◁ (α_ g h i).inv ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) ≫ (α_ (f ≫ g) h i).inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
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
⊢ inv ((α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom) =
    inv ((α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
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
⊢ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv = (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i

Tactic:
simp [← cancel_epi (f ◁ (α_ g h i).inv)]

Premises used: CategoryTheory.Bicategory.associator, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
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
⊢ inv ((α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv) =
    inv ((α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
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
rw :
  ((α_ f g (h ≫ i)).inv ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv) ≫ (α_ f g h).inv ▷ i =
    ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) ≫ (α_ f g h).inv ▷ i
⊢ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv = (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i

Tactic:
rw [← cancel_epi (α_ f g (h ≫ i)).inv, ← cancel_mono ((α_ f g h).inv ▷ i)]

Premises used: CategoryTheory.Bicategory.whiskerRight, CategoryTheory.cancel_mono, CategoryTheory.Bicategory.associator, CategoryTheory.CategoryStruct.comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
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
⊢ ((α_ f g (h ≫ i)).inv ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv) ≫ (α_ f g h).inv ▷ i =
    ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) ≫ (α_ f g h).inv ▷ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
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
⊢ inv ((α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) =
    inv ((α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
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
⊢ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom = (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom

Tactic:
simp [← cancel_epi ((α_ f g h).hom ▷ i)]

Premises used: CategoryTheory.Bicategory.whiskerRight, CategoryTheory.Bicategory.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
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
⊢ inv ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) =
    inv (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (𝟙 b) g).hom ≫ f ◁ (λ_ g).hom = (ρ_ f).hom ▷ g

Tactic:
triangle f g

Premises used: CategoryTheory.Bicategory.triangle
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
rw : (α_ f (𝟙 b) g).inv ≫ (α_ f (𝟙 b) g).hom ≫ f ◁ (λ_ g).hom = f ◁ (λ_ g).hom
rw₁ rw₂ : f ◁ (λ_ g).hom = f ◁ (λ_ g).hom
⊢ (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom

Tactic:
rw [← triangle, inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Bicategory.triangle
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv

Tactic:
simp [← cancel_mono (f ◁ (λ_ g).hom)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Bicategory.leftUnitor, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g

Tactic:
simp [← cancel_mono ((ρ_ f).hom ▷ g)]

Premises used: CategoryTheory.Bicategory.rightUnitor, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.cancel_mono, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ (g ≫ h) ≫ (α_ f' g h).inv = (α_ f g h).inv ≫ η ▷ g ▷ h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h = (α_ f g h).hom ≫ η ▷ (g ≫ h) ≫ (α_ f' g h).inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ η ▷ h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h ≫ (α_ f g' h).inv = (α_ f g h).inv ≫ (f ◁ η) ▷ h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h = (α_ f g h).inv ≫ (f ◁ η) ▷ h ≫ (α_ f g' h).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ g ◁ η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η ≫ (α_ f g h').inv = (α_ f g h).inv ≫ (f ≫ g) ◁ η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η = (α_ f g h).inv ≫ (f ≫ g) ◁ η ≫ (α_ f g h').hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ 𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ≫ (λ_ g).inv = (λ_ f).inv ≫ 𝟙 a ◁ η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ≫ (ρ_ g).inv = (ρ_ f).inv ≫ η ▷ 𝟙 b

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (ρ_ f).inv ≫ η ▷ 𝟙 b ≫ (ρ_ g).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ Eq (α := 𝟙 a ≫ f ⟶ 𝟙 a ≫ g) (𝟙 a ◁ η) (𝟙 a ◁ θ) ↔ η = θ

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ η ▷ 𝟙 b = θ ▷ 𝟙 b ↔ η = θ

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
rw : Eq (α := 𝟙 a ≫ (𝟙 a ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g) (𝟙 a ◁ (λ_ f).hom ▷ g) (𝟙 a ◁ (hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom))
rw₁ :
  Eq (α := 𝟙 a ≫ (𝟙 a ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g) (𝟙 a ◁ (λ_ f).hom ▷ g) (𝟙 a ◁ hom (α_ (𝟙 a) f g) ≫ 𝟙 a ◁ (λ_ (f ≫ g)).hom)
rw₂ :
  Eq (α := (𝟙 a ≫ 𝟙 a ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g) (hom (α_ (𝟙 a) (𝟙 a ≫ f) g) ≫ 𝟙 a ◁ (λ_ f).hom ▷ g)
    (hom (α_ (𝟙 a) (𝟙 a ≫ f) g) ≫ 𝟙 a ◁ hom (α_ (𝟙 a) f g) ≫ 𝟙 a ◁ (λ_ (f ≫ g)).hom)
rw₃ :
  Eq (α := ((𝟙 a ≫ 𝟙 a) ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g)
    (hom (α_ (𝟙 a) (𝟙 a) f) ▷ g ≫ hom (α_ (𝟙 a) (𝟙 a ≫ f) g) ≫ 𝟙 a ◁ (λ_ f).hom ▷ g)
    (hom (α_ (𝟙 a) (𝟙 a) f) ▷ g ≫ hom (α_ (𝟙 a) (𝟙 a ≫ f) g) ≫ 𝟙 a ◁ hom (α_ (𝟙 a) f g) ≫ 𝟙 a ◁ (λ_ (f ≫ g)).hom)
rw₄ :
  Eq (α := ((𝟙 a ≫ 𝟙 a) ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g)
    (hom (α_ (𝟙 a) (𝟙 a) f) ▷ g ≫ hom (α_ (𝟙 a) (𝟙 a ≫ f) g) ≫ 𝟙 a ◁ (λ_ f).hom ▷ g)
    (hom (α_ (𝟙 a ≫ 𝟙 a) f g) ≫ hom (α_ (𝟙 a) (𝟙 a) (f ≫ g)) ≫ 𝟙 a ◁ (λ_ (f ≫ g)).hom)
rw₅ :
  Eq (α := ((𝟙 a ≫ 𝟙 a) ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g)
    (hom (α_ (𝟙 a) (𝟙 a) f) ▷ g ≫ hom (α_ (𝟙 a) (𝟙 a ≫ f) g) ≫ 𝟙 a ◁ (λ_ f).hom ▷ g)
    (hom (α_ (𝟙 a ≫ 𝟙 a) f g) ≫ hom (ρ_ (𝟙 a)) ▷ (f ≫ g))
rw₆ :
  Eq (α := ((𝟙 a ≫ 𝟙 a) ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g)
    (hom (α_ (𝟙 a) (𝟙 a) f) ▷ g ≫ (𝟙 a ◁ (λ_ f).hom) ▷ g ≫ hom (α_ (𝟙 a) f g))
    (hom (α_ (𝟙 a ≫ 𝟙 a) f g) ≫ hom (ρ_ (𝟙 a)) ▷ (f ≫ g))
rw₇ :
  Eq (α := ((𝟙 a ≫ 𝟙 a) ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g) ((hom (α_ (𝟙 a) (𝟙 a) f) ≫ 𝟙 a ◁ (λ_ f).hom) ▷ g ≫ hom (α_ (𝟙 a) f g))
    (hom (α_ (𝟙 a ≫ 𝟙 a) f g) ≫ hom (ρ_ (𝟙 a)) ▷ (f ≫ g))
rw₈ :
  Eq (α := ((𝟙 a ≫ 𝟙 a) ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g) (hom (ρ_ (𝟙 a)) ▷ f ▷ g ≫ hom (α_ (𝟙 a) f g))
    (hom (α_ (𝟙 a ≫ 𝟙 a) f g) ≫ hom (ρ_ (𝟙 a)) ▷ (f ≫ g))
rw₉ rw₁₀ :
  Eq (α := ((𝟙 a ≫ 𝟙 a) ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g) (hom (α_ (𝟙 a ≫ 𝟙 a) f g) ≫ hom (ρ_ (𝟙 a)) ▷ (f ≫ g))
    (hom (α_ (𝟙 a ≫ 𝟙 a) f g) ≫ hom (ρ_ (𝟙 a)) ▷ (f ≫ g))
⊢ (λ_ f).hom ▷ g = hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom

Tactic:
rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ←
      cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle, ← associator_naturality_middle, ←
      comp_whiskerRight_assoc, triangle, associator_naturality_left]

Premises used: CategoryTheory.Bicategory.whiskerLeft_iff, CategoryTheory.Bicategory.whiskerLeft_comp, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.Bicategory.pentagon_assoc, CategoryTheory.Bicategory.comp_whiskerRight_assoc, CategoryTheory.Bicategory.associator_naturality_middle, CategoryTheory.Bicategory.triangle, CategoryTheory.Bicategory.associator, CategoryTheory.Bicategory.associator_naturality_left, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ inv ((λ_ f).inv ▷ g) = inv ((λ_ (f ≫ g)).inv ≫ Iso.inv (α_ (𝟙 a) f g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
rw : (f ◁ (ρ_ g).hom) ▷ 𝟙 c = ((α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom) ▷ 𝟙 c
rw₁ : (f ◁ (ρ_ g).hom) ▷ 𝟙 c = (α_ f g (𝟙 c)).inv ▷ 𝟙 c ≫ (ρ_ (f ≫ g)).hom ▷ 𝟙 c
rw₂ :
  (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
    (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (α_ f g (𝟙 c)).inv ▷ 𝟙 c ≫ (ρ_ (f ≫ g)).hom ▷ 𝟙 c
rw₃ :
  f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
    f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (α_ f g (𝟙 c)).inv ▷ 𝟙 c ≫ (ρ_ (f ≫ g)).hom ▷ 𝟙 c
rw₄ :
  f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
    (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (α_ (f ≫ g) (𝟙 c) (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom ▷ 𝟙 c
rw₅ :
  f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
    (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ hom (λ_ (𝟙 c))
rw₆ :
  f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ f ◁ (ρ_ g).hom ▷ 𝟙 c ≫ (α_ f g (𝟙 c)).inv =
    (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ hom (λ_ (𝟙 c))
rw₇ :
  f ◁ ((α_ g (𝟙 c) (𝟙 c)).inv ≫ (ρ_ g).hom ▷ 𝟙 c) ≫ (α_ f g (𝟙 c)).inv =
    (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ hom (λ_ (𝟙 c))
rw₈ : f ◁ g ◁ hom (λ_ (𝟙 c)) ≫ (α_ f g (𝟙 c)).inv = (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ hom (λ_ (𝟙 c))
rw₉ rw₁₀ : (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ hom (λ_ (𝟙 c)) = (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ hom (λ_ (𝟙 c))
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom

Tactic:
rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ←
      cancel_epi (f ◁ (α_ _ _ _).inv), pentagon_inv_assoc, triangle_assoc_comp_right, ←
      associator_inv_naturality_middle, ← whiskerLeft_comp_assoc, triangle_assoc_comp_right,
      associator_inv_naturality_right]

Premises used: CategoryTheory.Bicategory.associator_inv_naturality_middle, CategoryTheory.Bicategory.associator_inv_naturality_right, CategoryTheory.Bicategory.comp_whiskerRight, CategoryTheory.Bicategory.whiskerRight_iff, CategoryTheory.Bicategory.pentagon_inv_assoc, CategoryTheory.Bicategory.triangle_assoc_comp_right, CategoryTheory.Bicategory.whiskerLeft_comp_assoc, CategoryTheory.Bicategory.associator, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ inv (f ◁ (ρ_ g).inv) = inv ((ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).hom = Iso.inv (α_ (𝟙 a) f g) ≫ (λ_ f).hom ▷ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).inv = (λ_ f).inv ▷ g ≫ hom (α_ (𝟙 a) f g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ (f ≫ g)).hom = (α_ f g (𝟙 c)).hom ≫ f ◁ (ρ_ g).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ (f ≫ g)).inv = f ◁ (ρ_ g).inv ≫ (α_ f g (𝟙 c)).inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
rw :
  Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a ≫ 𝟙 a) (𝟙 a ≫ 𝟙 a)) (𝟙 a ◁ hom (λ_ (𝟙 a)))
    (𝟙 a ◁ hom (ρ_ (𝟙 a)))
rw₁ :
  Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) ((𝟙 a ≫ 𝟙 a) ≫ 𝟙 a) (𝟙 a ≫ 𝟙 a))
    (hom (α_ (𝟙 a) (𝟙 a) (𝟙 a)) ≫ 𝟙 a ◁ hom (λ_ (𝟙 a))) (hom (α_ (𝟙 a) (𝟙 a) (𝟙 a)) ≫ 𝟙 a ◁ hom (ρ_ (𝟙 a)))
rw₂ :
  Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) ((𝟙 a ≫ 𝟙 a) ≫ 𝟙 a) (𝟙 a))
    ((hom (α_ (𝟙 a) (𝟙 a) (𝟙 a)) ≫ 𝟙 a ◁ hom (λ_ (𝟙 a))) ≫ hom (ρ_ (𝟙 a)))
    ((hom (α_ (𝟙 a) (𝟙 a) (𝟙 a)) ≫ 𝟙 a ◁ hom (ρ_ (𝟙 a))) ≫ hom (ρ_ (𝟙 a)))
rw₃ :
  Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) ((𝟙 a ≫ 𝟙 a) ≫ 𝟙 a) (𝟙 a)) (hom (ρ_ (𝟙 a)) ▷ 𝟙 a ≫ hom (ρ_ (𝟙 a)))
    ((hom (α_ (𝟙 a) (𝟙 a) (𝟙 a)) ≫ 𝟙 a ◁ hom (ρ_ (𝟙 a))) ≫ hom (ρ_ (𝟙 a)))
rw₄ :
  Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) ((𝟙 a ≫ 𝟙 a) ≫ 𝟙 a) (𝟙 a)) (hom (ρ_ (𝟙 a)) ▷ 𝟙 a ≫ hom (ρ_ (𝟙 a)))
    (hom (ρ_ (𝟙 a ≫ 𝟙 a)) ≫ hom (ρ_ (𝟙 a)))
rw₅ rw₆ :
  Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) ((𝟙 a ≫ 𝟙 a) ≫ 𝟙 a) (𝟙 a)) (hom (ρ_ (𝟙 a ≫ 𝟙 a)) ≫ hom (ρ_ (𝟙 a)))
    (hom (ρ_ (𝟙 a ≫ 𝟙 a)) ≫ hom (ρ_ (𝟙 a)))
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a)) (hom (λ_ (𝟙 a))) (hom (ρ_ (𝟙 a)))

Tactic:
rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ←
      rightUnitor_comp, rightUnitor_naturality]

Premises used: CategoryTheory.Bicategory.whiskerLeft_iff, CategoryTheory.Bicategory.rightUnitor, CategoryTheory.cancel_mono, CategoryTheory.Bicategory.triangle, CategoryTheory.Bicategory.rightUnitor_comp, CategoryTheory.Bicategory.rightUnitor_naturality, CategoryTheory.Bicategory.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a) (𝟙 a ≫ 𝟙 a)) (Iso.inv (λ_ (𝟙 a))) (Iso.inv (ρ_ (𝟙 a)))

Tactic:
simp [Iso.inv_eq_inv]

Premises used: CategoryTheory.Iso.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
X : CatEnriched C
⊢ Eq.{u_2 + 1} (α := X ⟶ X) (𝟙 X)
    (Functor.obj (Cat.Hom.toFunctor (eId Cat X))
      { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
X Y Z : CatEnriched C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ g = Functor.obj (Cat.Hom.toFunctor (eComp Cat X Y Z)) (f, g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g : b ⟶ c
⊢ hComp (𝟙 f) (𝟙 g) = 𝟙 (f ≫ g)

Tactic:
Functor.map_id ..

Premises used: CategoryTheory.CatEnriched.hComp, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f f' : a ⟶ b
α : f = f'
g g' : b ⟶ c
β : g = g'
refl : hComp (eqToHom ⋯) (eqToHom β) = eqToHom ⋯
⊢ hComp (eqToHom α) (eqToHom β) = eqToHom ⋯

Tactic:
cases α
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g g' : b ⟶ c
β : g = g'
refl : hComp (eqToHom ⋯) (eqToHom ⋯) = eqToHom ⋯
⊢ hComp (eqToHom ⋯) (eqToHom β) = eqToHom ⋯

Tactic:
cases β
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g : b ⟶ c
⊢ hComp (eqToHom ⋯) (eqToHom ⋯) = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f₁ f₂ f₃ : a ⟶ b
g₁ g₂ g₃ : b ⟶ c
η : f₁ ⟶ f₂
η' : f₂ ⟶ f₃
θ : g₁ ⟶ g₂
θ' : g₂ ⟶ g₃
⊢ hComp η θ ≫ hComp η' θ' = hComp (η ≫ η') (θ ≫ θ')

Tactic:
((eComp Cat a b c).toFunctor.map_comp (Y := (_, _)) (_, _) (_, _)).symm

Premises used: CategoryTheory.CatEnriched.hComp, Prod.mk, CategoryTheory.Cat, CategoryTheory.eComp, CategoryTheory.Functor.map_comp, Eq.symm, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
rw :
  HEq (α :=
    Quiver.Hom (V := a ⟶ b)
      (Functor.obj (Cat.Hom.toFunctor (eId Cat a))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) } ≫
        f)
      (Functor.obj (Cat.Hom.toFunctor (eId Cat a))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) } ≫
        f'))
    (hComp (Functor.map (Cat.Hom.toFunctor (eId Cat a)) (𝟙 { down := { as := () } })) η) η
⊢ HEq (α := 𝟙 a ≫ f ⟶ 𝟙 a ≫ f') (hComp (𝟙 (𝟙 a)) η) η

Tactic:
rw [id_eq, ← Functor.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.CatEnriched.id_eq
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ HEq (α :=
    Quiver.Hom (V := a ⟶ b)
      (Functor.obj (Cat.Hom.toFunctor (eId Cat a))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) } ≫
        f)
      (Functor.obj (Cat.Hom.toFunctor (eId Cat a))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) } ≫
        f'))
    (hComp (Functor.map (Cat.Hom.toFunctor (eId Cat a)) (𝟙 { down := { as := () } })) η) η

Tactic:
congr_arg_heq (·.toFunctor.map η) (e_id_comp (V := Cat) a b)

Premises used: CategoryTheory.e_id_comp, congr_arg_heq, CategoryTheory.CatEnriched.hComp, CategoryTheory.Cat
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ HEq (α :=
    Quiver.Hom (V := a ⟶ b)
      (Functor.obj (Cat.Hom.toFunctor (eId Cat a))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) } ≫
        f)
      (Functor.obj (Cat.Hom.toFunctor (eId Cat a))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) } ≫
        f'))
    (hComp (Functor.map (Cat.Hom.toFunctor (eId Cat a)) (𝟙 { down := { as := () } })) η) η

Tactic:
exact congr_arg_heq (·.toFunctor.map η) (e_id_comp (V := Cat) a b)

Premises used: CategoryTheory.e_id_comp, congr_arg_heq, CategoryTheory.Cat
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ Eq (α := 𝟙 a ≫ f ⟶ 𝟙 a ≫ f') (hComp (𝟙 (𝟙 a)) η) (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)

Tactic:
simp [← heq_eq_eq, id_hComp_heq]

Premises used: CategoryTheory.CatEnriched.id_hComp_heq, heq_eq_eq
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
rw :
  HEq (α :=
    f ≫
        Functor.obj (Cat.Hom.toFunctor (eId Cat b))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) } ⟶
      f' ≫
        Functor.obj (Cat.Hom.toFunctor (eId Cat b))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) })
    (hComp η (Functor.map (Cat.Hom.toFunctor (eId Cat b)) (𝟙 { down := { as := () } }))) η
⊢ HEq (α := f ≫ 𝟙 b ⟶ f' ≫ 𝟙 b) (hComp η (𝟙 (𝟙 b))) η

Tactic:
rw [id_eq, ← Functor.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.CatEnriched.id_eq
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ HEq (α :=
    f ≫
        Functor.obj (Cat.Hom.toFunctor (eId Cat b))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) } ⟶
      f' ≫
        Functor.obj (Cat.Hom.toFunctor (eId Cat b))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) })
    (hComp η (Functor.map (Cat.Hom.toFunctor (eId Cat b)) (𝟙 { down := { as := () } }))) η

Tactic:
congr_arg_heq (·.toFunctor.map η) (e_comp_id (V := Cat) a b)

Premises used: CategoryTheory.e_comp_id, congr_arg_heq, CategoryTheory.CatEnriched.hComp, CategoryTheory.Cat