awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
⊢ Eq (α :=
    Quiver.Hom (V := a ⟶ b) (𝟙 a ≫ Functor.obj (𝟭 (a ⟶ b)) f)
      (Functor.obj
        (Functor.comp (D :=
          Prefunctor.obj
              (PrelaxFunctorStruct.toPrefunctor
                (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
              a ⟶
            Prefunctor.obj
              (PrelaxFunctorStruct.toPrefunctor
                (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
              b)
          (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
        g))
    (CategoryStruct.comp (Y := 𝟙 a ≫ Functor.obj (𝟭 (a ⟶ b)) g) (𝟙 a ◁ Functor.map (𝟭 (a ⟶ b)) η)
        (Iso.hom (normalizeIso nil g)) :
      Quiver.Hom (V := a ⟶ b) (𝟙 a ≫ Functor.obj (𝟭 (a ⟶ b)) f)
        (Functor.obj
          (Functor.comp (D :=
            Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                a ⟶
              Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                b)
            (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
          g))
    (Iso.hom (normalizeIso nil f) ≫
        Functor.map
          (Functor.comp (D :=
            Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                a ⟶
              Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                b)
            (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
          η :
      Quiver.Hom (V := a ⟶ b) (𝟙 a ≫ f : a ⟶ b)
        (Functor.obj
          (Functor.comp (D :=
            Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                a ⟶
              Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                b)
            (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
          g))

Tactic:
exact normalize_naturality nil η

Premises used: Quiver.Path.nil, CategoryTheory.FreeBicategory.normalize_naturality
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : B
f : Discrete (Path.{v, u} a b)
obtain :
  ∀ (f : Path.{v, u} a b),
    Functor.obj (inclusionPath a b ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b)
        { as := f : Discrete (Path.{v, u} a b) } =
      Functor.obj (𝟭 (Discrete (Path.{v, u} a b))) { as := f : Discrete (Path.{v, u} a b) }
⊢ Functor.obj (inclusionPath a b ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) f =
    Functor.obj (𝟭 (Discrete (Path.{v, u} a b))) f

Tactic:
obtain ⟨f⟩ := f
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : B
⊢ Eq (α := Discrete (Path.{v, u} a a))
    (Functor.obj (C := Discrete (Path.{v, u} a a))
        (inclusionPath a a ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a a) { as := nil } :
      Discrete (Path.{v, u} a a))
    (Functor.obj (𝟭 (Discrete (Path.{v, u} a a))) { as := nil } : Discrete (Path.{v, u} a a))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b b_1 c : B
a_1 : Path.{v, u} a b_1
a_2 : b_1 ⟶ c
ih :
  Functor.obj (inclusionPath a b_1 ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b_1)
      { as := a_1 : Discrete (Path.{v, u} a b_1) } =
    Functor.obj (𝟭 (Discrete (Path.{v, u} a b_1))) { as := a_1 : Discrete (Path.{v, u} a b_1) }
cons :
  Discrete.as
      (Functor.obj (inclusionPath a c ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a c)
        { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) }) =
    (Functor.obj (𝟭 (Discrete (Path.{v, u} a c))) { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) }).as
⊢ Functor.obj (inclusionPath a c ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a c)
      { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) } =
    Functor.obj (𝟭 (Discrete (Path.{v, u} a c))) { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) }

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b b_1 c : B
a_1 : Path.{v, u} a b_1
a_2 : b_1 ⟶ c
ih :
  Functor.obj (inclusionPath a b_1 ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b_1)
      { as := a_1 : Discrete (Path.{v, u} a b_1) } =
    Functor.obj (𝟭 (Discrete (Path.{v, u} a b_1))) { as := a_1 : Discrete (Path.{v, u} a b_1) }
⊢ normalizeAux nil (Functor.obj (inclusionPath a b_1) { as := a_1 : Discrete (Path.{v, u} a b_1) }) = a_1

Tactic:
injection ih with ih
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b b_1 c : B
a_1 : Path.{v, u} a b_1
a_2 : b_1 ⟶ c
ih : normalizeAux nil (Functor.obj (inclusionPath a b_1) { as := a_1 : Discrete (Path.{v, u} a b_1) }) = a_1
rw :
  (Functor.obj (𝟭 (Discrete (Path.{v, u} a c)))
      {
        as :=
          (normalizeAux nil (Functor.obj (inclusionPath a b_1) { as := a_1 : Discrete (Path.{v, u} a b_1) })).cons a_2 :
        Discrete (Path.{v, u} a c) }).as
| (Functor.obj (𝟭 (Discrete (Path.{v, u} a c))) { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) }).as

Tactic:
rw [← ih]
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b b_1 c : B
a_1 : Path.{v, u} a b_1
a_2 : b_1 ⟶ c
ih : normalizeAux nil (Functor.obj (inclusionPath a b_1) { as := a_1 : Discrete (Path.{v, u} a b_1) }) = a_1
cons :
  Discrete.as
      (Functor.obj (inclusionPath a c ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a c)
        { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) }) =
    (Functor.obj (𝟭 (Discrete (Path.{v, u} a c)))
        {
          as :=
            (normalizeAux nil (Functor.obj (inclusionPath a b_1) { as := a_1 : Discrete (Path.{v, u} a b_1) })).cons
              a_2 :
          Discrete (Path.{v, u} a c) }).as
⊢ Discrete.as
      (Functor.obj (inclusionPath a c ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a c)
        { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) }) =
    (Functor.obj (𝟭 (Discrete (Path.{v, u} a c))) { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) }).as

Tactic:
conv_rhs => rw [← ih]
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b b_1 c : B
a_1 : Path.{v, u} a b_1
a_2 : b_1 ⟶ c
ih : normalizeAux nil (Functor.obj (inclusionPath a b_1) { as := a_1 : Discrete (Path.{v, u} a b_1) }) = a_1
⊢ Discrete.as
      (Functor.obj (inclusionPath a c ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a c)
        { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) }) =
    (Functor.obj (𝟭 (Discrete (Path.{v, u} a c)))
        {
          as :=
            (normalizeAux nil (Functor.obj (inclusionPath a b_1) { as := a_1 : Discrete (Path.{v, u} a b_1) })).cons
              a_2 :
          Discrete (Path.{v, u} a c) }).as

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : B
f : Path.{v, u} a b
nil :
  Eq (α := Discrete (Path.{v, u} a a))
    (Functor.obj (C := Discrete (Path.{v, u} a a))
        (inclusionPath a a ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a a)
        { as := Path.nil } :
      Discrete (Path.{v, u} a a))
    (Functor.obj (𝟭 (Discrete (Path.{v, u} a a))) { as := Path.nil } : Discrete (Path.{v, u} a a))
cons :
  ∀ {b c : B} (a_1 : Path.{v, u} a b) (a_2 : b ⟶ c)
    (ih :
      Functor.obj (inclusionPath a b ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b)
          { as := a_1 : Discrete (Path.{v, u} a b) } =
        Functor.obj (𝟭 (Discrete (Path.{v, u} a b))) { as := a_1 : Discrete (Path.{v, u} a b) }),
    Functor.obj (inclusionPath a c ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a c)
        { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) } =
      Functor.obj (𝟭 (Discrete (Path.{v, u} a c))) { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) }
⊢ Functor.obj (inclusionPath a b ⋙ PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b)
      { as := f : Discrete (Path.{v, u} a b) } =
    Functor.obj (𝟭 (Discrete (Path.{v, u} a b))) { as := f : Discrete (Path.{v, u} a b) }

Tactic:
induction f with
      | nil => rfl
      | cons _ _ ih =>
        ext1 -- Porting note: `tidy` closes the goal in mathlib3 but `aesop` doesn't here.
        injection ih with ih
        conv_rhs => rw [← ih]
        rfl

Premises used: Quiver.Path.nil, Quiver.Path.cons
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
⊢ Quiver.IsThin (a ⟶ b)

Tactic:
fun _ _ =>
  ⟨fun _ _ =>
    (@normalizeEquiv B _ a b).functor.map_injective (Subsingleton.elim _ _)⟩

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map, Subsingleton.intro, CategoryTheory.FreeBicategory.normalizeEquiv, CategoryTheory.Functor.map_injective, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Bicategory.End
Goal:
C : Type u
inst : Bicategory.{w, v, u} C
X : C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : X ⟶ X
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
dsimp : (f₁ ▷ X₂ ≫ Y₁ ◁ f₂) ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ≫ g₁) ▷ X₂ ≫ Z₁ ◁ (f₂ ≫ g₂)
⊢ Eq.{w + 1} (α := X₁ ≫ X₂ ⟶ Z₁ ≫ Z₂)
    (CategoryStruct.comp (Y := Y₁ ≫ Y₂)
      (CategoryStruct.comp (Y := (fun (f g : X ⟶ X) ↦ f ≫ g) Y₁ X₂)
        ((fun {x x_1 : X ⟶ X} (η : x ⟶ x_1) (h : X ⟶ X) ↦ η ▷ h) f₁ X₂)
        ((fun {f x x_1 : X ⟶ X} (η : x ⟶ x_1) ↦ f ◁ η) f₂))
      (CategoryStruct.comp (Y := (fun (f g : X ⟶ X) ↦ f ≫ g) Z₁ Y₂)
        ((fun {x x_1 : X ⟶ X} (η : x ⟶ x_1) (h : X ⟶ X) ↦ η ▷ h) g₁ Y₂)
        ((fun {f x x_1 : X ⟶ X} (η : x ⟶ x_1) ↦ f ◁ η) g₂)))
    (CategoryStruct.comp (Y := (fun (f g : X ⟶ X) ↦ f ≫ g) Z₁ X₂)
      ((fun {x x_1 : X ⟶ X} (η : x ⟶ x_1) (h : X ⟶ X) ↦ η ▷ h) (f₁ ≫ g₁) X₂)
      ((fun {f x x_1 : X ⟶ X} (η : x ⟶ x_1) ↦ f ◁ η) (f₂ ≫ g₂)))

