awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s_1 t_1 : LeftLift f g
t : LeftLift f (𝟙 c ≫ g)
P : t.IsKan
s : LeftLift f g
τ : t.ofIdComp ⟶ s
h :
  t.unit ≫ StructuredArrow.Hom.right τ ▷ f =
    t.unit ≫
      StructuredArrow.Hom.right
          ((fun (s : LeftLift f g) ↦ (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))) : t.ofIdComp ⟶ s))
            s) ▷
        f
⊢ StructuredArrow.Hom.right τ =
    StructuredArrow.Hom.right
      ((fun (s : LeftLift f g) ↦ (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))) : t.ofIdComp ⟶ s)) s)

Tactic:
apply P.hom_ext

Premises used: CategoryTheory.Bicategory.LeftLift.IsKan.hom_ext
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s_1 t_1 : LeftLift f g
t : LeftLift f (𝟙 c ≫ g)
P : t.IsKan
s : LeftLift f g
τ : t.ofIdComp ⟶ s
⊢ t.unit ≫ StructuredArrow.Hom.right τ ▷ f =
    t.unit ≫
      StructuredArrow.Hom.right
          ((fun (s : LeftLift f g) ↦ (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))) : t.ofIdComp ⟶ s))
            s) ▷
        f

Tactic:
simp [← LeftLift.w τ]

Premises used: CategoryTheory.Bicategory.LeftLift.w
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
a : LocallyDiscrete C
⊢ { as := a.as : LocallyDiscrete C } = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
a : LocallyDiscrete C
⊢ Eq.{v + 1} (α := a.as ⟶ a.as) (Discrete.as (𝟙 a)) (𝟙 a.as)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
a b c : LocallyDiscrete C
f : a ⟶ b
g : b ⟶ c
⊢ (f ≫ g).as = f.as ≫ g.as

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
a b : LocallyDiscrete C
f g : a ⟶ b
⊢ Subsingleton.{v + 1} (f ⟶ g)

Tactic:
instSubsingletonDiscreteHom f g

Premises used: CategoryTheory.Discrete.instSubsingletonDiscreteHom
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y : LocallyDiscrete C
f g : X ⟶ Y
η : f ⟶ g
⊢ f = g

Tactic:
Discrete.ext η.1.1

Premises used: PLift.down, CategoryTheory.Discrete.ext, ULift.down
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : Category.{v, u} C
a b c d : LocallyDiscrete C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
as : ((f ≫ g) ≫ h).as = (f ≫ g ≫ h).as
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
apply Discrete.ext

Premises used: CategoryTheory.Discrete.ext
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : Category.{v, u} C
a b c d : LocallyDiscrete C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ ((f ≫ g) ≫ h).as = (f ≫ g ≫ h).as

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : Category.{v, u} C
a b : LocallyDiscrete C
f : a ⟶ b
as : (𝟙 a ≫ f).as = f.as
⊢ 𝟙 a ≫ f = f

Tactic:
apply Discrete.ext

Premises used: CategoryTheory.Discrete.ext
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : Category.{v, u} C
a b : LocallyDiscrete C
f : a ⟶ b
⊢ (𝟙 a ≫ f).as = f.as

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : Category.{v, u} C
a b : LocallyDiscrete C
f : a ⟶ b
as : (f ≫ 𝟙 b).as = f.as
⊢ f ≫ 𝟙 b = f

Tactic:
apply Discrete.ext

Premises used: CategoryTheory.Discrete.ext
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : Category.{v, u} C
a b : LocallyDiscrete C
f : a ⟶ b
⊢ (f ≫ 𝟙 b).as = f.as

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ IsLocallyDiscrete.{u_1, v_1, v_1} (LocallyDiscrete C)

Tactic:
fun _ _ ↦ Discrete.isDiscrete _

Premises used: Quiver.Hom, CategoryTheory.LocallyDiscrete.as, CategoryTheory.Discrete.isDiscrete
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
a : C
⊢ Eq.{v + 1} (α := { as := a : LocallyDiscrete C } ⟶ { as := a }) (toLoc (𝟙 a)) (𝟙 { as := a })

Tactic:
rfl

Premises used: Quiver.Hom.toLoc, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
a b c : C
f : a ⟶ b
g : b ⟶ c
⊢ (f ≫ g).toLoc = f.toLoc ≫ g.toLoc

