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 : 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))
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom
have rw₆ : f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ f ◁ (ρ_ g).hom ▷ 𝟙 c ≫ (α_ f g (𝟙 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
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))
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom
have rw₇ : f ◁ ((α_ g (𝟙 c) (𝟙 c)).inv ≫ (ρ_ g).hom ▷ 𝟙 c) ≫ (α_ f g (𝟙 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
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))
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom
have rw₈ : f ◁ g ◁ hom (λ_ (𝟙 c)) ≫ (α_ f g (𝟙 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
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))
⊢ 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) ◁ 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
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a)) (hom (λ_ (𝟙 a))) (hom (ρ_ (𝟙 a)))
have rw : Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a ≫ 𝟙 a) (𝟙 a ≫ 𝟙 a)) (𝟙 a ◁ hom (λ_ (𝟙 a)))
  (𝟙 a ◁ hom (ρ_ (𝟙 a)))
Tactic: rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ←
      rightUnitor_comp, rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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)))
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a)) (hom (λ_ (𝟙 a))) (hom (ρ_ (𝟙 a)))
have 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)))
Tactic: rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ←
      rightUnitor_comp, rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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)))
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a)) (hom (λ_ (𝟙 a))) (hom (ρ_ (𝟙 a)))
have 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)))
Tactic: rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ←
      rightUnitor_comp, rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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)))
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a)) (hom (λ_ (𝟙 a))) (hom (ρ_ (𝟙 a)))
have 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)))
Tactic: rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ←
      rightUnitor_comp, rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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)))
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a)) (hom (λ_ (𝟙 a))) (hom (ρ_ (𝟙 a)))
have 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)))
Tactic: rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ←
      rightUnitor_comp, rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
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)))
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a)) (hom (λ_ (𝟙 a))) (hom (ρ_ (𝟙 a)))
have 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)))
Tactic: rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ←
      rightUnitor_comp, rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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'
⊢ hComp (eqToHom α) (eqToHom β) = eqToHom ⋯
have refl : hComp (eqToHom sorry) (eqToHom β) = eqToHom sorry
Tactic: cases α
Cleared hypotheses: f', α
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom ⋯) (eqToHom β) = eqToHom ⋯
have refl : hComp (eqToHom sorry) (eqToHom sorry) = eqToHom sorry
Tactic: cases β
Cleared hypotheses: g', β
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ HEq (α := 𝟙 a ≫ f ⟶ 𝟙 a ≫ f') (hComp (𝟙 (𝟙 a)) η) η
have 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 := () } })) η) η
Tactic: rw [id_eq, ← Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ HEq (α := f ≫ 𝟙 b ⟶ f' ≫ 𝟙 b) (hComp η (𝟙 (𝟙 b))) η
have 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 := () } }))) η
Tactic: rw [id_eq, ← Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c d e : CatEnriched C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ Eq (α := ((f ≫ g) ≫ h) ≫ i ⟶ f ≫ g ≫ h ≫ i)
    (CategoryStruct.comp (Y := (f ≫ g ≫ h) ≫ i) (hComp (Iso.hom (eqToIso ⋯)) (𝟙 i))
      (CategoryStruct.comp (Y := f ≫ (g ≫ h) ≫ i) (Iso.hom (eqToIso ⋯)) (hComp (𝟙 f) (Iso.hom (eqToIso ⋯)))))
    (CategoryStruct.comp (Y := (f ≫ g) ≫ h ≫ i) (Iso.hom (eqToIso ⋯)) (Iso.hom (eqToIso ⋯)))
have generalize_proofs : ∀ (h1 : (f ≫ g) ≫ h = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i) (h3 : (g ≫ h) ≫ i = g ≫ h ≫ i)
  (h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i) (pf : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i),
  hComp (Iso.hom (eqToIso h1)) (𝟙 i) ≫ Iso.hom (eqToIso h2) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h3)) =
    Iso.hom (eqToIso h4) ≫ Iso.hom (eqToIso pf)
