awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
b c a_1 b_1 c_1 : B
g : Hom.{v, u} a_1 b_1
g_1 : Hom.{v, u} b_1 c_1
ihf : ∀ {a : B} (f : Hom.{v, u} a a_1), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom.{v, u} a b_1), normalizeAux nil (f.comp g_1) = (normalizeAux nil f).comp (normalizeAux nil g_1)
a : B
f : Hom.{v, u} a a_1
comp :
  (normalizeAux nil (f.comp g)).comp (normalizeAux nil g_1) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g_1))
comp₁ :
  ((normalizeAux nil f).comp (normalizeAux nil g)).comp (normalizeAux nil g_1) =
    (normalizeAux nil f).comp (normalizeAux nil (g.comp g_1))
⊢ normalizeAux nil (f.comp (g.comp g_1)) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g_1))
have comp₂ : ((normalizeAux nil f).comp (normalizeAux nil g)).comp (normalizeAux nil g_1) =
  (normalizeAux nil f).comp ((normalizeAux nil g).comp (normalizeAux nil g_1))
Tactic: erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
b c a_1 b_1 c_1 : B
g : Hom.{v, u} a_1 b_1
g_1 : Hom.{v, u} b_1 c_1
ihf : ∀ {a : B} (f : Hom.{v, u} a a_1), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom.{v, u} a b_1), normalizeAux nil (f.comp g_1) = (normalizeAux nil f).comp (normalizeAux nil g_1)
a : B
f : Hom.{v, u} a a_1
comp :
  (normalizeAux nil (f.comp g)).comp (normalizeAux nil g_1) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g_1))
comp₁ :
  ((normalizeAux nil f).comp (normalizeAux nil g)).comp (normalizeAux nil g_1) =
    (normalizeAux nil f).comp (normalizeAux nil (g.comp g_1))
comp₂ :
  ((normalizeAux nil f).comp (normalizeAux nil g)).comp (normalizeAux nil g_1) =
    (normalizeAux nil f).comp ((normalizeAux nil g).comp (normalizeAux nil g_1))
⊢ normalizeAux nil (f.comp (g.comp g_1)) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g_1))
have comp₃ : (normalizeAux nil f).comp ((normalizeAux nil g).comp (normalizeAux nil g_1)) =
  (normalizeAux nil f).comp ((normalizeAux nil g).comp (normalizeAux nil g_1))
Tactic: erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f : Hom.{v, u} a b
g : Hom.{v, u} b c
⊢ normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
have id : ∀ (a : B) {a_1 : B} (f : Hom.{v, u} a_1 a),
  normalizeAux nil (f.comp (Hom.id a)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.id a))
Tactic: induction g generalizing a with
  | id => rfl
  | of => rfl
  | comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
Cleared hypotheses: a, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f : Hom.{v, u} a b
g : Hom.{v, u} b c
id :
  ∀ (a : B) {a_1 : B} (f : Hom.{v, u} a_1 a),
    normalizeAux nil (f.comp (Hom.id a)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.id a))
⊢ normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
have of : ∀ {a b : B} (f : a ⟶ b) {a_1 : B} (f_1 : Hom.{v, u} a_1 a),
  normalizeAux nil (f_1.comp (Hom.of f)) = (normalizeAux nil f_1).comp (normalizeAux nil (Hom.of f))
Tactic: induction g generalizing a with
  | id => rfl
  | of => rfl
  | comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
Cleared hypotheses: a, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f : Hom.{v, u} a b
g : Hom.{v, u} b c
id :
  ∀ (a : B) {a_1 : B} (f : Hom.{v, u} a_1 a),
    normalizeAux nil (f.comp (Hom.id a)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.id a))
of :
  ∀ {a b : B} (f : a ⟶ b) {a_1 : B} (f_1 : Hom.{v, u} a_1 a),
    normalizeAux nil (f_1.comp (Hom.of f)) = (normalizeAux nil f_1).comp (normalizeAux nil (Hom.of f))