Tactic:
dsimp only
-- Module: Mathlib.CategoryTheory.Bicategory.End
Goal:
C : Type u
inst : Bicategory.{w, v, u} C
X : C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : X ⟶ X
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
rw : (f₁ ▷ X₂ ≫ Y₁ ◁ f₂) ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ≫ g₁) ▷ X₂ ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂
rw₁ : (f₁ ▷ X₂ ≫ Y₁ ◁ f₂) ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ▷ X₂ ≫ g₁ ▷ X₂) ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂
rw₂ : f₁ ▷ X₂ ≫ Y₁ ◁ f₂ ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ▷ X₂ ≫ g₁ ▷ X₂) ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂
rw₃ : f₁ ▷ X₂ ≫ Y₁ ◁ f₂ ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = f₁ ▷ X₂ ≫ g₁ ▷ X₂ ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂
rw₄ rw₅ : f₁ ▷ X₂ ≫ g₁ ▷ X₂ ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂ = f₁ ▷ X₂ ≫ g₁ ▷ X₂ ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂
⊢ (f₁ ▷ X₂ ≫ Y₁ ◁ f₂) ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ≫ g₁) ▷ X₂ ≫ Z₁ ◁ (f₂ ≫ g₂)

Tactic:
rw [Bicategory.whiskerLeft_comp, Bicategory.comp_whiskerRight, Category.assoc, Category.assoc,
      Bicategory.whisker_exchange_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Bicategory.whiskerLeft_comp, CategoryTheory.Bicategory.comp_whiskerRight, CategoryTheory.Bicategory.whisker_exchange_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x : B
⊢ Eq.{w + 1} (α := Iso.{w, v} (C := x ⟶ x) (eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom ⋯)) (eqToHomTransIso ⋯ ⋯)
    (Iso.symm (λ_ (𝟙 x)))

Tactic:
rfl

Premises used: CategoryTheory.Bicategory.eqToHomTransIso, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
e₁ : x = y
w :
  Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ y) (eqToHom ⋯) (eqToHom e₁ ≫ eqToHom ⋯)) (Iso.hom (eqToHomTransIso e₁ ⋯))
    (Iso.hom (Iso.symm (ρ_ (eqToHom e₁))))