Tactic:
rfl

Premises used: Quiver.Hom.toLoc, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : Category.{v, u} C
a b : C
h : a = b
subst : Eq.{v + 1} (α := { as := a : LocallyDiscrete C } ⟶ { as := a }) (Quiver.Hom.toLoc (eqToHom ⋯)) (eqToHom ⋯)
⊢ Eq.{v + 1} (α := { as := a : LocallyDiscrete C } ⟶ { as := b }) (Quiver.Hom.toLoc (eqToHom h)) (eqToHom ⋯)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u
inst : Category.{v, u} C
a : C
⊢ Eq.{v + 1} (α := { as := a : LocallyDiscrete C } ⟶ { as := a }) (Quiver.Hom.toLoc (eqToHom ⋯)) (eqToHom ⋯)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : CommSq t l r b
⊢ t.toLoc ≫ r.toLoc = l.toLoc ≫ b.toLoc

Tactic:
simp only [← Quiver.Hom.comp_toLoc, h.w]

Premises used: Quiver.Hom.comp_toLoc, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
Goal:
B : Type u₁
b : Pith B
⊢ { as := b.as : Pith B } = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
a : Pith B
⊢ Eq.{v₁ + 1} (α := a.as ⟶ a.as) (Core.of (𝟙 a)) (𝟙 a.as)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
a b c : Pith B
f : a ⟶ b
g : b ⟶ c
⊢ (f ≫ g).of = f.of ≫ g.of

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
a b : Pith B
x y : a ⟶ b
f g : x ⟶ y
h : f.iso.hom = g.iso.hom
⊢ f = g

Tactic:
CoreHom.ext <| Iso.ext h

Premises used: CategoryTheory.CoreHom.ext, CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
a b : Pith B
x y z : a ⟶ b
f : x ⟶ y
g : y ⟶ z
⊢ (f ≫ g).iso.hom = f.iso.hom ≫ g.iso.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
a b : Pith B
x y z : a ⟶ b
f : x ⟶ y
g : y ⟶ z
⊢ (f ≫ g).iso.inv = g.iso.inv ≫ f.iso.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
a b : Pith B
x : a ⟶ b
⊢ (CoreHom.iso (𝟙 x)).hom = 𝟙 x.of

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
a b : Pith B
x : a ⟶ b
⊢ (CoreHom.iso (𝟙 x)).inv = 𝟙 x.of

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
Goal:
B : Type u₁
inst_1 : Bicategory.{w₁, v₁, u₁} B
a b c : Pith B
f g : a ⟶ b
h_1 i : b ⟶ c
η : f ⟶ g
θ : h_1 ⟶ i
h :
  Eq.{w₁ + 1} (α := (f ≫ h_1).of ⟶ (g ≫ i).of)
    (Iso.hom
      (CoreHom.iso
        ({ iso := f.of ◁ᵢ θ.iso :
            CoreHom { of := f.of ≫ h_1.of : Core (a.as ⟶ c.as) } { of := f.of ≫ i.of : Core (a.as ⟶ c.as) } } ≫
          { iso := η.iso ▷ᵢ i.of })))
    (Iso.hom
      (CoreHom.iso
        ({ iso := η.iso ▷ᵢ h_1.of :
            CoreHom { of := f.of ≫ h_1.of : Core (a.as ⟶ c.as) } { of := g.of ≫ h_1.of : Core (a.as ⟶ c.as) } } ≫
          { iso := g.of ◁ᵢ θ.iso })))
