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
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))
rw : 𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = σs'.unit
⊢ 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = t.unit ≫ f ◁ H.desc σs'

Tactic:
rw [Hτ', IsKan.fac]

Premises used: CategoryTheory.Bicategory.LeftExtension.IsKan.fac
-- 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)
τ₀' : 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 ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = σs'.unit

Tactic:
dsimp only [StructuredArrow.mk_hom_eq_self, σs']

Premises used: CategoryTheory.StructuredArrow.mk_hom_eq_self
-- 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)
τ₀' : 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 ◁ 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:
bicategory
-- 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)
τ₀' : 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'
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))))
⊢ 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:
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

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.Bicategory.LeftExtension.extension, CategoryTheory.Bicategory.LeftExtension.IsKan.desc, CategoryTheory.Bicategory.LeftExtension.unit, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.whiskerLeft, 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
x : B
h : c ⟶ x
inst_1 : IsLeftAdjoint h
inst_2 : HasLeftKanExtension f g
⊢ Lan.CommuteWith f g h

Tactic:
⟨⟨isKanOfWhiskerLeftAdjoint (lanIsKan f g) (Adjunction.ofIsLeftAdjoint h)⟩⟩

Premises used: CategoryTheory.Bicategory.lanIsKan, CategoryTheory.Bicategory.Lan.CommuteWith.mk, Nonempty.intro, CategoryTheory.Bicategory.LeftExtension.isKanOfWhiskerLeftAdjoint, CategoryTheory.Bicategory.Adjunction.ofIsLeftAdjoint
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
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
⊢ HasLeftKanExtension f g

Tactic:
⟨IsInitial.hasInitial H⟩

Premises used: CategoryTheory.Limits.IsInitial.hasInitial, CategoryTheory.Bicategory.HasLeftKanExtension.mk
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
inst_1 : HasLeftKanExtension f g
⊢ HasInitial (LeftExtension f g)

Tactic:
HasLeftKanExtension.hasInitial

Premises used: CategoryTheory.Bicategory.HasLeftKanExtension.hasInitial
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
inst_1 : HasLeftKanExtension f g
⊢ (lanLeftExtension f g).extension = f⁺ g

Tactic:
rfl

Premises used: CategoryTheory.Bicategory.lan, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
inst_1 : HasLeftKanExtension f g
⊢ (lanLeftExtension f g).unit = lanUnit f g

Tactic:
rfl

Premises used: CategoryTheory.Bicategory.lanUnit, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
inst_1 : HasLeftKanExtension f g
s : LeftExtension f g
⊢ CategoryStruct.comp (Y := f ≫ f⁺ g) (lanUnit f g) (f ◁ lanDesc s) = s.unit

Tactic:
(lanIsKan f g).fac s

Premises used: CategoryTheory.Bicategory.lanIsKan, CategoryTheory.Bicategory.lan, CategoryTheory.Bicategory.lanDesc, CategoryTheory.Bicategory.lanUnit, CategoryTheory.Bicategory.LeftExtension.IsKan.fac
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
inst_1 : HasLeftKanExtension f g
s : LeftExtension f g
⊢ Eq (α := (lanLeftExtension f g).extension ⟶ s.extension) (IsKan.desc (lanIsKan f g) s) (lanDesc s)

Tactic:
rfl

Premises used: CategoryTheory.Bicategory.lanDesc, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
inst_1 : HasLeftKanExtension f g
s : LeftExtension f g
⊢ ∃! τ : f⁺ g ⟶ s.extension, lanUnit f g ≫ f ◁ τ = s.unit

Tactic:
(lanIsKan f g).existsUnique _

Premises used: CategoryTheory.Bicategory.lanIsKan, CategoryTheory.Bicategory.lan, CategoryTheory.StructuredArrow.IsUniversal.existsUnique, CategoryTheory.Bicategory.lanUnit
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
inst_1 : HasLeftKanExtension f g
t : LeftExtension f g
x : B
h : c ⟶ x
H : (t.whisker h).IsKan
i : t.whisker h ≅ (lanLeftExtension f g).whisker h
⊢ CommuteWith f g h

Tactic:
⟨⟨IsKan.ofIsoKan H i⟩⟩

Premises used: CategoryTheory.Bicategory.Lan.CommuteWith.mk, Nonempty.intro, CategoryTheory.Bicategory.LeftExtension.IsKan.ofIsoKan
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
inst_1 : HasLeftKanExtension f g
x : B
h : c ⟶ x
inst_2 : HasLeftKanExtension f (g ≫ h)
i : f⁺ (g ≫ h) ≅ f⁺ g ≫ h
w : lanUnit f (g ≫ h) ≫ f ◁ i.hom = lanUnit f g ▷ h ≫ (α_ f (f⁺ g) h).hom
⊢ CommuteWith f g h