⊢ Eq.{w + 1} (α := Iso.{w, v} (C := x ⟶ y) (eqToHom ⋯) (eqToHom e₁ ≫ eqToHom ⋯)) (eqToHomTransIso e₁ ⋯)
    (Iso.symm (ρ_ (eqToHom e₁)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
e₁ : x = y
w :
  Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ x) (eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom ⋯)) (Iso.hom (eqToHomTransIso ⋯ ⋯))
    (Iso.hom (Iso.symm (ρ_ (eqToHom ⋯))))
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ y) (eqToHom ⋯) (eqToHom e₁ ≫ eqToHom ⋯)) (Iso.hom (eqToHomTransIso e₁ ⋯))
    (Iso.hom (Iso.symm (ρ_ (eqToHom e₁))))

Tactic:
subst e₁
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x : B
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ x) (eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom ⋯)) (Iso.hom (eqToHomTransIso ⋯ ⋯))
    (Iso.hom (Iso.symm (ρ_ (eqToHom ⋯))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
e₁ : x = y
w :
  Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ y) (eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom e₁)) (Iso.hom (eqToHomTransIso ⋯ e₁))
    (Iso.hom (Iso.symm (λ_ (eqToHom e₁))))
⊢ Eq.{w + 1} (α := Iso.{w, v} (C := x ⟶ y) (eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom e₁)) (eqToHomTransIso ⋯ e₁)
    (Iso.symm (λ_ (eqToHom e₁)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
e₁ : x = y
w :
  Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ x) (eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom ⋯)) (Iso.hom (eqToHomTransIso ⋯ ⋯))
    (Iso.hom (Iso.symm (λ_ (eqToHom ⋯))))
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ y) (eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom e₁)) (Iso.hom (eqToHomTransIso ⋯ e₁))
    (Iso.hom (Iso.symm (λ_ (eqToHom e₁))))