⊢ Eq.{w₁ + 1} (α := f ≫ h_1 ⟶ g ≫ i)
    ({ iso := f.of ◁ᵢ θ.iso :
        CoreHom { of := f.of ≫ h_1.of : Core (a.as ⟶ c.as) } { of := f.of ≫ i.of : Core (a.as ⟶ c.as) } } ≫
      { iso := η.iso ▷ᵢ i.of })
    ({ iso := η.iso ▷ᵢ h_1.of :
        CoreHom { of := f.of ≫ h_1.of : Core (a.as ⟶ c.as) } { of := g.of ≫ h_1.of : Core (a.as ⟶ c.as) } } ≫
      { iso := g.of ◁ᵢ θ.iso })

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
Goal:
B : Type u₁
inst_1 : Bicategory.{w₁, v₁, u₁} B
a b c : Pith B
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
⊢ Eq.{w₁ + 1} (α := (f ≫ h).of ⟶ (g ≫ i).of)
    (Iso.hom
      (CoreHom.iso
        ({ iso := f.of ◁ᵢ θ.iso :
            CoreHom { of := f.of ≫ h.of : Core (a.as ⟶ c.as) } { of := f.of ≫ i.of : Core (a.as ⟶ c.as) } } ≫
          { iso := η.iso ▷ᵢ i.of })))
    (Iso.hom
      (CoreHom.iso
        ({ iso := η.iso ▷ᵢ h.of :
            CoreHom { of := f.of ≫ h.of : Core (a.as ⟶ c.as) } { of := g.of ≫ h.of : Core (a.as ⟶ c.as) } } ≫
          { iso := g.of ◁ᵢ θ.iso })))

Tactic:
simp [whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
⊢ IsLocallyGroupoid.{w₁, v₁, u₁} (Pith B)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ Δ : η ⟶ θ
h : ∀ (a : B), Γ.as.app a = Δ.as.app a
⊢ Γ = Δ

Tactic:
Hom.ext <| Modification.ext <| funext h

Premises used: CategoryTheory.Lax.LaxTrans.Hom.ext, CategoryTheory.Lax.LaxTrans.Modification.ext, funext
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), (app a).hom ▷ G.map f ≫ θ.naturality f = η.naturality f ≫ F.map f ◁ (app b).hom
a b : B
f : a ⟶ b
⊢ (app a).inv ▷ G.map f ≫ η.naturality f = θ.naturality f ≫ F.map f ◁ (app b).inv

Tactic:
simpa using (app a).inv ▷ G.map f ≫= (naturality f).symm =≫ F.map f ◁ (app b).inv

Premises used: CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct, CategoryTheory.LaxFunctor.toPrelaxFunctor, Prefunctor.map, CategoryTheory.PrelaxFunctorStruct.toPrefunctor, Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ Δ : η ⟶ θ
h : ∀ (a : B), Γ.as.app a = Δ.as.app a
⊢ Γ = Δ

Tactic:
Hom.ext <| Modification.ext <| funext h

Premises used: funext, CategoryTheory.Lax.OplaxTrans.Hom.ext, CategoryTheory.Lax.OplaxTrans.Modification.ext
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ θ.naturality f = η.naturality f ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ η.naturality f = θ.naturality f ≫ (app a).inv ▷ G.map f

Tactic:
simpa using F.map f ◁ (app b).inv ≫= (naturality f).symm =≫ (app a).inv ▷ G.map f

Premises used: CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct, CategoryTheory.LaxFunctor.toPrelaxFunctor, Prefunctor.map, CategoryTheory.PrelaxFunctorStruct.toPrefunctor, Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : Modification η θ
a b : B
a' : C
f : a' ⟶ F.obj a
g : a ⟶ b
simp_rw : f ◁ (Γ.app a ▷ G.map g ≫ θ.naturality g) = f ◁ (η.naturality g ≫ F.map g ◁ Γ.app b)
⊢ f ◁ Γ.app a ▷ G.map g ≫ f ◁ θ.naturality g = f ◁ η.naturality g ≫ f ◁ F.map g ◁ Γ.app b

Tactic:
simp_rw [← whiskerLeft_comp, naturality]

Premises used: CategoryTheory.Bicategory.whiskerLeft_comp, CategoryTheory.Oplax.LaxTrans.Modification.naturality
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : Modification η θ
a b : B
a' : C
f : a ⟶ b
g : G.obj b ⟶ a'
simp_rw : (Γ.app a ▷ G.map f ≫ θ.naturality f) ▷ g = (η.naturality f ≫ F.map f ◁ Γ.app b) ▷ g
⊢ Γ.app a ▷ G.map f ▷ g ≫ θ.naturality f ▷ g = η.naturality f ▷ g ≫ (F.map f ◁ Γ.app b) ▷ g

Tactic:
simp_rw [← comp_whiskerRight, naturality]

Premises used: CategoryTheory.Bicategory.comp_whiskerRight, CategoryTheory.Oplax.LaxTrans.Modification.naturality
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
m n : η ⟶ θ
h : ∀ (a : B), m.as.app a = n.as.app a
⊢ m = n