⊢ normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
have comp : ∀ {a b c : B} (g : Hom.{v, u} a b) (g_1 : Hom.{v, u} b c)
  (ihf :
    ∀ {a_1 : B} (f : Hom.{v, u} a_1 a), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g))
  (ihg :
    ∀ {a : B} (f : Hom.{v, u} a b), normalizeAux nil (f.comp g_1) = (normalizeAux nil f).comp (normalizeAux nil g_1))
  {a_1 : B} (f : Hom.{v, u} a_1 a),
  normalizeAux nil (f.comp (g.comp g_1)) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g_1))
Tactic: induction g generalizing a with
  | id => rfl
  | of => rfl
  | comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
Cleared hypotheses: a, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : B
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
have 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) }
Tactic: obtain ⟨f⟩ := f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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) }
⊢ 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) }
have 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
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (hypothesis)
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) }
⊢ 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
have ih₁ : 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
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
| (Functor.obj (𝟭 (Discrete (Path.{v, u} a c))) { as := a_1.cons a_2 : Discrete (Path.{v, u} a c) }).as
have 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
Tactic: rw [← ih]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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 := a_1.cons a_2 : Discrete (Path.{v, u} a c) }).as
have 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
Tactic: conv_rhs => rw [← ih]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : B
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) }
have 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 := nil } :
    Discrete (Path.{v, u} a a))
  (Functor.obj (𝟭 (Discrete (Path.{v, u} a a))) { as := nil } : Discrete (Path.{v, u} a a))
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
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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))
⊢ 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) }
have 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) }
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
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.End (goal)
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₂
⊢ (f₁ ▷ X₂ ≫ Y₁ ◁ f₂) ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ≫ g₁) ▷ X₂ ≫ Z₁ ◁ (f₂ ≫ g₂)
have rw : (f₁ ▷ X₂ ≫ Y₁ ◁ f₂) ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ≫ g₁) ▷ X₂ ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂
Tactic: rw [Bicategory.whiskerLeft_comp, Bicategory.comp_whiskerRight, Category.assoc, Category.assoc,
      Bicategory.whisker_exchange_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.End (goal)
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₂
⊢ (f₁ ▷ X₂ ≫ Y₁ ◁ f₂) ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ≫ g₁) ▷ X₂ ≫ Z₁ ◁ (f₂ ≫ g₂)
have rw₁ : (f₁ ▷ X₂ ≫ Y₁ ◁ f₂) ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ▷ X₂ ≫ g₁ ▷ X₂) ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂
Tactic: rw [Bicategory.whiskerLeft_comp, Bicategory.comp_whiskerRight, Category.assoc, Category.assoc,
      Bicategory.whisker_exchange_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.End (goal)
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₂
⊢ (f₁ ▷ X₂ ≫ Y₁ ◁ f₂) ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ≫ g₁) ▷ X₂ ≫ Z₁ ◁ (f₂ ≫ g₂)
have rw₂ : f₁ ▷ X₂ ≫ Y₁ ◁ f₂ ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ▷ X₂ ≫ g₁ ▷ X₂) ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂
Tactic: rw [Bicategory.whiskerLeft_comp, Bicategory.comp_whiskerRight, Category.assoc, Category.assoc,
      Bicategory.whisker_exchange_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.End (goal)
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₂
⊢ (f₁ ▷ X₂ ≫ Y₁ ◁ f₂) ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ≫ g₁) ▷ X₂ ≫ Z₁ ◁ (f₂ ≫ g₂)
have rw₃ : f₁ ▷ X₂ ≫ Y₁ ◁ f₂ ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = f₁ ▷ X₂ ≫ g₁ ▷ X₂ ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂
Tactic: rw [Bicategory.whiskerLeft_comp, Bicategory.comp_whiskerRight, Category.assoc, Category.assoc,
      Bicategory.whisker_exchange_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.End (goal)
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₂
⊢ (f₁ ▷ X₂ ≫ Y₁ ◁ f₂) ≫ g₁ ▷ Y₂ ≫ Z₁ ◁ g₂ = (f₁ ≫ g₁) ▷ X₂ ≫ Z₁ ◁ (f₂ ≫ g₂)
have rw₄ : f₁ ▷ X₂ ≫ g₁ ▷ X₂ ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂ = f₁ ▷ X₂ ≫ g₁ ▷ X₂ ≫ Z₁ ◁ f₂ ≫ Z₁ ◁ g₂
Tactic: rw [Bicategory.whiskerLeft_comp, Bicategory.comp_whiskerRight, Category.assoc, Category.assoc,
      Bicategory.whisker_exchange_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
e₁ : x = y
⊢ Eq.{w + 1} (α := Iso.{w, v} (C := x ⟶ y) (eqToHom ⋯) (eqToHom e₁ ≫ eqToHom ⋯)) (eqToHomTransIso e₁ ⋯)
    (Iso.symm (ρ_ (eqToHom e₁)))
have w : Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ y) (eqToHom sorry) (eqToHom e₁ ≫ eqToHom sorry)) (Iso.hom (eqToHomTransIso e₁ sorry))
  (Iso.hom (Iso.symm (ρ_ (eqToHom e₁))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
e₁ : x = y
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ y) (eqToHom ⋯) (eqToHom e₁ ≫ eqToHom ⋯)) (Iso.hom (eqToHomTransIso e₁ ⋯))
    (Iso.hom (Iso.symm (ρ_ (eqToHom e₁))))
