awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
⊢ h ◁ adj.unit ⊗≫ τ ▷ u = s.unit

Tactic:
have hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit := by simpa [bicategoricalComp] using LeftLift.w τ₀
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
rw : τ = 𝟙 (h ≫ f) ⊗≫ h ◁ ((λ_ f).hom ≫ (ρ_ f).inv) ⊗≫ τ ⊗≫ 𝟙 s.lift
⊢ τ = 𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift

Tactic:
rw [adj.left_triangle]

Premises used: CategoryTheory.Bicategory.Adjunction.left_triangle
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ τ = 𝟙 (h ≫ f) ⊗≫ h ◁ ((λ_ f).hom ≫ (ρ_ f).inv) ⊗≫ τ ⊗≫ 𝟙 s.lift

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
rw :
  𝟙 (h ≫ f) ⊗≫ h ◁ (adj.unit ▷ f ⊗≫ f ◁ adj.counit) ⊗≫ τ ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift

Tactic:
rw [leftZigzag]

Premises used: CategoryTheory.Bicategory.leftZigzag
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ (adj.unit ▷ f ⊗≫ f ◁ adj.counit) ⊗≫ τ ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
rw :
  𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ (τ ▷ (u ≫ f) ≫ s.lift ◁ adj.counit) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift

