awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
rw : f ◁ (η.inv ≫ η.hom) = 𝟙 (f ≫ h)
rw₁ : f ◁ 𝟙 h = 𝟙 (f ≫ h)
⊢ f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)
have rw₂ : 𝟙 (f ≫ h) = 𝟙 (f ≫ h)
Tactic: rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
⊢ η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h)
have rw : (η.inv ≫ η.hom) ▷ h = 𝟙 (g ≫ h)
Tactic: rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
rw : (η.inv ≫ η.hom) ▷ h = 𝟙 (g ≫ h)
⊢ η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h)
have rw₁ : 𝟙 g ▷ h = 𝟙 (g ≫ h)
Tactic: rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
rw : (η.inv ≫ η.hom) ▷ h = 𝟙 (g ≫ h)
rw₁ : 𝟙 g ▷ h = 𝟙 (g ≫ h)
⊢ η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h)
have rw₂ : 𝟙 (g ≫ h) = 𝟙 (g ≫ h)
Tactic: rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst_1 : IsIso η
⊢ inv (f ◁ η) = f ◁ inv η
have hom_inv_id : f ◁ η ≫ f ◁ inv η = 𝟙 (f ≫ g)
Tactic: apply IsIso.inv_eq_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst_1 : IsIso η
⊢ inv (η ▷ h) = inv η ▷ h
have hom_inv_id : η ▷ h ≫ inv η ▷ h = 𝟙 (f ≫ h)
Tactic: apply IsIso.inv_eq_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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).inv ▷ i ≫ (α_ (f ≫ g) h i).hom = f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv
have 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
Tactic: rw [← cancel_epi (f ◁ (α_ g h i).inv), ← cancel_mono (α_ (f ≫ g) h i).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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).hom ▷ i
have 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
Tactic: rw [← cancel_epi (α_ f g (h ≫ i)).inv, ← cancel_mono ((α_ f g h).inv ▷ i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom
have rw : (α_ f (𝟙 b) g).inv ≫ (α_ f (𝟙 b) g).hom ≫ f ◁ (λ_ g).hom = f ◁ (λ_ g).hom
Tactic: rw [← triangle, inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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
⊢ (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom
have rw₁ : f ◁ (λ_ g).hom = f ◁ (λ_ g).hom
Tactic: rw [← triangle, inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ f).hom ▷ g = hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom
have rw : Eq (α := 𝟙 a ≫ (𝟙 a ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g) (𝟙 a ◁ (λ_ f).hom ▷ g) (𝟙 a ◁ (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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))
⊢ (λ_ f).hom ▷ g = hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom
have rw₁ : Eq (α := 𝟙 a ≫ (𝟙 a ≫ f) ≫ g ⟶ 𝟙 a ≫ f ≫ g) (𝟙 a ◁ (λ_ f).hom ▷ g) (𝟙 a ◁ hom (α_ (𝟙 a) f g) ≫ 𝟙 a ◁ (λ_ (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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)
⊢ (λ_ f).hom ▷ g = hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom
have 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)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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)
⊢ (λ_ f).hom ▷ g = hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom
have 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)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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)
⊢ (λ_ f).hom ▷ g = hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom
have 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)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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)
⊢ (λ_ f).hom ▷ g = hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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))
⊢ (λ_ f).hom ▷ g = hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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))
⊢ (λ_ f).hom ▷ g = hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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))
⊢ (λ_ f).hom ▷ g = hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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))
⊢ (λ_ f).hom ▷ g = hom (α_ (𝟙 a) f g) ≫ (λ_ (f ≫ g)).hom
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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)).inv ≫ (ρ_ (f ≫ g)).hom
have rw : (f ◁ (ρ_ g).hom) ▷ 𝟙 c = ((α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom) ▷ 𝟙 c
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom
have rw₁ : (f ◁ (ρ_ g).hom) ▷ 𝟙 c = (α_ f g (𝟙 c)).inv ▷ 𝟙 c ≫ (ρ_ (f ≫ g)).hom ▷ 𝟙 c
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom
have rw₂ : (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
  (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (α_ f g (𝟙 c)).inv ▷ 𝟙 c ≫ (ρ_ (f ≫ g)).hom ▷ 𝟙 c
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom
have 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
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom
have 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
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom
have rw₅ : f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
  (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ hom (λ_ (𝟙 c))
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]