awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Unique (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' G'' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    (adj1.rightAdjointUniq adj3).hom.app x
have rw : (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
  ((adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom).app x
Tactic: rw [← rightAdjointUniq_trans adj1 adj2 adj3]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Whiskering (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X Y : Functor.{v_1, v_2, u_1, u_2} C D
f : X ⟶ Y
⊢ map (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) f ≫
      (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) Y).rightUnitor.inv ≫ Y.whiskerLeft adj.unit ≫ (Y.associator F G).inv =
    ((obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) X).rightUnitor.inv ≫ X.whiskerLeft adj.unit ≫ (X.associator F G).inv) ≫
      map (obj (whiskeringRight C D E) F ⋙ obj (whiskeringRight C E D) G) f
have w : ∀ (x : C),
  (map (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) f ≫
          (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) Y).rightUnitor.inv ≫
            Y.whiskerLeft adj.unit ≫ (Y.associator F G).inv).app
      x =
    NatTrans.app
      (((obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) X).rightUnitor.inv ≫
          X.whiskerLeft adj.unit ≫ (X.associator F G).inv) ≫
        map (obj (whiskeringRight C D E) F ⋙ obj (whiskeringRight C E D) G) f)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Whiskering (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X Y : Functor.{v_1, v_3, u_1, u_3} C E
f : X ⟶ Y
⊢ map (obj (whiskeringRight C E D) G ⋙ obj (whiskeringRight C D E) F) f ≫
      (Y.associator G F).hom ≫ Y.whiskerLeft adj.counit ≫ Y.rightUnitor.hom =
    ((X.associator G F).hom ≫ X.whiskerLeft adj.counit ≫ X.rightUnitor.hom) ≫
      map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C E)) f