Tactic:
rw [whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ (τ ▷ (u ≫ f) ≫ s.lift ◁ adj.counit) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
rw :
  𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift =
    StructuredArrow.Hom.right
      ((fun (s : LeftLift u (h ≫ 𝟙 a)) ↦ homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯) s)
⊢ 𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift =
    StructuredArrow.Hom.right
      ((fun (s : LeftLift u (h ≫ 𝟙 a)) ↦ homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯) s)

Tactic:
rw [hτ]
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift =
    StructuredArrow.Hom.right
      ((fun (s : LeftLift u (h ≫ 𝟙 a)) ↦ homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯) s)

Tactic:
dsimp only [StructuredArrow.homMk_right]

Premises used: CategoryTheory.StructuredArrow.homMk_right
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
calc : τ = 𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift
calc₁ :
  𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift
calc₂ :
  𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift
calc₃ :
  𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift =
    StructuredArrow.Hom.right
      ((fun (s : LeftLift u (h ≫ 𝟙 a)) ↦ homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯) s)
⊢ StructuredArrow.Hom.right τ₀ =
    StructuredArrow.Hom.right
      ((fun (s : LeftLift u (h ≫ 𝟙 a)) ↦ homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯) s)

Tactic:
calc τ
        _ = 𝟙 _ ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 _ := by
          rw [adj.left_triangle]; bicategory
        _ = 𝟙 _ ⊗≫ h ◁ adj.unit ▷ f ⊗≫ (_ ◁ adj.counit ≫ τ ▷ _) ⊗≫ 𝟙 _ := by
          rw [leftZigzag]; bicategory
        _ = 𝟙 _ ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = _ := by
          rw [hτ]; dsimp only [StructuredArrow.homMk_right]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.Bicategory.LeftLift.lift, CategoryTheory.Bicategory.leftZigzag, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.Adjunction.unit, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.bicategoricalComp, CategoryTheory.Bicategory.Adjunction.counit
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
⊢ rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv

Tactic:
simpa [rightZigzag, bicategoricalComp] using H'.fac <| .mk _ <| (ρ_ u).hom ≫ (λ_ u).inv

Premises used: CategoryTheory.Bicategory.rightUnitor, CategoryTheory.Bicategory.leftUnitor, CategoryTheory.Bicategory.rightZigzag, CategoryTheory.Bicategory.LeftLift.IsKan.fac, CategoryTheory.Iso.hom, CategoryTheory.bicategoricalComp, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
apply : (λ_ t.lift).inv ≫ leftZigzag t.unit ε = (λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv
⊢ leftZigzag t.unit ε = (λ_ t.lift).hom ≫ (ρ_ t.lift).inv

Tactic:
apply (cancel_epi (λ_ _).inv).mp

Premises used: CategoryTheory.Bicategory.leftUnitor, Iff.mp, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
apply :
  t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
⊢ (λ_ t.lift).inv ≫ leftZigzag t.unit ε = (λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv

Tactic:
apply H.hom_ext

Premises used: CategoryTheory.Bicategory.LeftLift.IsKan.hom_ext
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
rw :
  Eq (α := 𝟙 a ⟶ (t.lift ≫ 𝟙 b) ≫ u)
    (𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ (t.unit ▷ t.lift ⊗≫ t.lift ◁ ε) ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
    (𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
⊢ Eq (α := 𝟙 a ⟶ (t.lift ≫ 𝟙 b) ≫ u) (𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
    (𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))

Tactic:
rw [leftZigzag]

Premises used: CategoryTheory.Bicategory.leftZigzag
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ Eq (α := 𝟙 a ⟶ (t.lift ≫ 𝟙 b) ≫ u)
    (𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ (t.unit ▷ t.lift ⊗≫ t.lift ◁ ε) ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
    (𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
rw :
  Eq (α := 𝟙 a ⟶ (t.lift ≫ 𝟙 b) ≫ u)
    (𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (t.lift ≫ u) ◁ t.unit) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
    (𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
⊢ Eq (α := 𝟙 a ⟶ (t.lift ≫ 𝟙 b) ≫ u)
    (𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
    (𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))

Tactic:
rw [whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ Eq (α := 𝟙 a ⟶ (t.lift ≫ 𝟙 b) ≫ u)
    (𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (t.lift ≫ u) ◁ t.unit) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
    (𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
rw :
  𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ ((ρ_ u).hom ≫ (λ_ u).inv) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u

Tactic:
rw [← rightZigzag, Hε]

Premises used: CategoryTheory.Bicategory.rightZigzag
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ ((ρ_ u).hom ≫ (λ_ u).inv) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
calc :
  t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)
calc₁ :
  Eq (α := 𝟙 a ⟶ (t.lift ≫ 𝟙 b) ≫ u) (𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
    (𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
calc₂ :
  Eq (α := 𝟙 a ⟶ (t.lift ≫ 𝟙 b) ≫ u)
    (𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
    (𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
calc₃ :
  𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
⊢ t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u

Tactic:
calc _
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ (_ ◁ t.unit ≫ t.unit ▷ _) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 _ := by
          rw [leftZigzag]; bicategory
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = _ := by
          rw [← rightZigzag, Hε]; bicategory

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.Bicategory.LeftLift.lift, CategoryTheory.Bicategory.leftZigzag, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.LeftLift.unit, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.bicategoricalComp
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
⊢ IsRightAdjoint u

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
⊢ HasAbsLeftKanLift u (𝟙 a)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
⊢ ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
⊢ ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)

Tactic:
tfae_have 1 → 2
  | h => IsAbsKan.hasAbsLeftKanLift (Adjunction.ofIsRightAdjoint u).isAbsoluteLeftKanLift
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
tfae_1_to_2 : ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)
⊢ HasAbsLeftKanLift u (𝟙 a)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
tfae_1_to_2 : ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)
⊢ ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
tfae_1_to_2 : ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)
⊢ ∀ (a_1 : HasAbsLeftKanLift u (𝟙 a)), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
tfae_1_to_2 : ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)
⊢ ∀ (a_1 : HasAbsLeftKanLift u (𝟙 a)), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u

Tactic:
tfae_have 2 → 3
  | h => ⟨inferInstance, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
tfae_1_to_2 : ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : ∀ (a_1 : HasAbsLeftKanLift u (𝟙 a)), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
⊢ ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
tfae_1_to_2 : ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : ∀ (a_1 : HasAbsLeftKanLift u (𝟙 a)), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
⊢ IsRightAdjoint u

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
tfae_1_to_2 : ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : ∀ (a_1 : HasAbsLeftKanLift u (𝟙 a)), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
⊢ ∀ (a_1 : ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u), IsRightAdjoint u

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
tfae_1_to_2 : ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : ∀ (a_1 : HasAbsLeftKanLift u (𝟙 a)), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
⊢ ∀ (a_1 : ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u), IsRightAdjoint u

Tactic:
tfae_have 3 → 1
  | ⟨h, h'⟩ => .mk <| (lanLiftIsKan u (𝟙 a)).adjunction <| LanLift.CommuteWith.isKan u (𝟙 a) u
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
tfae_1_to_2 : ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : ∀ (a_1 : HasAbsLeftKanLift u (𝟙 a)), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
tfae_3_to_1 : ∀ (a_1 : ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u), IsRightAdjoint u
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
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)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
⊢ t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ

Tactic:
simpa [bicategoricalComp] using (H' _).fac (.mk _ <| (ρ_ _).hom ≫ τ)

Premises used: CategoryTheory.Bicategory.rightUnitor, CategoryTheory.Bicategory.LeftLift.IsKan.fac, CategoryTheory.Bicategory.LeftLift.mk, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.bicategoricalComp
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
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)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
⊢ t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ

Tactic:
have Hσ : t.extension ◁ η' ⊗≫ σ ▷ u  = 𝟙 _ ⊗≫ τ := by
        simpa [bicategoricalComp] using (H' _).fac (.mk _ <| (ρ_ _).hom ≫ τ)
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
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)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
Hσ : t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ
dsimp :
  (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
    (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
⊢ ((LeftLift.mk h η').whisker g).unit ≫ ((t.whisker h).unit ≫ f ◁ σ) ▷ u =
    ((LeftLift.mk h η').whisker g).unit ≫ s.unit ▷ u

Tactic:
dsimp only [LeftLift.whisker_lift, StructuredArrow.mk_right, LeftLift.whisker_unit,
        StructuredArrow.mk_hom_eq_self, whisker_extension, whisker_unit]

Premises used: CategoryTheory.Bicategory.LeftLift.whisker_unit, CategoryTheory.Bicategory.LeftLift.whisker_lift, CategoryTheory.StructuredArrow.mk_right, CategoryTheory.Bicategory.LeftExtension.whisker_unit, CategoryTheory.Bicategory.LeftExtension.whisker_extension, CategoryTheory.StructuredArrow.mk_hom_eq_self