have w : Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ x) (eqToHom sorry) (eqToHom sorry ≫ eqToHom sorry)) (Iso.hom (eqToHomTransIso sorry sorry))
  (Iso.hom (Iso.symm (ρ_ (eqToHom sorry))))
Tactic: subst e₁
Cleared hypotheses: y, e₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
e₁ : x = y
⊢ Eq.{w + 1} (α := Iso.{w, v} (C := x ⟶ y) (eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom e₁)) (eqToHomTransIso ⋯ e₁)
    (Iso.symm (λ_ (eqToHom e₁)))
have w : Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ y) (eqToHom sorry) (eqToHom sorry ≫ eqToHom e₁)) (Iso.hom (eqToHomTransIso sorry e₁))
  (Iso.hom (Iso.symm (λ_ (eqToHom e₁))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
e₁ : x = y
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ y) (eqToHom ⋯) (eqToHom ⋯ ≫ eqToHom e₁)) (Iso.hom (eqToHomTransIso ⋯ e₁))
    (Iso.hom (Iso.symm (λ_ (eqToHom e₁))))
have w : Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := x ⟶ x) (eqToHom sorry) (eqToHom sorry ≫ eqToHom sorry)) (Iso.hom (eqToHomTransIso sorry sorry))
  (Iso.hom (Iso.symm (λ_ (eqToHom sorry))))
Tactic: subst e₁
Cleared hypotheses: y, e₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
e₁ : x = y
e₂ : y = z
e₃ : z = t
⊢ 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₃))
have subst_vars : Eq.{w + 1} (α :=
  Quiver.Hom.{w, v} (V := t ⟶ t) ((eqToHom sorry ≫ eqToHom sorry) ≫ eqToHom sorry) (eqToHom sorry ≫ eqToHom sorry ≫ eqToHom sorry))
  (Iso.hom (α_ (eqToHom sorry) (eqToHom sorry) (eqToHom sorry)))
  (Iso.inv (eqToHomTransIso sorry sorry) ▷ eqToHom sorry ≫
    Iso.inv (eqToHomTransIso sorry sorry) ≫ Iso.hom (eqToHomTransIso sorry sorry) ≫ eqToHom sorry ◁ Iso.hom (eqToHomTransIso sorry sorry))
Tactic: subst_vars
Cleared hypotheses: x, y, z, e₁, e₂, e₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y z t : B
e₁ : x = y
e₂ : y = z
e₃ : z = t
⊢ 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₃)
have subst_vars : Eq.{w + 1} (α :=
  Quiver.Hom.{w, v} (V := t ⟶ t) (eqToHom sorry ≫ eqToHom sorry ≫ eqToHom sorry) ((eqToHom sorry ≫ eqToHom sorry) ≫ eqToHom sorry))
  (Iso.inv (α_ (eqToHom sorry) (eqToHom sorry) (eqToHom sorry)))
  (eqToHom sorry ◁ Iso.inv (eqToHomTransIso sorry sorry) ≫
    Iso.inv (eqToHomTransIso sorry sorry) ≫ Iso.hom (eqToHomTransIso sorry sorry) ≫ Iso.hom (eqToHomTransIso sorry sorry) ▷ eqToHom sorry)
