awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1 : B} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = t.unit ≫ f ◁ H.desc σs'
have rw : 𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = σs'.unit
Tactic: rw [Hτ', IsKan.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1 : B} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ t.unit ≫
      f ◁ ((ρ_ t.extension).inv ≫ (t.extension ◁ η' ≫ (α_ t.extension h u).inv) ≫ StructuredArrow.Hom.right τ₀' ▷ u) =
    t.unit ≫
      f ◁
        ((ρ_ t.extension).inv ≫
          (ρ_ t.extension).hom ≫
            H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))
have calc : t.unit ≫
    f ◁ ((ρ_ t.extension).inv ≫ (t.extension ◁ η' ≫ (α_ t.extension h u).inv) ≫ StructuredArrow.Hom.right τ₀' ▷ u) =
  𝟙 g ⊗≫ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u
Tactic: calc _
      _ = 𝟙 _ ⊗≫ (t.unit ▷ (𝟙 c) ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u := by
        bicategory
      _ = 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 _ := by
        rw [← whisker_exchange]; bicategory
      _ = t.unit ≫ f ◁ H.desc σs' := by
        rw [Hτ', IsKan.fac]
        dsimp only [StructuredArrow.mk_hom_eq_self, σs']
      _ = _ := by
        bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1 : B} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
calc :
  t.unit ≫
      f ◁ ((ρ_ t.extension).inv ≫ (t.extension ◁ η' ≫ (α_ t.extension h u).inv) ≫ StructuredArrow.Hom.right τ₀' ▷ u) =
    𝟙 g ⊗≫ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u
⊢ t.unit ≫
      f ◁ ((ρ_ t.extension).inv ≫ (t.extension ◁ η' ≫ (α_ t.extension h u).inv) ≫ StructuredArrow.Hom.right τ₀' ▷ u) =
    t.unit ≫
      f ◁
        ((ρ_ t.extension).inv ≫
          (ρ_ t.extension).hom ≫
            H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))
have calc₁ : 𝟙 g ⊗≫ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u =
  𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)
Tactic: calc _
      _ = 𝟙 _ ⊗≫ (t.unit ▷ (𝟙 c) ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u := by
        bicategory
      _ = 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 _ := by
        rw [← whisker_exchange]; bicategory
      _ = t.unit ≫ f ◁ H.desc σs' := by
        rw [Hτ', IsKan.fac]
        dsimp only [StructuredArrow.mk_hom_eq_self, σs']
      _ = _ := by
        bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1 : B} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
calc :
  t.unit ≫
      f ◁ ((ρ_ t.extension).inv ≫ (t.extension ◁ η' ≫ (α_ t.extension h u).inv) ≫ StructuredArrow.Hom.right τ₀' ▷ u) =
    𝟙 g ⊗≫ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u
calc₁ :
  𝟙 g ⊗≫ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u =
    𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)
⊢ t.unit ≫
      f ◁ ((ρ_ t.extension).inv ≫ (t.extension ◁ η' ≫ (α_ t.extension h u).inv) ≫ StructuredArrow.Hom.right τ₀' ▷ u) =
    t.unit ≫
      f ◁
        ((ρ_ t.extension).inv ≫
          (ρ_ t.extension).hom ≫
            H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))
have calc₂ : 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = t.unit ≫ f ◁ H.desc σs'
Tactic: calc _
      _ = 𝟙 _ ⊗≫ (t.unit ▷ (𝟙 c) ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u := by
        bicategory
      _ = 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 _ := by
        rw [← whisker_exchange]; bicategory
      _ = t.unit ≫ f ◁ H.desc σs' := by
        rw [Hτ', IsKan.fac]
        dsimp only [StructuredArrow.mk_hom_eq_self, σs']
      _ = _ := by
        bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1 : B} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
calc :
  t.unit ≫
      f ◁ ((ρ_ t.extension).inv ≫ (t.extension ◁ η' ≫ (α_ t.extension h u).inv) ≫ StructuredArrow.Hom.right τ₀' ▷ u) =
    𝟙 g ⊗≫ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u
calc₁ :
  𝟙 g ⊗≫ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u =
    𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)
calc₂ : 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = t.unit ≫ f ◁ H.desc σs'
⊢ t.unit ≫
      f ◁ ((ρ_ t.extension).inv ≫ (t.extension ◁ η' ≫ (α_ t.extension h u).inv) ≫ StructuredArrow.Hom.right τ₀' ▷ u) =
    t.unit ≫
      f ◁
        ((ρ_ t.extension).inv ≫
          (ρ_ t.extension).hom ≫
            H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))
have calc₃ : t.unit ≫ f ◁ H.desc σs' =
  t.unit ≫
    f ◁
      ((ρ_ t.extension).inv ≫
        (ρ_ t.extension).hom ≫
          H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))
Tactic: calc _
      _ = 𝟙 _ ⊗≫ (t.unit ▷ (𝟙 c) ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u := by
        bicategory
      _ = 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 _ := by
        rw [← whisker_exchange]; bicategory
      _ = t.unit ≫ f ◁ H.desc σs' := by
        rw [Hτ', IsKan.fac]
        dsimp only [StructuredArrow.mk_hom_eq_self, σs']
      _ = _ := by
        bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.IsKan (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s_1 t_1 : LeftExtension f g
t : LeftExtension f (g ≫ 𝟙 c)
P : t.IsKan
s : LeftExtension f g
τ : t.ofCompId ⟶ s
⊢ τ = (fun (s : LeftExtension f g) ↦ (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))) : t.ofCompId ⟶ s)) s
have h : StructuredArrow.Hom.right τ =
  StructuredArrow.Hom.right
    ((fun (s : LeftExtension f g) ↦ (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))) : t.ofCompId ⟶ s)) s)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.IsKan (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s_1 t_1 : LeftExtension f g
t : LeftExtension f (g ≫ 𝟙 c)
P : t.IsKan
s : LeftExtension f g
τ : t.ofCompId ⟶ s
⊢ StructuredArrow.Hom.right τ =
    StructuredArrow.Hom.right
      ((fun (s : LeftExtension f g) ↦ (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))) : t.ofCompId ⟶ s)) s)
have h : t.unit ≫ f ◁ StructuredArrow.Hom.right τ =
  t.unit ≫
    f ◁
      StructuredArrow.Hom.right
        ((fun (s : LeftExtension f g) ↦ (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))) : t.ofCompId ⟶ s))
          s)