Tactic:
⟨⟨(lanIsKan f (g ≫ h)).ofIsoKan <| StructuredArrow.isoMk i⟩⟩

Premises used: CategoryTheory.StructuredArrow.isoMk, CategoryTheory.Bicategory.lanIsKan, CategoryTheory.Bicategory.Lan.CommuteWith.mk, Nonempty.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.LeftExtension.IsKan.ofIsoKan
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f_1 : a ⟶ b
g_1 : a ⟶ c
f_2 : a ⟶ b
g_2 : a ⟶ c
f : a ⟶ b
g : a ⟶ c
inst_1 : HasLeftKanExtension f g
x : B
h : c ⟶ x
inst_2 : CommuteWith f g h
⊢ HasLeftKanExtension f (g ≫ h)

Tactic:
(Lan.CommuteWith.isKan f g h).hasLeftKanExtension

Premises used: CategoryTheory.Bicategory.Lan.CommuteWith.isKan, CategoryTheory.Bicategory.LeftExtension.IsKan.hasLeftKanExtension
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
inst_1 : HasLeftKanExtension f g
x : B
h : c ⟶ x
inst_2 : CommuteWith f g h
⊢ Eq (α :=
    StructuredArrow.right (lanLeftExtension f (g ≫ h)) ⟶ StructuredArrow.right ((lanLeftExtension f g).whisker h))
    (StructuredArrow.Hom.right (Iso.hom (lanCompIsoWhisker f g h)) :
      StructuredArrow.right (lanLeftExtension f (g ≫ h)) ⟶ StructuredArrow.right ((lanLeftExtension f g).whisker h))
    (lanDesc ((lanLeftExtension f g).whisker h) : f⁺ (g ≫ h) ⟶ ((lanLeftExtension f g).whisker h).extension)

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.IsUniversal.desc, CategoryTheory.Bicategory.lanDesc, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
inst_1 : HasLeftKanExtension f g
x : B
h : c ⟶ x
inst_2 : CommuteWith f g h
⊢ Eq (α :=
    StructuredArrow.right ((lanLeftExtension f g).whisker h) ⟶ StructuredArrow.right (lanLeftExtension f (g ≫ h)))
    (StructuredArrow.Hom.right (Iso.inv (lanCompIsoWhisker f g h)) :
      StructuredArrow.right ((lanLeftExtension f g).whisker h) ⟶ StructuredArrow.right (lanLeftExtension f (g ≫ h)))
    (IsKan.desc (isKan f g h) (lanLeftExtension f (g ≫ h)) :
      ((lanLeftExtension f g).whisker h).extension ⟶ (lanLeftExtension f (g ≫ h)).extension)

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.IsUniversal.desc, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f_1 : a ⟶ b
g_1 : a ⟶ c
f : a ⟶ b
g : a ⟶ c
inst_1 : HasAbsLeftKanExtension f g
x : B
h : c ⟶ x
⊢ Lan.CommuteWith f g h

Tactic:
HasAbsLeftKanExtension.commute h

Premises used: CategoryTheory.Bicategory.HasAbsLeftKanExtension.commute
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
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.IsAbsKan
⊢ HasAbsLeftKanExtension f g

Tactic:
have : HasLeftKanExtension f g := H.isKan.hasLeftKanExtension
  ⟨fun h ↦ ⟨⟨H.ofIsoAbsKan (IsKan.uniqueUpToIso H.isKan (lanIsKan f g)) h⟩⟩⟩

Premises used: CategoryTheory.Bicategory.lanIsKan, CategoryTheory.Bicategory.LeftExtension.IsAbsKan.ofIsoAbsKan, CategoryTheory.Bicategory.Lan.CommuteWith.mk, CategoryTheory.Bicategory.LeftExtension.IsKan.hasLeftKanExtension, Nonempty.intro, CategoryTheory.Bicategory.LeftExtension.IsAbsKan.isKan, CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso, CategoryTheory.Bicategory.HasAbsLeftKanExtension.mk
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
t : LeftLift f g
H : t.IsKan
⊢ HasLeftKanLift f g

Tactic:
⟨IsInitial.hasInitial H⟩

Premises used: CategoryTheory.Bicategory.HasLeftKanLift.mk', CategoryTheory.Limits.IsInitial.hasInitial
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
inst_1 : HasLeftKanLift f g
⊢ HasInitial (LeftLift f g)

Tactic:
HasLeftKanLift.hasInitial

Premises used: CategoryTheory.Bicategory.HasLeftKanLift.hasInitial
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
inst_1 : HasLeftKanLift f g
⊢ (lanLiftLeftLift f g).lift = f₊ g