Tactic:
Hom.ext <| Modification.ext <| funext h

Premises used: CategoryTheory.Oplax.LaxTrans.Modification.ext, funext, CategoryTheory.Oplax.LaxTrans.Hom.ext
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), (app a).hom ▷ G.map f ≫ θ.naturality f = η.naturality f ≫ F.map f ◁ (app b).hom
a b : B
f : a ⟶ b
⊢ (app a).inv ▷ G.map f ≫ η.naturality f = θ.naturality f ≫ F.map f ◁ (app b).inv

Tactic:
simpa using (app a).inv ▷ G.map f ≫= (naturality f).symm =≫ F.map f ◁ (app b).inv

Premises used: CategoryTheory.OplaxFunctor.toPrelaxFunctor, CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct, Prefunctor.map, CategoryTheory.PrelaxFunctorStruct.toPrefunctor, Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : Modification η θ
b c : B
a' : C
f : a' ⟶ F.obj b
g : b ⟶ c
simp_rw : f ◁ (F.map g ◁ Γ.app c ≫ θ.naturality g) = f ◁ (η.naturality g ≫ Γ.app b ▷ G.map g)
⊢ f ◁ F.map g ◁ Γ.app c ≫ f ◁ θ.naturality g = f ◁ η.naturality g ≫ f ◁ Γ.app b ▷ G.map g

Tactic:
simp_rw [← Bicategory.whiskerLeft_comp, naturality]

Premises used: CategoryTheory.Bicategory.whiskerLeft_comp, CategoryTheory.Oplax.OplaxTrans.Modification.naturality
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : Modification η θ
a b : B
a' : C
f : a ⟶ b
g : G.obj b ⟶ a'
simp_rw :
  (α_ (F.map f) (η.app b) g).inv ≫ (F.map f ◁ Γ.app b) ▷ g ≫ θ.naturality f ▷ g =
    (α_ (F.map f) (η.app b) g).inv ≫ η.naturality f ▷ g ≫ Γ.app a ▷ G.map f ▷ g
simp_rw₁ :
  (α_ (F.map f) (η.app b) g).inv ≫ (F.map f ◁ Γ.app b ≫ θ.naturality f) ▷ g =
    (α_ (F.map f) (η.app b) g).inv ≫ (η.naturality f ≫ Γ.app a ▷ G.map f) ▷ g
⊢ F.map f ◁ Γ.app b ▷ g ≫ (α_ (F.map f) (θ.app b) g).inv ≫ θ.naturality f ▷ g =
    (α_ (F.map f) (η.app b) g).inv ≫ η.naturality f ▷ g ≫ Γ.app a ▷ G.map f ▷ g

Tactic:
simp_rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight, naturality]

Premises used: CategoryTheory.Bicategory.comp_whiskerRight, CategoryTheory.Oplax.OplaxTrans.Modification.naturality, CategoryTheory.Bicategory.associator_inv_naturality_middle_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
m n : η ⟶ θ
w : ∀ (b : B), m.as.app b = n.as.app b
⊢ m = n

Tactic:
Hom.ext <| Modification.ext <| funext w

Premises used: CategoryTheory.Oplax.OplaxTrans.Hom.ext, CategoryTheory.Oplax.OplaxTrans.Modification.ext, funext
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ θ.naturality f = η.naturality f ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ η.naturality f = θ.naturality f ≫ (app a).inv ▷ G.map f

Tactic:
simpa using _ ◁ (app b).inv ≫= (naturality f).symm =≫ (app a).inv ▷ _

Premises used: Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ_1 : Modification η θ
Γ : (StrongTrans.toOplax η).Modification (StrongTrans.toOplax θ)
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.app b ≫ (θ.naturality f).hom = (η.naturality f).hom ≫ Γ.app a ▷ G.map f

Tactic:
simpa using Γ.naturality f

Premises used: CategoryTheory.Oplax.OplaxTrans.Modification.naturality
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : Modification η θ
b c : B
a' : C
f : a' ⟶ F.obj b
g : b ⟶ c
⊢ f ◁ F.map g ◁ Γ.app c ≫ f ◁ (θ.naturality g).hom = f ◁ (η.naturality g).hom ≫ f ◁ Γ.app b ▷ G.map g