Tactic:
subst e₁
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x : B
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ x) (eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom ⋯)) (Iso.hom (eqToHomTransIso ⋯ ⋯))
    (Iso.hom (Iso.symm (λ_ (eqToHom ⋯))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
e₁ : x = y
e₂ : y = z
e₃ : z = t
subst_vars :
  Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := t ⟶ t) ((eqToHom ⋯ ≫ eqToHom ⋯) ≫ eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom ⋯ ≫ eqToHom ⋯))
    (Iso.hom (α_ (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯)))
    (Iso.inv (eqToHomTransIso ⋯ ⋯) ▷ eqToHom ⋯ ≫
      Iso.inv (eqToHomTransIso ⋯ ⋯) ≫ Iso.hom (eqToHomTransIso ⋯ ⋯) ≫ eqToHom ⋯ ◁ Iso.hom (eqToHomTransIso ⋯ ⋯))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := x ⟶ t) ((eqToHom e₁ ≫ eqToHom e₂) ≫ eqToHom e₃) (eqToHom e₁ ≫ eqToHom e₂ ≫ eqToHom e₃))
    (Iso.hom (α_ (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)))
    (Iso.inv (eqToHomTransIso e₁ e₂) ▷ eqToHom e₃ ≫
      Iso.inv (eqToHomTransIso ⋯ e₃) ≫ Iso.hom (eqToHomTransIso e₁ ⋯) ≫ eqToHom e₁ ◁ Iso.hom (eqToHomTransIso e₂ e₃))