Tactic:
rfl

Premises used: CategoryTheory.Bicategory.lanLift, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
inst_1 : HasLeftKanLift f g
⊢ (lanLiftLeftLift f g).unit = lanLiftUnit f g

Tactic:
rfl

Premises used: CategoryTheory.Bicategory.lanLiftUnit, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
inst_1 : HasLeftKanLift f g
s : LeftLift f g
⊢ CategoryStruct.comp (Y := f₊ g ≫ f) (lanLiftUnit f g) (lanLiftDesc s ▷ f) = s.unit

Tactic:
(lanLiftIsKan f g).fac s

Premises used: CategoryTheory.Bicategory.lanLiftDesc, CategoryTheory.Bicategory.LeftLift.IsKan.fac, CategoryTheory.Bicategory.lanLiftUnit, CategoryTheory.Bicategory.lanLiftIsKan, CategoryTheory.Bicategory.lanLift
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
inst_1 : HasLeftKanLift f g
s : LeftLift f g
⊢ Eq (α := (lanLiftLeftLift f g).lift ⟶ s.lift) (IsKan.desc (lanLiftIsKan f g) s) (lanLiftDesc s)

Tactic:
rfl

Premises used: CategoryTheory.Bicategory.lanLiftDesc, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
inst_1 : HasLeftKanLift f g
s : LeftLift f g
⊢ ∃! τ : f₊ g ⟶ s.lift, lanLiftUnit f g ≫ τ ▷ f = s.unit

Tactic:
(lanLiftIsKan f g).existsUnique _

Premises used: CategoryTheory.StructuredArrow.IsUniversal.existsUnique, CategoryTheory.Bicategory.lanLiftUnit, CategoryTheory.Bicategory.lanLiftIsKan, CategoryTheory.Bicategory.lanLift
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
inst_1 : HasLeftKanLift f g
t : LeftLift f g
x : B
h : x ⟶ c
H : (t.whisker h).IsKan
i : t.whisker h ≅ (lanLiftLeftLift f g).whisker h
⊢ CommuteWith f g h

Tactic:
⟨⟨IsKan.ofIsoKan H i⟩⟩

Premises used: CategoryTheory.Bicategory.LanLift.CommuteWith.mk, CategoryTheory.Bicategory.LeftLift.IsKan.ofIsoKan, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
inst_1 : HasLeftKanLift f g
x : B
h : x ⟶ c
inst_2 : HasLeftKanLift f (h ≫ g)
i : f₊ (h ≫ g) ≅ h ≫ f₊ g
w : lanLiftUnit f (h ≫ g) ≫ i.hom ▷ f = h ◁ lanLiftUnit f g ≫ (α_ h (f₊ g) f).inv
⊢ CommuteWith f g h

Tactic:
⟨⟨(lanLiftIsKan f (h ≫ g)).ofIsoKan <| StructuredArrow.isoMk i⟩⟩

Premises used: CategoryTheory.StructuredArrow.isoMk, CategoryTheory.Bicategory.LanLift.CommuteWith.mk, CategoryTheory.Bicategory.LeftLift.IsKan.ofIsoKan, Nonempty.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.lanLiftIsKan
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f_1 : b ⟶ a
g_1 : c ⟶ a
f_2 : b ⟶ a
g_2 : c ⟶ a
f : b ⟶ a
g : c ⟶ a
inst_1 : HasLeftKanLift f g
x : B
h : x ⟶ c
inst_2 : CommuteWith f g h
⊢ HasLeftKanLift f (h ≫ g)

Tactic:
(LanLift.CommuteWith.isKan f g h).hasLeftKanLift

