awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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σ
⊢ ((LeftLift.mk h η').whisker g).unit ≫ ((t.whisker h).unit ≫ f ◁ σ) ▷ u =
    ((LeftLift.mk h η').whisker g).unit ≫ s.unit ▷ u
have Hσ : t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ
Tactic: have Hσ : t.extension ◁ η' ⊗≫ σ ▷ u  = 𝟙 _ ⊗≫ τ := by
        simpa [bicategoricalComp] using (H' _).fac (.mk _ <| (ρ_ _).hom ≫ τ)
-- 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)
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) ⊗≫ τ
⊢ ((LeftLift.mk h η').whisker g).unit ≫ ((t.whisker h).unit ≫ f ◁ σ) ▷ u =
    ((LeftLift.mk h η').whisker g).unit ≫ s.unit ▷ u
have dsimp : (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
  (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
Tactic: dsimp only [LeftLift.whisker_lift, StructuredArrow.mk_right, LeftLift.whisker_unit,
        StructuredArrow.mk_hom_eq_self, whisker_extension, whisker_unit]
-- 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)
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) ⊗≫ τ
⊢ (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
    t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)
have rw : (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
  t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ 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
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) ⊗≫ τ
⊢ t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
    (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv
have rw : t.unit ▷ 𝟙 c ⊗≫ f ◁ (𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
  (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv
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
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) ⊗≫ τ
⊢ (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv = (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
have rw : (ρ_ g).hom ≫ sτ.unit ≫ (α_ f s.extension u).inv = (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
Tactic: rw [IsKan.fac_assoc]
-- 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)
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) ⊗≫ τ
⊢ (ρ_ g).hom ≫ sτ.unit ≫ (α_ f s.extension u).inv = (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
have dsimp : (ρ_ g).hom ≫ (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u)) ≫ (α_ f s.extension u).inv =
  (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
Tactic: dsimp only [StructuredArrow.mk_right, StructuredArrow.mk_hom_eq_self, sτ]
-- 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)
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) ⊗≫ τ
⊢ (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
    (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
have calc : (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
  (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)
Tactic: calc _
        _ = (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 _ := by
          bicategory
        _ = t.unit ▷ (𝟙 c) ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv := by
          rw [Hσ]
          dsimp only [τ]
          bicategory
        _ = _ := by
          rw [IsKan.fac_assoc]
          dsimp only [StructuredArrow.mk_right, StructuredArrow.mk_hom_eq_self, sτ]
          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)
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) ⊗≫ τ
calc :
  (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
    (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)
⊢ (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
    (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
have calc₁ : (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
  t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)
Tactic: calc _
        _ = (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 _ := by
          bicategory
        _ = t.unit ▷ (𝟙 c) ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv := by
          rw [Hσ]
          dsimp only [τ]
          bicategory
        _ = _ := by
          rw [IsKan.fac_assoc]
          dsimp only [StructuredArrow.mk_right, StructuredArrow.mk_hom_eq_self, sτ]
          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)
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) ⊗≫ τ
calc :
  (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
    (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)
calc₁ :
  (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
    t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)
⊢ (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
    (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
have calc₂ : t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
  (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv
Tactic: calc _
        _ = (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 _ := by
          bicategory
        _ = t.unit ▷ (𝟙 c) ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv := by
          rw [Hσ]
          dsimp only [τ]
          bicategory
        _ = _ := by
          rw [IsKan.fac_assoc]
          dsimp only [StructuredArrow.mk_right, StructuredArrow.mk_hom_eq_self, sτ]
          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)
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) ⊗≫ τ
calc :
  (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
    (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)
calc₁ :
  (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
    t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)
calc₂ :
  t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
    (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv
⊢ (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
    (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
have calc₃ : (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv = (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u
Tactic: calc _
        _ = (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 _ := by
          bicategory
        _ = t.unit ▷ (𝟙 c) ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv := by
          rw [Hσ]
          dsimp only [τ]
          bicategory
        _ = _ := by
          rw [IsKan.fac_assoc]
          dsimp only [StructuredArrow.mk_right, StructuredArrow.mk_hom_eq_self, sτ]
          bicategory
-- 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
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 τ₀'
⊢ τ₀' =
    (fun (s : LeftExtension f (g ≫ h)) ↦
        let k := s.extension;
        let θ := s.unit;
        let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
        let τ := H.desc sτ;
        let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
        let σ := H'.desc sσ;
        homMk σ ⋯)
      s'
have Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
Tactic: have Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit := by simpa [bicategoricalComp] using τ₀'.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
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
⊢ τ₀' =
    (fun (s : LeftExtension f (g ≫ h)) ↦
        let k := s.extension;
        let θ := s.unit;
        let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
        let τ := H.desc sτ;
        let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
        let σ := H'.desc sσ;
        homMk σ ⋯)
      s'
have h₁ : StructuredArrow.Hom.right τ₀' =
  StructuredArrow.Hom.right
    ((fun (s : LeftExtension f (g ≫ h)) ↦
        let k := s.extension;
        let θ := s.unit;
        let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
        let τ := H.desc sτ;
        let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
        let σ := H'.desc sσ;
        homMk σ sorry)
      s')
Tactic: 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
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
⊢ StructuredArrow.Hom.right τ₀' =
    StructuredArrow.Hom.right
      ((fun (s : LeftExtension f (g ≫ h)) ↦
          let k := s.extension;
          let θ := s.unit;
          let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
          let τ := H.desc sτ;
          let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
          let σ := H'.desc sσ;
          homMk σ ⋯)
        s')
have h₁ : ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u =
  ((LeftLift.mk h η').whisker t.extension).unit ≫
    StructuredArrow.Hom.right
        ((fun (s : LeftExtension f (g ≫ h)) ↦
            let k := s.extension;
            let θ := s.unit;
            let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
            let τ := H.desc sτ;
            let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
            let σ := H'.desc sσ;
            homMk σ sorry)
          s') ▷
      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
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
⊢ ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u =
    ((LeftLift.mk h η').whisker t.extension).unit ≫
      StructuredArrow.Hom.right
          ((fun (s : LeftExtension f (g ≫ h)) ↦
              let k := s.extension;
              let θ := s.unit;
              let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
              let τ := H.desc sτ;
              let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
              let σ := H'.desc sσ;
              homMk σ ⋯)
            s') ▷
        u
have h₁ : ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u =
  ((LeftLift.mk h η').whisker t.extension).unit ≫
    H'.desc
        (LeftLift.mk s'.extension
          ((ρ_ t.extension).hom ≫
            H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))) ▷
      u
Tactic: 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
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
⊢ ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u =
    ((LeftLift.mk h η').whisker t.extension).unit ≫
      H'.desc
          (LeftLift.mk s'.extension
            ((ρ_ t.extension).hom ≫
              H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))) ▷
        u
have h₁ : ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u =
  LeftLift.unit
    (LeftLift.mk s'.extension
      ((ρ_ t.extension).hom ≫
        H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)))))
Tactic: rw [(H' _).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
⊢ ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u =
    LeftLift.unit
      (LeftLift.mk s'.extension
        ((ρ_ t.extension).hom ≫
          H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)))))
have h₁ : (ρ_ t.extension).inv ≫ ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u =
  (ρ_ t.extension).inv ≫
    LeftLift.unit
      (LeftLift.mk s'.extension
        ((ρ_ t.extension).hom ≫
          H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)))))
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
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
⊢ (ρ_ t.extension).inv ≫ ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u =
    (ρ_ t.extension).inv ≫
      LeftLift.unit
        (LeftLift.mk s'.extension
          ((ρ_ t.extension).hom ≫
            H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)))))
have h₁ : t.unit ≫
    f ◁ ((ρ_ t.extension).inv ≫ ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u) =
  t.unit ≫
    f ◁
      ((ρ_ t.extension).inv ≫
        LeftLift.unit
          (LeftLift.mk s'.extension
            ((ρ_ t.extension).hom ≫
              H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ 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
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
⊢ t.unit ≫
      f ◁ ((ρ_ t.extension).inv ≫ ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u) =
    t.unit ≫
      f ◁
        ((ρ_ t.extension).inv ≫
          LeftLift.unit
            (LeftLift.mk s'.extension
              ((ρ_ t.extension).hom ≫
                H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))))
have h₁ : 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))))
Tactic: dsimp only [LeftLift.whisker_lift, StructuredArrow.mk_right, LeftLift.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
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 ⊗≫ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u =
    𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)
have rw : 𝟙 g ⊗≫ (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ τ' ▷ u =
  𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)
Tactic: rw [← whisker_exchange]