Tactic: generalize_proofs h1 h2 h3 h4
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c d e : CatEnriched C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
h1 : (f ≫ g) ≫ h = f ≫ g ≫ h
h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i
h3 : (g ≫ h) ≫ i = g ≫ h ≫ i
h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i
pf : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
⊢ hComp (Iso.hom (eqToIso h1)) (𝟙 i) ≫ Iso.hom (eqToIso h2) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h3)) =
    Iso.hom (eqToIso h4) ≫ Iso.hom (eqToIso pf)
have revert : ∀ (h1 : (f ≫ g) ≫ h = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i) (h3 : (g ≫ h) ≫ i = g ≫ h ≫ i)
  (h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i),
  hComp (Iso.hom (eqToIso h1)) (𝟙 i) ≫ Iso.hom (eqToIso h2) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h3)) =
    Iso.hom (eqToIso h4) ≫ Iso.hom (eqToIso pf)
Tactic: revert h1 h2 h3 h4
Cleared hypotheses: h1, h2, h3, h4
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c d e : CatEnriched C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
pf : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
⊢ ∀ (h1 : (f ≫ g) ≫ h = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i) (h3 : (g ≫ h) ≫ i = g ≫ h ≫ i)
    (h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i),
    hComp (Iso.hom (eqToIso h1)) (𝟙 i) ≫ Iso.hom (eqToIso h2) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h3)) =
      Iso.hom (eqToIso h4) ≫ Iso.hom (eqToIso pf)
have generalize : ∀ (x : a ⟶ d) (w : b ⟶ e) (h1 : x = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ w) (h3 : w = g ≫ h ≫ i)
  (h4 : x ≫ i = (f ≫ g) ≫ h ≫ i),
  hComp (Iso.hom (eqToIso h1)) (𝟙 i) ≫ Iso.hom (eqToIso h2) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h3)) =
    Iso.hom (eqToIso h4) ≫ Iso.hom (eqToIso pf)
Tactic: generalize (f ≫ g) ≫ h = x, (g ≫ h) ≫ i = w
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g : b ⟶ c
⊢ Eq.{u_3 + 1} (α := (f ≫ 𝟙 b) ≫ g ⟶ f ≫ g)
    (CategoryStruct.comp (Y := f ≫ 𝟙 b ≫ g) (Iso.hom (eqToIso ⋯)) (hComp (𝟙 f) (Iso.hom (eqToIso ⋯))) :
      (f ≫ 𝟙 b) ≫ g ⟶ f ≫ g)
    (hComp (Iso.hom (eqToIso ⋯)) (𝟙 g) : (f ≫ 𝟙 b) ≫ g ⟶ f ≫ g)
have generalize_proofs : ∀ (h1 : (f ≫ 𝟙 b) ≫ g = f ≫ 𝟙 b ≫ g) (h2 : 𝟙 b ≫ g = g) (h3 : f ≫ 𝟙 b = f),
  Iso.hom (eqToIso h1) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h2)) = hComp (Iso.hom (eqToIso h3)) (𝟙 g)
Tactic: generalize_proofs h1 h2 h3
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g : b ⟶ c
h1 : (f ≫ 𝟙 b) ≫ g = f ≫ 𝟙 b ≫ g
h2 : 𝟙 b ≫ g = g
h3 : f ≫ 𝟙 b = f
⊢ Iso.hom (eqToIso h1) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h2)) = hComp (Iso.hom (eqToIso h3)) (𝟙 g)
have revert : ∀ (h1 : (f ≫ 𝟙 b) ≫ g = f ≫ 𝟙 b ≫ g) (h2 : 𝟙 b ≫ g = g) (h3 : f ≫ 𝟙 b = f),
  Iso.hom (eqToIso h1) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h2)) = hComp (Iso.hom (eqToIso h3)) (𝟙 g)