Premises used: CategoryTheory.Bicategory.LanLift.CommuteWith.isKan, CategoryTheory.Bicategory.LeftLift.IsKan.hasLeftKanLift
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
inst_1 : HasLeftKanLift f g
x : B
h : x ⟶ c
inst_2 : CommuteWith f g h
⊢ Eq (α := StructuredArrow.right (lanLiftLeftLift f (h ≫ g)) ⟶ StructuredArrow.right ((lanLiftLeftLift f g).whisker h))
    (StructuredArrow.Hom.right (Iso.hom (lanLiftCompIsoWhisker f g h)) :
      StructuredArrow.right (lanLiftLeftLift f (h ≫ g)) ⟶ StructuredArrow.right ((lanLiftLeftLift f g).whisker h))
    (lanLiftDesc ((lanLiftLeftLift f g).whisker h) : f₊ (h ≫ g) ⟶ ((lanLiftLeftLift f g).whisker h).lift)

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.IsUniversal.desc, CategoryTheory.Bicategory.lanLiftDesc, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
inst_1 : HasLeftKanLift f g
x : B
h : x ⟶ c
inst_2 : CommuteWith f g h
⊢ Eq (α := StructuredArrow.right ((lanLiftLeftLift f g).whisker h) ⟶ StructuredArrow.right (lanLiftLeftLift f (h ≫ g)))
    (StructuredArrow.Hom.right (Iso.inv (lanLiftCompIsoWhisker f g h)) :
      StructuredArrow.right ((lanLiftLeftLift f g).whisker h) ⟶ StructuredArrow.right (lanLiftLeftLift f (h ≫ g)))
    (IsKan.desc (isKan f g h) (lanLiftLeftLift f (h ≫ g)) :
      ((lanLiftLeftLift f g).whisker h).lift ⟶ (lanLiftLeftLift f (h ≫ g)).lift)

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.IsUniversal.desc, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f_1 : b ⟶ a
g_1 : c ⟶ a
f : b ⟶ a
g : c ⟶ a
inst_1 : HasAbsLeftKanLift f g
x : B
h : x ⟶ c
⊢ LanLift.CommuteWith f g h

Tactic:
HasAbsLeftKanLift.commute h

Premises used: CategoryTheory.Bicategory.HasAbsLeftKanLift.commute
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
t : LeftLift f g
H : t.IsAbsKan
⊢ HasAbsLeftKanLift f g

Tactic:
have : HasLeftKanLift f g := H.isKan.hasLeftKanLift
  ⟨fun h ↦ ⟨⟨H.ofIsoAbsKan (IsKan.uniqueUpToIso H.isKan (lanLiftIsKan f g)) h⟩⟩⟩

Premises used: CategoryTheory.Bicategory.LeftLift.IsAbsKan.isKan, CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso, CategoryTheory.Bicategory.LanLift.CommuteWith.mk, Nonempty.intro, CategoryTheory.Bicategory.lanLiftIsKan, CategoryTheory.Bicategory.LeftLift.IsAbsKan.ofIsoAbsKan, CategoryTheory.Bicategory.HasAbsLeftKanLift.mk, CategoryTheory.Bicategory.LeftLift.IsKan.hasLeftKanLift
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
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
s : LeftExtension f g
⊢ t.unit ≫ f ◁ H.desc s = s.unit

Tactic:
StructuredArrow.IsUniversal.fac H s

Premises used: CategoryTheory.StructuredArrow.IsUniversal.fac
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
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
k : b ⟶ c
τ τ' : t.extension ⟶ k
w : t.unit ≫ f ◁ τ = t.unit ≫ f ◁ τ'
⊢ τ = τ'

Tactic:
StructuredArrow.IsUniversal.hom_ext H w

Premises used: CategoryTheory.StructuredArrow.IsUniversal.hom_ext
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
P : s.IsKan
Q : t.IsKan
⊢ StructuredArrow.Hom.right (P.uniqueUpToIso Q).hom = P.desc t

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.IsUniversal.desc, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
P : s.IsKan
Q : t.IsKan
⊢ StructuredArrow.Hom.right (P.uniqueUpToIso Q).inv = Q.desc s

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.IsUniversal.desc, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
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
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)
⊢ τ = (fun (s : LeftExtension f g) ↦ (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))) : t.ofCompId ⟶ s)) s

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
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
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)
⊢ 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:
apply P.hom_ext

Premises used: CategoryTheory.Bicategory.LeftExtension.IsKan.hom_ext
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
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
⊢ 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:
simp [← LeftExtension.w τ]

Premises used: CategoryTheory.Bicategory.LeftExtension.w
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
t : LeftLift f g
H : t.IsKan
s : LeftLift f g
⊢ t.unit ≫ H.desc s ▷ f = s.unit

Tactic:
StructuredArrow.IsUniversal.fac H s

Premises used: CategoryTheory.StructuredArrow.IsUniversal.fac
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
t : LeftLift f g
H : t.IsKan
k : c ⟶ b
τ τ' : t.lift ⟶ k
w : t.unit ≫ τ ▷ f = t.unit ≫ τ' ▷ f
⊢ τ = τ'

Tactic:
StructuredArrow.IsUniversal.hom_ext H w

Premises used: CategoryTheory.StructuredArrow.IsUniversal.hom_ext
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
P : s.IsKan
Q : t.IsKan
⊢ StructuredArrow.Hom.right (P.uniqueUpToIso Q).hom = P.desc t

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.IsUniversal.desc, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
P : s.IsKan
Q : t.IsKan
⊢ StructuredArrow.Hom.right (P.uniqueUpToIso Q).inv = Q.desc s

Tactic:
rfl

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

Tactic:
ext