Tactic: subst_vars
Cleared hypotheses: x, y, z, e₁, e₂, e₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
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).hom = eqToHom ⋯ ≫ (α_ f' g' h').hom ≫ eqToHom ⋯
have subst_vars : (α_ f' g' h').hom = eqToHom sorry ≫ (α_ f' g' h').hom ≫ eqToHom sorry
Tactic: subst_vars
Cleared hypotheses: f, g, h, ef, eg, eh
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
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).inv = eqToHom ⋯ ≫ (α_ f' g' h').inv ≫ eqToHom ⋯
have subst_vars : (α_ f' g' h').inv = eqToHom sorry ≫ (α_ f' g' h').inv ≫ eqToHom sorry
Tactic: subst_vars
Cleared hypotheses: f, g, h, ef, eg, eh
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
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'
⊢ f ≫ g = f' ≫ g
have rw : f' ≫ g = f' ≫ g
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
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'
⊢ f' ≫ g' = f ≫ g'
have rw : f' ≫ g' = f' ≫ g'
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
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'
⊢ f ◁ η = eqToHom ⋯ ≫ f' ◁ η ≫ eqToHom ⋯
have subst : f ◁ η = eqToHom sorry ≫ f ◁ η ≫ eqToHom sorry
Tactic: subst h
Cleared hypotheses: f', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
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'
⊢ f ≫ g = f ≫ g'
have rw : f ≫ g' = f ≫ g'
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
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'
⊢ f' ≫ g' = f' ≫ g
have rw : f' ≫ g' = f' ≫ g'
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
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'
⊢ η ▷ g = eqToHom ⋯ ≫ η ▷ g' ≫ eqToHom ⋯
have subst : η ▷ g = eqToHom sorry ≫ η ▷ g ≫ eqToHom sorry
Tactic: subst h
Cleared hypotheses: g', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f f' : x ⟶ y
h : f = f'
⊢ (λ_ f).hom = 𝟙 x ◁ eqToHom h ≫ (λ_ f').hom ≫ eqToHom ⋯
have subst : (λ_ f).hom = 𝟙 x ◁ eqToHom sorry ≫ (λ_ f).hom ≫ eqToHom sorry
Tactic: subst h
Cleared hypotheses: f', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f f' : x ⟶ y
h : f = f'
⊢ (λ_ f).inv = eqToHom h ≫ (λ_ f').inv ≫ 𝟙 x ◁ eqToHom ⋯
have subst : (λ_ f).inv = eqToHom sorry ≫ (λ_ f).inv ≫ 𝟙 x ◁ eqToHom sorry
Tactic: subst h
Cleared hypotheses: f', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f f' : x ⟶ y
h : f = f'
⊢ (ρ_ f).hom = eqToHom h ▷ 𝟙 y ≫ (ρ_ f').hom ≫ eqToHom ⋯
have subst : (ρ_ f).hom = eqToHom sorry ▷ 𝟙 y ≫ (ρ_ f).hom ≫ eqToHom sorry
Tactic: subst h
Cleared hypotheses: f', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.EqToHom (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
x y : B
f f' : x ⟶ y
h : f = f'
⊢ (ρ_ f).inv = eqToHom h ≫ (ρ_ f').inv ≫ eqToHom ⋯ ▷ 𝟙 y
have subst : (ρ_ f).inv = eqToHom sorry ≫ (ρ_ f).inv ≫ eqToHom sorry ▷ 𝟙 y
Tactic: subst h
Cleared hypotheses: f', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Extension (goal)
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
i : s ⟶ t
x : B
h : c ⟶ x
⊢ StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h) =
    StructuredArrow.hom (t.whisker h)
have rw : (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
  StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv
Tactic: rw [← cancel_mono (α_ _ _ _).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Extension (goal)
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
i : s ⟶ t
x : B
h : c ⟶ x
⊢ (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
    StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv
have _ : (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
  (s.unit ≫ f ◁ StructuredArrow.Hom.right i) ▷ h
Tactic: calc
      _ = (unit s ≫ f ◁ i.right) ▷ h := by simp [-LeftExtension.w]
      _ = unit t ▷ h := congrArg (· ▷ h) (LeftExtension.w i)
      _ = _ := by simp