Tactic: revert h1 h2 h3
Cleared hypotheses: h1, h2, h3
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g : b ⟶ c
⊢ ∀ (h1 : (f ≫ 𝟙 b) ≫ g = f ≫ 𝟙 b ≫ g) (h2 : 𝟙 b ≫ g = g) (h3 : f ≫ 𝟙 b = f),
    Iso.hom (eqToIso h1) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h2)) = hComp (Iso.hom (eqToIso h3)) (𝟙 g)
have generalize : ∀ (g_1 : b ⟶ c) (f_1 : a ⟶ b) (h1 : f_1 ≫ g = f ≫ g_1) (h2 : g_1 = g) (h3 : f_1 = f),
  Iso.hom (eqToIso h1) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h2)) = hComp (Iso.hom (eqToIso h3)) (𝟙 g)
Tactic: generalize 𝟙 _ ≫ g = g, f ≫ 𝟙 _ = f
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
⊢ Eq.{u' + 1} (α := a.toBase ⟶ a.toBase)
    ((Equiv.trans (eHomEquiv Cat)
            (Equiv.trans
              (Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a a))
              Cat.fromChosenTerminalEquiv) :
          (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase)
        (𝟙 a) :
      a.toBase ⟶ a.toBase)
    (𝟙 a.toBase : a.toBase ⟶ a.toBase)
have simp : Eq.{u' + 1} (α := a.toBase ⟶ a.toBase)
  ((Cat.fromChosenTerminalEquiv :
        (a_1 : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u')) → a.toBase ⟶ a.toBase)
      ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
            (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a a) :
          (a_1 : MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] a) →
            (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u'))
        ((eHomEquiv Cat : (a_1 : a ⟶ a) → MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] a) (𝟙 a))) :
    a.toBase ⟶ a.toBase)
  (𝟙 a.toBase : a.toBase ⟶ a.toBase)
Tactic: simp only [Equiv.trans_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
⊢ Eq.{u' + 1} (α := a.toBase ⟶ a.toBase)
    ((Cat.fromChosenTerminalEquiv :
          (a_1 : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u')) →
            a.toBase ⟶ a.toBase)
        ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
              (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a a) :
            (a_1 : MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] a) →
              (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u'))
          ((eHomEquiv Cat : (a_1 : a ⟶ a) → MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] a) (𝟙 a))) :
      a.toBase ⟶ a.toBase)
    (𝟙 a.toBase : a.toBase ⟶ a.toBase)
have rw : Eq.{u' + 1} (α := a.toBase ⟶ a.toBase)
  ((Cat.fromChosenTerminalEquiv :
        (a_1 : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u')) → a.toBase ⟶ a.toBase)
      ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
            (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a a) :
          (a_1 : MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] a) →
            (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u'))
        (eId Cat a)) :
    a.toBase ⟶ a.toBase)
  (𝟙 a.toBase : a.toBase ⟶ a.toBase)
Tactic: rw [eHomEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
⊢ Eq.{u' + 1} (α := a.toBase ⟶ c.toBase)
    ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f ≫ g) : a.toBase ⟶ c.toBase)
    (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f)
        ((homEquiv : (a : b ⟶ c) → b.toBase ⟶ c.toBase) g) :
      a.toBase ⟶ c.toBase)
have unfold : Eq.{u' + 1} (α := a.toBase ⟶ c.toBase)
  ((Equiv.trans (eHomEquiv Cat)
          (Equiv.trans
            (Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
              (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a c))
            Cat.fromChosenTerminalEquiv) :
        (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase)
      (f ≫ g) :
    a.toBase ⟶ c.toBase)
  (CategoryStruct.comp (Y := b.toBase)
      ((Equiv.trans (eHomEquiv Cat)
            (Equiv.trans
              (Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a b))
              Cat.fromChosenTerminalEquiv) :
          (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase)
        f)
      ((Equiv.trans (eHomEquiv Cat)
            (Equiv.trans
              (Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ b c))
              Cat.fromChosenTerminalEquiv) :
          (a : b ⟶ c) → b.toBase ⟶ c.toBase)
        g) :
    a.toBase ⟶ c.toBase)
Tactic: unfold homEquiv