Tactic:
subst_vars
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
t : B
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := t ⟶ t) ((eqToHom ⋯ ≫ eqToHom ⋯) ≫ eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom ⋯ ≫ eqToHom ⋯))
    (Iso.hom (α_ (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯)))
    (Iso.inv (eqToHomTransIso ⋯ ⋯) ▷ eqToHom ⋯ ≫
      Iso.inv (eqToHomTransIso ⋯ ⋯) ≫ Iso.hom (eqToHomTransIso ⋯ ⋯) ≫ eqToHom ⋯ ◁ Iso.hom (eqToHomTransIso ⋯ ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
e₁ : x = y
e₂ : y = z
e₃ : z = t
subst_vars :
  Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := t ⟶ t) (eqToHom ⋯ ≫ eqToHom ⋯ ≫ eqToHom ⋯) ((eqToHom ⋯ ≫ eqToHom ⋯) ≫ eqToHom ⋯))
    (Iso.inv (α_ (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯)))
    (eqToHom ⋯ ◁ Iso.inv (eqToHomTransIso ⋯ ⋯) ≫
      Iso.inv (eqToHomTransIso ⋯ ⋯) ≫ Iso.hom (eqToHomTransIso ⋯ ⋯) ≫ Iso.hom (eqToHomTransIso ⋯ ⋯) ▷ eqToHom ⋯)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := x ⟶ t) (eqToHom e₁ ≫ eqToHom e₂ ≫ eqToHom e₃) ((eqToHom e₁ ≫ eqToHom e₂) ≫ eqToHom e₃))
    (Iso.inv (α_ (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)))
    (eqToHom e₁ ◁ Iso.inv (eqToHomTransIso e₂ e₃) ≫
      Iso.inv (eqToHomTransIso e₁ ⋯) ≫ Iso.hom (eqToHomTransIso ⋯ e₃) ≫ Iso.hom (eqToHomTransIso e₁ e₂) ▷ eqToHom e₃)