have w : ∀ (x : C),
  (map (obj (whiskeringRight C E D) G ⋙ obj (whiskeringRight C D E) F) f ≫
          (Y.associator G F).hom ≫ Y.whiskerLeft adj.counit ≫ Y.rightUnitor.hom).app
      x =
    NatTrans.app
      (((X.associator G F).hom ≫ X.whiskerLeft adj.counit ≫ X.rightUnitor.hom) ≫
        map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C E)) f)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Whiskering (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X : Functor.{v_2, v_1, u_2, u_1} D C
⊢ map (obj (whiskeringLeft E D C) G)
        (NatTrans.app
          {
            app := fun (X : Functor.{v_2, v_1, u_2, u_1} D C) ↦
              (obj (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C)) X).leftUnitor.inv ≫
                whiskerRight adj.unit X ≫ (F.associator G X).hom,
            naturality := ⋯ }
          X) ≫
      NatTrans.app
        {
          app := fun (X : Functor.{v_3, v_1, u_3, u_1} E C) ↦
            (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
          naturality := ⋯ :
          NatTrans (C := Functor.{v_3, v_1, u_3, u_1} E C) (obj (whiskeringLeft D E C) F ⋙ obj (whiskeringLeft E D C) G)
            (𝟭 (Functor.{v_3, v_1, u_3, u_1} E C)) }
        (obj (obj (whiskeringLeft E D C) G) X) =
    𝟙 (obj (obj (whiskeringLeft E D C) G) X)
have w : ∀ (x : E),
  NatTrans.app
      (map (obj (whiskeringLeft E D C) G)
          (NatTrans.app
            {
              app := fun (X : Functor.{v_2, v_1, u_2, u_1} D C) ↦
                (obj (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C)) X).leftUnitor.inv ≫
                  whiskerRight adj.unit X ≫ (F.associator G X).hom,
              naturality := sorry }
            X) ≫
        NatTrans.app
          {
            app := fun (X : Functor.{v_3, v_1, u_3, u_1} E C) ↦
              (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
            naturality := sorry :
            NatTrans (C := Functor.{v_3, v_1, u_3, u_1} E C)
              (obj (whiskeringLeft D E C) F ⋙ obj (whiskeringLeft E D C) G) (𝟭 (Functor.{v_3, v_1, u_3, u_1} E C)) }
          (obj (obj (whiskeringLeft E D C) G) X))
      x =
    NatTrans.app (𝟙 (obj (obj (whiskeringLeft E D C) G) X)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Whiskering (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X : Functor.{v_3, v_1, u_3, u_1} E C
⊢ NatTrans.app
        {
          app := fun (X : Functor.{v_2, v_1, u_2, u_1} D C) ↦
            (obj (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C)) X).leftUnitor.inv ≫
              whiskerRight adj.unit X ≫ (F.associator G X).hom,
          naturality := ⋯ :
          NatTrans (C := Functor.{v_2, v_1, u_2, u_1} D C) (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C))
            (obj (whiskeringLeft E D C) G ⋙ obj (whiskeringLeft D E C) F) }
        (obj (obj (whiskeringLeft D E C) F) X) ≫
      map (obj (whiskeringLeft D E C) F)
        (NatTrans.app
          {
            app := fun (X : Functor.{v_3, v_1, u_3, u_1} E C) ↦
              (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
            naturality := ⋯ }
          X) =
    𝟙 (obj (obj (whiskeringLeft D E C) F) X)
have w : ∀ (x : D),
  NatTrans.app
      (NatTrans.app
          {
            app := fun (X : Functor.{v_2, v_1, u_2, u_1} D C) ↦
              (obj (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C)) X).leftUnitor.inv ≫
                whiskerRight adj.unit X ≫ (F.associator G X).hom,
            naturality := sorry :
            NatTrans (C := Functor.{v_2, v_1, u_2, u_1} D C) (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C))
              (obj (whiskeringLeft E D C) G ⋙ obj (whiskeringLeft D E C) F) }
          (obj (obj (whiskeringLeft D E C) F) X) ≫
        map (obj (whiskeringLeft D E C) F)
          (NatTrans.app
            {
              app := fun (X : Functor.{v_3, v_1, u_3, u_1} E C) ↦
                (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
              naturality := sorry }
            X))
      x =
    NatTrans.app (𝟙 (obj (obj (whiskeringLeft D E C) F) X)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : Adj.{w, v, u} B
α β : a ⟶ b
p : Hom₂ α β
⊢ ((conjugateEquiv β.adj α.adj).symm : (a_1 : β.r ⟶ α.r) → α.l ⟶ β.l) p.τr = p.τl
have rw : ((conjugateEquiv β.adj α.adj).symm : (a_1 : β.r ⟶ α.r) → α.l ⟶ β.l)
    ((conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) p.τl : β.r ⟶ α.r) =
  p.τl
Tactic: rw [← Hom₂.conjugateEquiv_τl, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : Adj.{w, v, u} B
α β : a ⟶ b
p : Hom₂ α β
rw :
  ((conjugateEquiv β.adj α.adj).symm : (a_1 : β.r ⟶ α.r) → α.l ⟶ β.l)
      ((conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) p.τl : β.r ⟶ α.r) =
    p.τl
⊢ ((conjugateEquiv β.adj α.adj).symm : (a_1 : β.r ⟶ α.r) → α.l ⟶ β.l) p.τr = p.τl
have rw₁ : p.τl = p.τl
Tactic: rw [← Hom₂.conjugateEquiv_τl, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Adj.{w, v, u} B
α β : a ⟶ b
el : α.l ≅ β.l
er : β.r ≅ α.r
h : (conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom = er.hom
⊢ (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv = er.inv
have rw : (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom = er.inv ≫ er.hom
Tactic: rw [← cancel_mono er.hom, Iso.inv_hom_id, ← h,
          conjugateEquiv_comp, Iso.hom_inv_id, conjugateEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Adj.{w, v, u} B
α β : a ⟶ b
el : α.l ≅ β.l
er : β.r ≅ α.r
h : (conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom = er.hom
rw : (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom = er.inv ≫ er.hom
⊢ (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv = er.inv
have rw₁ : Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom : α.r ⟶ α.r)
  (𝟙 α.r : α.r ⟶ α.r)
Tactic: rw [← cancel_mono er.hom, Iso.inv_hom_id, ← h,
          conjugateEquiv_comp, Iso.hom_inv_id, conjugateEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Adj.{w, v, u} B
α β : a ⟶ b
el : α.l ≅ β.l
er : β.r ≅ α.r
h : (conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom = er.hom
rw : (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom = er.inv ≫ er.hom
rw₁ :
  Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom : α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
⊢ (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv = er.inv
have rw₂ : Eq (α := α.r ⟶ α.r)
  (CategoryStruct.comp (Y := β.r) ((conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv)
      ((conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom) :
    α.r ⟶ α.r)
  (𝟙 α.r : α.r ⟶ α.r)
Tactic: rw [← cancel_mono er.hom, Iso.inv_hom_id, ← h,
          conjugateEquiv_comp, Iso.hom_inv_id, conjugateEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Adj.{w, v, u} B
α β : a ⟶ b
el : α.l ≅ β.l
er : β.r ≅ α.r
h : (conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom = er.hom
rw : (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom = er.inv ≫ er.hom
rw₁ :
  Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom : α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
rw₂ :
  Eq (α := α.r ⟶ α.r)
    (CategoryStruct.comp (Y := β.r) ((conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv)
        ((conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom) :
      α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
⊢ (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv = er.inv
have rw₃ : Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj α.adj : (a_1 : α.l ⟶ α.l) → α.r ⟶ α.r) (el.hom ≫ el.inv) : α.r ⟶ α.r)
  (𝟙 α.r : α.r ⟶ α.r)
Tactic: rw [← cancel_mono er.hom, Iso.inv_hom_id, ← h,
          conjugateEquiv_comp, Iso.hom_inv_id, conjugateEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Adj.{w, v, u} B
α β : a ⟶ b
el : α.l ≅ β.l
er : β.r ≅ α.r
h : (conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom = er.hom
rw : (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom = er.inv ≫ er.hom
rw₁ :
  Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom : α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
rw₂ :
  Eq (α := α.r ⟶ α.r)
    (CategoryStruct.comp (Y := β.r) ((conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv)
        ((conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom) :
      α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
rw₃ :
  Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj α.adj : (a_1 : α.l ⟶ α.l) → α.r ⟶ α.r) (el.hom ≫ el.inv) : α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
⊢ (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv = er.inv
have rw₄ : Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj α.adj : (a_1 : α.l ⟶ α.l) → α.r ⟶ α.r) (𝟙 α.l) : α.r ⟶ α.r)
  (𝟙 α.r : α.r ⟶ α.r)
Tactic: rw [← cancel_mono er.hom, Iso.inv_hom_id, ← h,
          conjugateEquiv_comp, Iso.hom_inv_id, conjugateEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Adj.{w, v, u} B
α β : a ⟶ b
el : α.l ≅ β.l
er : β.r ≅ α.r
h : (conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom = er.hom
rw : (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom = er.inv ≫ er.hom
rw₁ :
  Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom : α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
rw₂ :
  Eq (α := α.r ⟶ α.r)
    (CategoryStruct.comp (Y := β.r) ((conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv)
        ((conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom) :
      α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
rw₃ :
  Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj α.adj : (a_1 : α.l ⟶ α.l) → α.r ⟶ α.r) (el.hom ≫ el.inv) : α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
rw₄ :
  Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj α.adj : (a_1 : α.l ⟶ α.l) → α.r ⟶ α.r) (𝟙 α.l) : α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
⊢ (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv = er.inv
have rw₅ : 𝟙 α.r = 𝟙 α.r
Tactic: rw [← cancel_mono er.hom, Iso.inv_hom_id, ← h,
          conjugateEquiv_comp, Iso.hom_inv_id, conjugateEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.hom.τl ≫ e.inv.τl = 𝟙 adj₁.l
have rw : (e.hom ≫ e.inv).τl = 𝟙 adj₁.l
Tactic: rw [← comp_τl, e.hom_inv_id, id_τl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.hom ≫ e.inv).τl = 𝟙 adj₁.l
⊢ e.hom.τl ≫ e.inv.τl = 𝟙 adj₁.l
have rw₁ : Hom₂.τl (𝟙 adj₁) = 𝟙 adj₁.l
Tactic: rw [← comp_τl, e.hom_inv_id, id_τl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.hom ≫ e.inv).τl = 𝟙 adj₁.l
rw₁ : Hom₂.τl (𝟙 adj₁) = 𝟙 adj₁.l
⊢ e.hom.τl ≫ e.inv.τl = 𝟙 adj₁.l
have rw₂ : 𝟙 adj₁.l = 𝟙 adj₁.l
Tactic: rw [← comp_τl, e.hom_inv_id, id_τl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.inv.τl ≫ e.hom.τl = 𝟙 adj₂.l
have rw : (e.inv ≫ e.hom).τl = 𝟙 adj₂.l
Tactic: rw [← comp_τl, e.inv_hom_id, id_τl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.inv ≫ e.hom).τl = 𝟙 adj₂.l
⊢ e.inv.τl ≫ e.hom.τl = 𝟙 adj₂.l
have rw₁ : Hom₂.τl (𝟙 adj₂) = 𝟙 adj₂.l
Tactic: rw [← comp_τl, e.inv_hom_id, id_τl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.inv ≫ e.hom).τl = 𝟙 adj₂.l
rw₁ : Hom₂.τl (𝟙 adj₂) = 𝟙 adj₂.l
⊢ e.inv.τl ≫ e.hom.τl = 𝟙 adj₂.l
have rw₂ : 𝟙 adj₂.l = 𝟙 adj₂.l
Tactic: rw [← comp_τl, e.inv_hom_id, id_τl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.inv.τr ≫ e.hom.τr = 𝟙 adj₁.r
have rw : (e.hom ≫ e.inv).τr = 𝟙 adj₁.r
Tactic: rw [← comp_τr, e.hom_inv_id, id_τr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.hom ≫ e.inv).τr = 𝟙 adj₁.r
⊢ e.inv.τr ≫ e.hom.τr = 𝟙 adj₁.r
have rw₁ : Hom₂.τr (𝟙 adj₁) = 𝟙 adj₁.r
Tactic: rw [← comp_τr, e.hom_inv_id, id_τr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.hom ≫ e.inv).τr = 𝟙 adj₁.r
rw₁ : Hom₂.τr (𝟙 adj₁) = 𝟙 adj₁.r
⊢ e.inv.τr ≫ e.hom.τr = 𝟙 adj₁.r
have rw₂ : 𝟙 adj₁.r = 𝟙 adj₁.r
Tactic: rw [← comp_τr, e.hom_inv_id, id_τr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.hom.τr ≫ e.inv.τr = 𝟙 adj₂.r
have rw : (e.inv ≫ e.hom).τr = 𝟙 adj₂.r
Tactic: rw [← comp_τr, e.inv_hom_id, id_τr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.inv ≫ e.hom).τr = 𝟙 adj₂.r
⊢ e.hom.τr ≫ e.inv.τr = 𝟙 adj₂.r
have rw₁ : Hom₂.τr (𝟙 adj₂) = 𝟙 adj₂.r
Tactic: rw [← comp_τr, e.inv_hom_id, id_τr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Adj (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.inv ≫ e.hom).τr = 𝟙 adj₂.r
rw₁ : Hom₂.τr (𝟙 adj₂) = 𝟙 adj₂.r
⊢ e.hom.τr ≫ e.inv.τr = 𝟙 adj₂.r
have rw₂ : 𝟙 adj₂.r = 𝟙 adj₂.r
Tactic: rw [← comp_τr, e.inv_hom_id, id_τr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)
have rw : g ◁ η ⊗≫ (((g ≫ f) ≫ g) ◁ η ≫ ε ▷ g ▷ (f ≫ g)) ⊗≫ ε ▷ g =
  𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)
Tactic: rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g) =
    g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g
have rw : 𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (𝟙 a ◁ η ≫ η ▷ (f ≫ g)) ⊗≫ ((g ≫ f) ◁ ε ≫ ε ▷ 𝟙 b) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g) =
  g ◁ η ⊗≫ g ◁ (η ▷ f ⊗≫ f ◁ ε) ▷ g ⊗≫ ε ▷ g
Tactic: rw [← whisker_exchange, ← whisker_exchange, leftZigzag]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g
have rw : g ◁ η ⊗≫ g ◁ ((λ_ f).hom ≫ (ρ_ f).inv) ▷ g ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g
have _ : (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g
Tactic: calc
    _ = g ◁ η ⊗≫ ((ε ▷ g ▷ 𝟙 a) ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g := by
      bicategory
    _ = 𝟙 _ ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g := by
      rw [← whisker_exchange, ← whisker_exchange, leftZigzag]; bicategory
    _ = g ◁ η ⊗≫ ε ▷ g := by
      rw [h]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
_ : (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g
⊢ (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g
have _₁ : g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g =
  𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)
Tactic: calc
    _ = g ◁ η ⊗≫ ((ε ▷ g ▷ 𝟙 a) ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g := by
      bicategory
    _ = 𝟙 _ ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g := by
      rw [← whisker_exchange, ← whisker_exchange, leftZigzag]; bicategory
    _ = g ◁ η ⊗≫ ε ▷ g := by
      rw [h]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
_ : (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g
_₁ :
  g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)
⊢ (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g
have _₂ : 𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g) =
  g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g
Tactic: calc
    _ = g ◁ η ⊗≫ ((ε ▷ g ▷ 𝟙 a) ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g := by
      bicategory
    _ = 𝟙 _ ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g := by
      rw [← whisker_exchange, ← whisker_exchange, leftZigzag]; bicategory
    _ = g ◁ η ⊗≫ ε ▷ g := by
      rw [h]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
_ : (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g
_₁ :
  g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)
_₂ :
  𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g) =
    g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g
⊢ (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g
have _₃ : g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g
Tactic: calc
    _ = g ◁ η ⊗≫ ((ε ▷ g ▷ 𝟙 a) ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g := by
      bicategory
    _ = 𝟙 _ ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g := by
      rw [← whisker_exchange, ← whisker_exchange, leftZigzag]; bicategory
    _ = g ◁ η ⊗≫ ε ▷ g := by
      rw [h]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
have dsimp : leftZigzag (adj₁.unit ⊗≫ f₁ ◁ adj₂.unit ▷ g₁ ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ g₂ ≫ g₁))
    (𝟙 ((g₂ ≫ g₁) ≫ f₁ ≫ f₂) ⊗≫ g₂ ◁ adj₁.counit ▷ f₂ ⊗≫ adj₂.counit) =
  𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
    adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
      f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
Tactic: dsimp only [compUnit, compCounit]