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
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
calc :
  t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ rightZigzag t.unit ε) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ f ◁ rightZigzag t.unit ε ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension)
calc₁ :
  Eq (α := 𝟙 a ⟶ f ≫ 𝟙 b ≫ t.extension) (𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ f ◁ rightZigzag t.unit ε ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension))
    (𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (f ≫ t.extension) ◁ t.unit) ⊗≫ f ◁ ε ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension))
calc₂ :
  Eq (α := 𝟙 a ⟶ f ≫ 𝟙 b ≫ t.extension)
    (𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (f ≫ t.extension) ◁ t.unit) ⊗≫ f ◁ ε ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension))
    (𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ (t.unit ▷ f ⊗≫ f ◁ ε) ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension))
⊢ t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ rightZigzag t.unit ε) =
    t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ (ρ_ t.extension).hom ≫ (λ_ t.extension).inv)
have calc₃ : 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ (t.unit ▷ f ⊗≫ f ◁ ε) ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
  t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ (ρ_ t.extension).hom ≫ (λ_ t.extension).inv)
Tactic: calc _
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ f ◁ rightZigzag t.unit ε ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ (t.unit ▷ _ ≫ _ ◁ t.unit) ⊗≫ f ◁ ε ▷ t.extension ⊗≫ 𝟙 _ := by
          rw [rightZigzag]; bicategory
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ (t.unit ▷ f ⊗≫ f ◁ ε) ▷ t.extension ⊗≫ 𝟙 _ := by
          rw [← whisker_exchange]; bicategory
        _ = _ := by
          rw [← leftZigzag, Hε]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (hypothesis)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE
have tfae_1_to_2 : ∀ (a_1 : IsLeftAdjoint f), HasAbsLeftKanExtension f (𝟙 a)
Tactic: tfae_have 1 → 2
  | h => IsAbsKan.hasAbsLeftKanExtension (Adjunction.ofIsLeftAdjoint f).isAbsoluteLeftKan
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (hypothesis)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
tfae_1_to_2 : ∀ (a_1 : IsLeftAdjoint f), HasAbsLeftKanExtension f (𝟙 a)
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE
have tfae_2_to_3 : ∀ (a_1 : HasAbsLeftKanExtension f (𝟙 a)), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f
Tactic: tfae_have 2 → 3
  | h => ⟨inferInstance, inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (hypothesis)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
tfae_1_to_2 : ∀ (a_1 : IsLeftAdjoint f), HasAbsLeftKanExtension f (𝟙 a)
tfae_2_to_3 : ∀ (a_1 : HasAbsLeftKanExtension f (𝟙 a)), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE
have tfae_3_to_1 : ∀ (a_1 : ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f), IsLeftAdjoint f
Tactic: tfae_have 3 → 1
  | ⟨h, h'⟩ => .mk <| (lanIsKan f (𝟙 a)).adjunction <| Lan.CommuteWith.isKan f (𝟙 a) f
-- 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
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ ((LeftLift.mk f adj.unit).whisker h).unit ≫ (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ▷ u =
    𝟙 (h ≫ 𝟙 a) ⊗≫ ((h ≫ 𝟙 a) ◁ adj.unit ≫ s.unit ▷ (f ≫ u)) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u)
have dsimp : (h ◁ adj.unit ≫ (α_ h f u).inv) ≫ (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ▷ u =
  𝟙 (h ≫ 𝟙 a) ⊗≫ ((h ≫ 𝟙 a) ◁ adj.unit ≫ s.unit ▷ (f ≫ u)) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u)
Tactic: dsimp only [whisker_lift, StructuredArrow.mk_right, whisker_unit,
          StructuredArrow.mk_hom_eq_self]
-- 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
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ s.unit ⊗≫ s.lift ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (s.lift ≫ u) = s.unit
have rw : s.unit ⊗≫ s.lift ◁ ((ρ_ u).hom ≫ (λ_ u).inv) ⊗≫ 𝟙 (s.lift ≫ u) = s.unit
Tactic: rw [adj.right_triangle]
-- 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
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
⊢ τ₀ = (fun (s : LeftLift u (h ≫ 𝟙 a)) ↦ homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯) s
have h₁ : StructuredArrow.Hom.right τ₀ =
  StructuredArrow.Hom.right
    ((fun (s : LeftLift u (h ≫ 𝟙 a)) ↦ homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) sorry) s)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (hypothesis)
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 τ₀
⊢ 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)
have hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
Tactic: have hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit := by simpa [bicategoricalComp] using LeftLift.w τ₀
-- 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
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 ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift
have rw : τ = 𝟙 (h ≫ f) ⊗≫ h ◁ ((λ_ f).hom ≫ (ρ_ f).inv) ⊗≫ τ ⊗≫ 𝟙 s.lift
Tactic: rw [adj.left_triangle]
-- 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
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 ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift
have 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
Tactic: rw [leftZigzag]
-- 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
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 ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift
have 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
Tactic: rw [whisker_exchange]
-- 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
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 ⊗≫ τ ▷ 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)
have 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) sorry) s)
Tactic: rw [hτ]
-- 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
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
⊢ 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)
have calc : τ = 𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift
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]
-- 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
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
⊢ 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)
have calc₁ : 𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift =
  𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift
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]
-- 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
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
⊢ 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)
have 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
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]
-- 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
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
⊢ 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)
have 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) sorry) 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]
-- 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
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
⊢ leftZigzag t.unit ε = (λ_ t.lift).hom ≫ (ρ_ t.lift).inv
have apply : (λ_ t.lift).inv ≫ leftZigzag t.unit ε = (λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv
Tactic: apply (cancel_epi (λ_ _).inv).mp
-- 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
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.lift).inv ≫ leftZigzag t.unit ε = (λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv
have apply : t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
  t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
Tactic: apply H.hom_ext
-- 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
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 ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
    (𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u))
have 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))
Tactic: rw [leftZigzag]
-- 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
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) ⊗≫ (𝟙 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))
have 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))
Tactic: rw [whisker_exchange]
-- 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
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 ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
have 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
Tactic: rw [← rightZigzag, Hε]
-- 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
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 =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
have calc : t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
  𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ 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
-- 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
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)
⊢ t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
have 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))
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
-- 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
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))
⊢ t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
have 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))
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
-- 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
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))
⊢ t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
have 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
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (hypothesis)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
u : b ⟶ a
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE
have tfae_1_to_2 : ∀ (a_1 : IsRightAdjoint u), HasAbsLeftKanLift u (𝟙 a)
Tactic: tfae_have 1 → 2
  | h => IsAbsKan.hasAbsLeftKanLift (Adjunction.ofIsRightAdjoint u).isAbsoluteLeftKanLift
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (hypothesis)
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)
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE
have tfae_2_to_3 : ∀ (a_1 : HasAbsLeftKanLift u (𝟙 a)), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
Tactic: tfae_have 2 → 3
  | h => ⟨inferInstance, inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Kan.Adjunction (hypothesis)
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, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE
have tfae_3_to_1 : ∀ (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