Tactic: apply P.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.IsKan (goal)
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
⊢ τ = (fun (s : LeftLift f g) ↦ (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))) : t.ofIdComp ⟶ s)) s
have h : 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.IsKan (goal)
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
⊢ StructuredArrow.Hom.right τ =
    StructuredArrow.Hom.right
      ((fun (s : LeftLift f g) ↦ (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))) : t.ofIdComp ⟶ s)) s)
have 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
Tactic: apply P.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.LocallyDiscrete (goal)
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 = f ≫ g ≫ h
have as : ((f ≫ g) ≫ h).as = (f ≫ g ≫ h).as
Tactic: apply Discrete.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.LocallyDiscrete (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : LocallyDiscrete C
f : a ⟶ b
⊢ 𝟙 a ≫ f = f
have as : (𝟙 a ≫ f).as = f.as
Tactic: apply Discrete.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.LocallyDiscrete (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : LocallyDiscrete C
f : a ⟶ b
⊢ f ≫ 𝟙 b = f
have as : (f ≫ 𝟙 b).as = f.as
Tactic: apply Discrete.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.LocallyDiscrete (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : C
h : a = b
⊢ Eq.{v + 1} (α := { as := a : LocallyDiscrete C } ⟶ { as := b }) (Quiver.Hom.toLoc (eqToHom h)) (eqToHom ⋯)
have subst : Eq.{v + 1} (α := { as := a : LocallyDiscrete C } ⟶ { as := a }) (Quiver.Hom.toLoc (eqToHom sorry)) (eqToHom sorry)
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.LocallyGroupoid (goal)
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 ⟶ g ≫ i)
    ({ 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 := η.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 })
have h : 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Modification.Oplax (goal)
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
⊢ f ◁ Γ.app a ▷ G.map g ≫ f ◁ θ.naturality g = f ◁ η.naturality g ≫ f ◁ F.map g ◁ Γ.app b
have simp_rw : f ◁ (Γ.app a ▷ G.map g ≫ θ.naturality g) = f ◁ (η.naturality g ≫ F.map g ◁ Γ.app b)
Tactic: simp_rw [← whiskerLeft_comp, naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Modification.Oplax (goal)
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'
⊢ Γ.app a ▷ G.map f ▷ g ≫ θ.naturality f ▷ g = η.naturality f ▷ g ≫ (F.map f ◁ Γ.app b) ▷ g
have simp_rw : (Γ.app a ▷ G.map f ≫ θ.naturality f) ▷ g = (η.naturality f ≫ F.map f ◁ Γ.app b) ▷ g
Tactic: simp_rw [← comp_whiskerRight, naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Modification.Oplax (goal)
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 = f ◁ η.naturality g ≫ f ◁ Γ.app b ▷ G.map g
have simp_rw : f ◁ (F.map g ◁ Γ.app c ≫ θ.naturality g) = f ◁ (η.naturality g ≫ Γ.app b ▷ G.map g)
Tactic: simp_rw [← Bicategory.whiskerLeft_comp, naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Modification.Oplax (goal)
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 ▷ g =
    (α_ (F.map f) (η.app b) g).inv ≫ η.naturality f ▷ g ≫ Γ.app a ▷ G.map f ▷ g
have 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
Tactic: simp_rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight, naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Modification.Oplax (goal)
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
⊢ 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
have 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
Tactic: simp_rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight, naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Monad.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
      MonoidalCategoryStruct.whiskerRight
        (F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
        (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) =
    Iso.inv (MonoidalCategoryStruct.leftUnitor (F.map (𝟙 { as := { as := () } })))
have simp : F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
    F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
        (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
      F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } ▷
        F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) =
  (λ_ (F.map (𝟙 { as := { as := () } }))).inv
Tactic: simp only [tensorUnit_def, tensorObj_def, whiskerRight_def, Category.assoc, leftUnitor_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Monad.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
        F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } ▷
          F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv
have rw : F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
    F.map₂ (λ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).hom ≫
      (λ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
  (λ_ (F.map (𝟙 { as := { as := () } }))).inv
Tactic: rw [F.mapComp_id_left, unitors_equal, F.map₂_inv_hom_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Monad.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
rw :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.map₂ (λ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).hom ≫
        (λ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
        F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } ▷
          F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv
have rw₁ : F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
    F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).hom ≫
      (λ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
  (λ_ (F.map (𝟙 { as := { as := () } }))).inv
Tactic: rw [F.mapComp_id_left, unitors_equal, F.map₂_inv_hom_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Monad.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
rw :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.map₂ (λ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).hom ≫
        (λ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv
rw₁ :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).hom ≫
        (λ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
        F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } ▷
          F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv
have rw₂ : (λ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
  (λ_ (F.map (𝟙 { as := { as := () } }))).inv
Tactic: rw [F.mapComp_id_left, unitors_equal, F.map₂_inv_hom_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Monad.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
      MonoidalCategoryStruct.whiskerLeft
        (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))
        (F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) =
    Iso.inv (MonoidalCategoryStruct.rightUnitor (F.map (𝟙 { as := { as := () } })))
have simp : (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
        (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
    F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
      F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } =
  (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
Tactic: simp only [tensorUnit_def, tensorObj_def, whiskerLeft_def, rightUnitor_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Monad.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
      F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
        F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
have rw : F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
    F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
        (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
      F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
        F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } =
  (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
Tactic: rw [Category.assoc, F.mapComp_id_right, F.map₂_inv_hom_assoc]