Tactic:
subst_vars
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
t : B
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := t ⟶ t) (eqToHom ⋯ ≫ eqToHom ⋯ ≫ eqToHom ⋯) ((eqToHom ⋯ ≫ eqToHom ⋯) ≫ eqToHom ⋯))
    (Iso.inv (α_ (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯)))
    (eqToHom ⋯ ◁ Iso.inv (eqToHomTransIso ⋯ ⋯) ≫
      Iso.inv (eqToHomTransIso ⋯ ⋯) ≫ Iso.hom (eqToHomTransIso ⋯ ⋯) ≫ Iso.hom (eqToHomTransIso ⋯ ⋯) ▷ eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ (f ≫ g) ≫ h = (f' ≫ g') ≫ h'

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ f' ≫ g' ≫ h' = f ≫ g ≫ h

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
subst_vars : (α_ f' g' h').hom = eqToHom ⋯ ≫ (α_ f' g' h').hom ≫ eqToHom ⋯
⊢ (α_ f g h).hom = eqToHom ⋯ ≫ (α_ f' g' h').hom ≫ eqToHom ⋯

Tactic:
subst_vars
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
f' : x ⟶ y
g' : y ⟶ z
h' : z ⟶ t
⊢ (α_ f' g' h').hom = eqToHom ⋯ ≫ (α_ f' g' h').hom ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ f ≫ g ≫ h = f' ≫ g' ≫ h'

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ (f' ≫ g') ≫ h' = (f ≫ g) ≫ h

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
subst_vars : (α_ f' g' h').inv = eqToHom ⋯ ≫ (α_ f' g' h').inv ≫ eqToHom ⋯
⊢ (α_ f g h).inv = eqToHom ⋯ ≫ (α_ f' g' h').inv ≫ eqToHom ⋯

Tactic:
subst_vars
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
f' : x ⟶ y
g' : y ⟶ z
h' : z ⟶ t
⊢ (α_ f' g' h').inv = eqToHom ⋯ ≫ (α_ f' g' h').inv ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
rw rw₁ : f' ≫ g = f' ≫ g
⊢ f ≫ g = f' ≫ g

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
rw rw₁ : f' ≫ g' = f' ≫ g'
⊢ f' ≫ g' = f ≫ g'

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
subst : f ◁ η = eqToHom ⋯ ≫ f ◁ η ≫ eqToHom ⋯
⊢ f ◁ η = eqToHom ⋯ ≫ f' ◁ η ≫ eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f : x ⟶ y
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f ◁ η = eqToHom ⋯ ≫ f ◁ η ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
rw rw₁ : f ≫ g' = f ≫ g'
⊢ f ≫ g = f ≫ g'

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
rw rw₁ : f' ≫ g' = f' ≫ g'
⊢ f' ≫ g' = f' ≫ g

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
subst : η ▷ g = eqToHom ⋯ ≫ η ▷ g ≫ eqToHom ⋯
⊢ η ▷ g = eqToHom ⋯ ≫ η ▷ g' ≫ eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
y z : B
g : y ⟶ z
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ η ▷ g = eqToHom ⋯ ≫ η ▷ g ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f f' : x ⟶ y
h : f = f'
subst : (λ_ f).hom = 𝟙 x ◁ eqToHom ⋯ ≫ (λ_ f).hom ≫ eqToHom ⋯
⊢ (λ_ f).hom = 𝟙 x ◁ eqToHom h ≫ (λ_ f').hom ≫ eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f : x ⟶ y
⊢ (λ_ f).hom = 𝟙 x ◁ eqToHom ⋯ ≫ (λ_ f).hom ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f f' : x ⟶ y
h : f = f'
subst : (λ_ f).inv = eqToHom ⋯ ≫ (λ_ f).inv ≫ 𝟙 x ◁ eqToHom ⋯
⊢ (λ_ f).inv = eqToHom h ≫ (λ_ f').inv ≫ 𝟙 x ◁ eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f : x ⟶ y
⊢ (λ_ f).inv = eqToHom ⋯ ≫ (λ_ f).inv ≫ 𝟙 x ◁ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f f' : x ⟶ y
h : f = f'
subst : (ρ_ f).hom = eqToHom ⋯ ▷ 𝟙 y ≫ (ρ_ f).hom ≫ eqToHom ⋯
⊢ (ρ_ f).hom = eqToHom h ▷ 𝟙 y ≫ (ρ_ f').hom ≫ eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f : x ⟶ y
⊢ (ρ_ f).hom = eqToHom ⋯ ▷ 𝟙 y ≫ (ρ_ f).hom ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f f' : x ⟶ y
h : f = f'
subst : (ρ_ f).inv = eqToHom ⋯ ≫ (ρ_ f).inv ≫ eqToHom ⋯ ▷ 𝟙 y
⊢ (ρ_ f).inv = eqToHom h ≫ (ρ_ f').inv ≫ eqToHom ⋯ ▷ 𝟙 y

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Bicategory.EqToHom
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f : x ⟶ y
⊢ (ρ_ f).inv = eqToHom ⋯ ≫ (ρ_ f).inv ≫ eqToHom ⋯ ▷ 𝟙 y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
η : s ⟶ t
⊢ s.unit ≫ f ◁ StructuredArrow.Hom.right η = t.unit

Tactic:
StructuredArrow.w η

Premises used: CategoryTheory.StructuredArrow.w
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
x : B
h : c ⟶ x
⊢ (t.whisker h).extension = t.extension ≫ h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
x : B
h : c ⟶ x
⊢ (t.whisker h).unit = t.unit ▷ h ≫ (α_ f t.extension h).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Extension
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
x : B
h : c ⟶ x
X Y : LeftExtension f g
η : X ⟶ Y
⊢ (X.whisker h).unit ≫ f ◁ StructuredArrow.Hom.right η ▷ h = (Y.whisker h).unit

Tactic:
simp [-LeftExtension.w, ← LeftExtension.w η]

Premises used: CategoryTheory.Bicategory.LeftExtension.w