Tactic:
OplaxTrans.Modification.whiskerLeft_naturality Γ.toOplax _ _

Premises used: CategoryTheory.Oplax.StrongTrans.Modification.toOplax, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : Modification η θ
a b : B
a' : C
f : a ⟶ b
g : G.obj b ⟶ a'
⊢ F.map f ◁ Γ.app b ▷ g ≫ (α_ (F.map f) (θ.app b) g).inv ≫ (θ.naturality f).hom ▷ g =
    (α_ (F.map f) (η.app b) g).inv ≫ (η.naturality f).hom ▷ g ≫ Γ.app a ▷ G.map f ▷ g

Tactic:
OplaxTrans.Modification.whiskerRight_naturality Γ.toOplax _ _

Premises used: CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality, CategoryTheory.Oplax.StrongTrans.Modification.toOplax
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
m n : η ⟶ θ
w : ∀ (b : B), m.as.app b = n.as.app b
⊢ m = n

Tactic:
Hom.ext <| Modification.ext <| funext w

Premises used: CategoryTheory.Oplax.StrongTrans.Modification.ext, funext, CategoryTheory.Oplax.StrongTrans.Hom.ext
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality :
  ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ (θ.naturality f).hom = (η.naturality f).hom ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ (η.naturality f).hom = (θ.naturality f).hom ≫ (app a).inv ▷ G.map f

Tactic:
simpa using _ ◁ (app b).inv ≫= (naturality f).symm =≫ (app a).inv ▷ _

Premises used: Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : Modification η θ
b c : B
a' : C
f : a' ⟶ F.obj b
g : b ⟶ c
⊢ f ◁ F.map g ◁ Γ.app c ≫ f ◁ (θ.naturality g).hom = f ◁ (η.naturality g).hom ≫ f ◁ Γ.app b ▷ G.map g

Tactic:
Oplax.StrongTrans.Modification.whiskerLeft_naturality Γ.toOplax _ _

Premises used: CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.Pseudofunctor.StrongTrans.Modification.toOplax
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : Modification η θ
a b : B
a' : C
f : a ⟶ b
g : G.obj b ⟶ a'
⊢ F.map f ◁ Γ.app b ▷ g ≫ (α_ (F.map f) (θ.app b) g).inv ≫ (θ.naturality f).hom ▷ g =
    (α_ (F.map f) (η.app b) g).inv ≫ (η.naturality f).hom ▷ g ≫ Γ.app a ▷ G.map f ▷ g

Tactic:
Oplax.StrongTrans.Modification.whiskerRight_naturality Γ.toOplax _ _

Premises used: CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Pseudofunctor.StrongTrans.Modification.toOplax
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
m n : η ⟶ θ
w : ∀ (b : B), m.as.app b = n.as.app b
⊢ m = n

Tactic:
Hom.ext <| Modification.ext <| funext w

Premises used: funext, CategoryTheory.Pseudofunctor.StrongTrans.Modification.ext, CategoryTheory.Pseudofunctor.StrongTrans.Hom.ext
-- Module: Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality :
  ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ (θ.naturality f).hom = (η.naturality f).hom ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ (η.naturality f).hom = (θ.naturality f).hom ≫ (app a).inv ▷ G.map f

Tactic:
simpa using _ ◁ (app b).inv ≫= (naturality f).symm =≫ (app a).inv ▷ _

Premises used: Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
t : a ⟶ a
inst_1 : Comonad t
⊢ Δ ≫ ε ▷ t = (λ_ t).inv

Tactic:
ComonObj.counit_comul t

Premises used: CategoryTheory.ComonObj.counit_comul
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
t : a ⟶ a
inst_1 : Comonad t
⊢ Δ ≫ t ◁ ε = (ρ_ t).inv

Tactic:
ComonObj.comul_counit t

Premises used: CategoryTheory.ComonObj.comul_counit
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
t : a ⟶ a
inst_1 : Comonad t
⊢ Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom

Tactic:
ComonObj.comul_assoc t

Premises used: CategoryTheory.ComonObj.comul_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
t : a ⟶ a
inst_1 : Comonad t
⊢ Δ ≫ Δ ▷ t = Δ ≫ t ◁ Δ ≫ (α_ t t t).inv

Tactic:
ComonObj.comul_assoc_flip t

Premises used: CategoryTheory.ComonObj.comul_assoc_flip