awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F₁ F₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D
τ : F₁ ⟶ F₂
dsimp :
  Eq (α := obj L.lan (T ⋙ F₁) ⟶ B ⋙ obj R.lan F₂)
    (map L.lan (T.whiskerLeft τ) ≫
      (Equiv.symm (Adjunction.homEquiv (L.lanAdjunction D) (T ⋙ F₂) (B ⋙ obj R.lan F₂)) :
          (a : T ⋙ F₂ ⟶ L ⋙ B ⋙ R.lan.obj F₂) → L.lan.obj (T ⋙ F₂) ⟶ B ⋙ R.lan.obj F₂)
        (T.whiskerLeft (NatTrans.app R.lanUnit F₂) ≫
          (T.associator R (obj R.lan F₂)).inv ≫
            whiskerRight w.natTrans (obj R.lan F₂) ≫ (L.associator B (obj R.lan F₂)).hom))
    ((Equiv.symm (Adjunction.homEquiv (L.lanAdjunction D) (T ⋙ F₁) (B ⋙ obj R.lan F₁)) :
          (a : T ⋙ F₁ ⟶ L ⋙ B ⋙ R.lan.obj F₁) → L.lan.obj (T ⋙ F₁) ⟶ B ⋙ R.lan.obj F₁)
        (T.whiskerLeft (NatTrans.app R.lanUnit F₁) ≫
          (T.associator R (obj R.lan F₁)).inv ≫
            whiskerRight w.natTrans (obj R.lan F₁) ≫ (L.associator B (obj R.lan F₁)).hom) ≫
      B.whiskerLeft (map R.lan τ))
⊢ Eq (α := obj (obj (whiskeringLeft C₁ C₂ D) T ⋙ L.lan) F₁ ⟶ obj (R.lan ⋙ obj (whiskeringLeft C₃ C₄ D) B) F₂)
    (map (obj (whiskeringLeft C₁ C₂ D) T ⋙ L.lan) τ ≫
      (Equiv.symm
            (Adjunction.homEquiv (L.lanAdjunction D) (obj (obj (whiskeringLeft C₁ C₂ D) T) F₂)
              (obj (R.lan ⋙ obj (whiskeringLeft C₃ C₄ D) B) F₂)) :
          (a :
              ((whiskeringLeft C₁ C₂ D).obj T).obj F₂ ⟶
                ((whiskeringLeft C₁ C₃ D).obj L).obj ((R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).obj F₂)) →
            L.lan.obj (((whiskeringLeft C₁ C₂ D).obj T).obj F₂) ⟶ (R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).obj F₂)
        (StructuredArrow.hom ((LeftExtension.mk (obj R.lan F₂) (NatTrans.app R.lanUnit F₂)).compTwoSquare w)))
    ((Equiv.symm
            (Adjunction.homEquiv (L.lanAdjunction D) (obj (obj (whiskeringLeft C₁ C₂ D) T) F₁)
              (obj (R.lan ⋙ obj (whiskeringLeft C₃ C₄ D) B) F₁)) :
          (a :
              ((whiskeringLeft C₁ C₂ D).obj T).obj F₁ ⟶
                ((whiskeringLeft C₁ C₃ D).obj L).obj ((R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).obj F₁)) →
            L.lan.obj (((whiskeringLeft C₁ C₂ D).obj T).obj F₁) ⟶ (R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).obj F₁)
        (StructuredArrow.hom ((LeftExtension.mk (obj R.lan F₁) (NatTrans.app R.lanUnit F₁)).compTwoSquare w)) ≫
      map (R.lan ⋙ obj (whiskeringLeft C₃ C₄ D) B) τ)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F₁ F₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D
τ : F₁ ⟶ F₂
⊢ Eq (α := obj L.lan (T ⋙ F₁) ⟶ B ⋙ obj R.lan F₂)
    (map L.lan (T.whiskerLeft τ) ≫
      (Equiv.symm (Adjunction.homEquiv (L.lanAdjunction D) (T ⋙ F₂) (B ⋙ obj R.lan F₂)) :
          (a : T ⋙ F₂ ⟶ L ⋙ B ⋙ R.lan.obj F₂) → L.lan.obj (T ⋙ F₂) ⟶ B ⋙ R.lan.obj F₂)
        (T.whiskerLeft (NatTrans.app R.lanUnit F₂) ≫
          (T.associator R (obj R.lan F₂)).inv ≫
            whiskerRight w.natTrans (obj R.lan F₂) ≫ (L.associator B (obj R.lan F₂)).hom))
    ((Equiv.symm (Adjunction.homEquiv (L.lanAdjunction D) (T ⋙ F₁) (B ⋙ obj R.lan F₁)) :
          (a : T ⋙ F₁ ⟶ L ⋙ B ⋙ R.lan.obj F₁) → L.lan.obj (T ⋙ F₁) ⟶ B ⋙ R.lan.obj F₁)
        (T.whiskerLeft (NatTrans.app R.lanUnit F₁) ≫
          (T.associator R (obj R.lan F₁)).inv ≫
            whiskerRight w.natTrans (obj R.lan F₁) ≫ (L.associator B (obj R.lan F₁)).hom) ≫
      B.whiskerLeft (map R.lan τ))

Tactic:
(Adjunction.homEquiv_naturality_left_symm ..).symm.trans
      (Eq.trans ?_ (Adjunction.homEquiv_naturality_right_symm ..))

Premises used: CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv_naturality_left_symm, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F₁ F₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D
τ : F₁ ⟶ F₂
refine :
  Eq (α := obj L.lan (T ⋙ F₁) ⟶ B ⋙ obj R.lan F₂)
    ((Equiv.symm (Adjunction.homEquiv (L.lanAdjunction D) (T ⋙ F₁) (B ⋙ obj R.lan F₂)) :
          (a : T ⋙ F₁ ⟶ ((whiskeringLeft C₁ C₃ D).obj L).obj (B ⋙ R.lan.obj F₂)) →
            L.lan.obj (T ⋙ F₁) ⟶ B ⋙ R.lan.obj F₂)
        (T.whiskerLeft τ ≫
          T.whiskerLeft (NatTrans.app R.lanUnit F₂) ≫
            (T.associator R (obj R.lan F₂)).inv ≫
              whiskerRight w.natTrans (obj R.lan F₂) ≫ (L.associator B (obj R.lan F₂)).hom) :
      obj L.lan (T ⋙ F₁) ⟶ B ⋙ obj R.lan F₂)
    ((Equiv.symm (Adjunction.homEquiv (L.lanAdjunction D) (T ⋙ F₁) (B ⋙ obj R.lan F₂)) :
          (a : T ⋙ F₁ ⟶ ((whiskeringLeft C₁ C₃ D).obj L).obj (B ⋙ R.lan.obj F₂)) →
            L.lan.obj (T ⋙ F₁) ⟶ B ⋙ R.lan.obj F₂)
        ((T.whiskerLeft (NatTrans.app R.lanUnit F₁) ≫
            (T.associator R (obj R.lan F₁)).inv ≫
              whiskerRight w.natTrans (obj R.lan F₁) ≫ (L.associator B (obj R.lan F₁)).hom) ≫
          map (obj (whiskeringLeft C₁ C₃ D) L) (B.whiskerLeft (map R.lan τ))) :
      obj L.lan (T ⋙ F₁) ⟶ B ⋙ obj R.lan F₂)
⊢ Eq (α := obj L.lan (T ⋙ F₁) ⟶ B ⋙ obj R.lan F₂)
    (map L.lan (T.whiskerLeft τ) ≫
      (Equiv.symm (Adjunction.homEquiv (L.lanAdjunction D) (T ⋙ F₂) (B ⋙ obj R.lan F₂)) :
          (a : T ⋙ F₂ ⟶ L ⋙ B ⋙ R.lan.obj F₂) → L.lan.obj (T ⋙ F₂) ⟶ B ⋙ R.lan.obj F₂)
        (T.whiskerLeft (NatTrans.app R.lanUnit F₂) ≫
          (T.associator R (obj R.lan F₂)).inv ≫
            whiskerRight w.natTrans (obj R.lan F₂) ≫ (L.associator B (obj R.lan F₂)).hom))
    ((Equiv.symm (Adjunction.homEquiv (L.lanAdjunction D) (T ⋙ F₁) (B ⋙ obj R.lan F₁)) :
          (a : T ⋙ F₁ ⟶ L ⋙ B ⋙ R.lan.obj F₁) → L.lan.obj (T ⋙ F₁) ⟶ B ⋙ R.lan.obj F₁)
        (T.whiskerLeft (NatTrans.app R.lanUnit F₁) ≫
          (T.associator R (obj R.lan F₁)).inv ≫
            whiskerRight w.natTrans (obj R.lan F₁) ≫ (L.associator B (obj R.lan F₁)).hom) ≫
      B.whiskerLeft (map R.lan τ))

Tactic:
refine (Adjunction.homEquiv_naturality_left_symm ..).symm.trans
      (Eq.trans ?_ (Adjunction.homEquiv_naturality_right_symm ..))

Premises used: CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv_naturality_left_symm, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F₁ F₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D
τ : F₁ ⟶ F₂
h :
  T.whiskerLeft τ ≫
      T.whiskerLeft (NatTrans.app R.lanUnit F₂) ≫
        (T.associator R (obj R.lan F₂)).inv ≫
          whiskerRight w.natTrans (obj R.lan F₂) ≫ (L.associator B (obj R.lan F₂)).hom =
    (T.whiskerLeft (NatTrans.app R.lanUnit F₁) ≫
        (T.associator R (obj R.lan F₁)).inv ≫
          whiskerRight w.natTrans (obj R.lan F₁) ≫ (L.associator B (obj R.lan F₁)).hom) ≫
      map (obj (whiskeringLeft C₁ C₃ D) L) (B.whiskerLeft (map R.lan τ))
⊢ Eq (α := obj L.lan (T ⋙ F₁) ⟶ B ⋙ obj R.lan F₂)
    ((Equiv.symm (Adjunction.homEquiv (L.lanAdjunction D) (T ⋙ F₁) (B ⋙ obj R.lan F₂)) :
          (a : T ⋙ F₁ ⟶ ((whiskeringLeft C₁ C₃ D).obj L).obj (B ⋙ R.lan.obj F₂)) →
            L.lan.obj (T ⋙ F₁) ⟶ B ⋙ R.lan.obj F₂)
        (T.whiskerLeft τ ≫
          T.whiskerLeft (NatTrans.app R.lanUnit F₂) ≫
            (T.associator R (obj R.lan F₂)).inv ≫
              whiskerRight w.natTrans (obj R.lan F₂) ≫ (L.associator B (obj R.lan F₂)).hom) :
      obj L.lan (T ⋙ F₁) ⟶ B ⋙ obj R.lan F₂)
    ((Equiv.symm (Adjunction.homEquiv (L.lanAdjunction D) (T ⋙ F₁) (B ⋙ obj R.lan F₂)) :
          (a : T ⋙ F₁ ⟶ ((whiskeringLeft C₁ C₃ D).obj L).obj (B ⋙ R.lan.obj F₂)) →
            L.lan.obj (T ⋙ F₁) ⟶ B ⋙ R.lan.obj F₂)
        ((T.whiskerLeft (NatTrans.app R.lanUnit F₁) ≫
            (T.associator R (obj R.lan F₁)).inv ≫
              whiskerRight w.natTrans (obj R.lan F₁) ≫ (L.associator B (obj R.lan F₁)).hom) ≫
          map (obj (whiskeringLeft C₁ C₃ D) L) (B.whiskerLeft (map R.lan τ))) :
      obj L.lan (T ⋙ F₁) ⟶ B ⋙ obj R.lan F₂)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F₁ F₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D
τ : F₁ ⟶ F₂
h :
  ∀ (X : C₁),
    (T.whiskerLeft τ ≫
            T.whiskerLeft (NatTrans.app R.lanUnit F₂) ≫
              (T.associator R (obj R.lan F₂)).inv ≫
                whiskerRight w.natTrans (obj R.lan F₂) ≫ (L.associator B (obj R.lan F₂)).hom).app
        X =
      NatTrans.app
        ((T.whiskerLeft (NatTrans.app R.lanUnit F₁) ≫
            (T.associator R (obj R.lan F₁)).inv ≫
              whiskerRight w.natTrans (obj R.lan F₁) ≫ (L.associator B (obj R.lan F₁)).hom) ≫
          map (obj (whiskeringLeft C₁ C₃ D) L) (B.whiskerLeft (map R.lan τ)))
        X
⊢ T.whiskerLeft τ ≫
      T.whiskerLeft (NatTrans.app R.lanUnit F₂) ≫
        (T.associator R (obj R.lan F₂)).inv ≫
          whiskerRight w.natTrans (obj R.lan F₂) ≫ (L.associator B (obj R.lan F₂)).hom =
    (T.whiskerLeft (NatTrans.app R.lanUnit F₁) ≫
        (T.associator R (obj R.lan F₁)).inv ≫
          whiskerRight w.natTrans (obj R.lan F₁) ≫ (L.associator B (obj R.lan F₁)).hom) ≫
      map (obj (whiskeringLeft C₁ C₃ D) L) (B.whiskerLeft (map R.lan τ))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F₁ F₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D
τ : F₁ ⟶ F₂
X : C₁
⊢ Eq (α :=
    (obj (𝟭 (Functor.{v₂, v₅, u₂, u₅} C₂ D)) F₁).obj (T.obj X) ⟶
      (obj (R.lan ⋙ obj (whiskeringLeft C₂ C₄ D) R) F₂).obj (T.obj X))
    (NatTrans.app (map (𝟭 (Functor.{v₂, v₅, u₂, u₅} C₂ D)) τ) (T.obj X) ≫
      NatTrans.app (NatTrans.app R.lanUnit F₂) (T.obj X))
    (NatTrans.app (NatTrans.app R.lanUnit F₁) (T.obj X) ≫
      NatTrans.app (map (R.lan ⋙ obj (whiskeringLeft C₂ C₄ D) R) τ) (T.obj X))

Tactic:
have := R.lanUnit.naturality_app (T.obj X) τ
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F₁ F₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D
τ : F₁ ⟶ F₂
X : C₁
this :
  Eq (α :=
    (obj (𝟭 (Functor.{v₂, v₅, u₂, u₅} C₂ D)) F₁).obj (T.obj X) ⟶
      (obj (R.lan ⋙ obj (whiskeringLeft C₂ C₄ D) R) F₂).obj (T.obj X))
    (NatTrans.app (map (𝟭 (Functor.{v₂, v₅, u₂, u₅} C₂ D)) τ) (T.obj X) ≫
      NatTrans.app (NatTrans.app R.lanUnit F₂) (T.obj X))
    (NatTrans.app (NatTrans.app R.lanUnit F₁) (T.obj X) ≫
      NatTrans.app (map (R.lan ⋙ obj (whiskeringLeft C₂ C₄ D) R) τ) (T.obj X))
⊢ (T.whiskerLeft τ ≫
          T.whiskerLeft (NatTrans.app R.lanUnit F₂) ≫
            (T.associator R (obj R.lan F₂)).inv ≫
              whiskerRight w.natTrans (obj R.lan F₂) ≫ (L.associator B (obj R.lan F₂)).hom).app
      X =
    NatTrans.app
      ((T.whiskerLeft (NatTrans.app R.lanUnit F₁) ≫
          (T.associator R (obj R.lan F₁)).inv ≫
            whiskerRight w.natTrans (obj R.lan F₁) ≫ (L.associator B (obj R.lan F₁)).hom) ≫
        map (obj (whiskeringLeft C₁ C₃ D) L) (B.whiskerLeft (map R.lan τ)))
      X

Tactic:
simp [reassoc_of% this]
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
rw :
  (obj (R.lan ⋙ obj (whiskeringLeft C₃ C₄ D) B) F).IsLeftKanExtension
      (StructuredArrow.hom ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w)) ↔
    (StructuredArrow.right
          ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w)).IsLeftKanExtension
      (StructuredArrow.hom ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w))
⊢ IsIso (X := obj (obj (whiskeringLeft C₁ C₂ D) T ⋙ L.lan) F) (Y := obj (R.lan ⋙ obj (whiskeringLeft C₃ C₄ D) B) F)
      (NatTrans.app w.lanBaseChange F) ↔
    (StructuredArrow.right
          ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w)).IsLeftKanExtension
      (StructuredArrow.hom ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w))

Tactic:
rw [lanBaseChange_app, isIso_lanAdjunction_homEquiv_symm_iff]

Premises used: CategoryTheory.Functor.isIso_lanAdjunction_homEquiv_symm_iff, CategoryTheory.TwoSquare.lanBaseChange_app
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
⊢ (obj (R.lan ⋙ obj (whiskeringLeft C₃ C₄ D) B) F).IsLeftKanExtension
      (StructuredArrow.hom ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w)) ↔
    (StructuredArrow.right
          ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w)).IsLeftKanExtension
      (StructuredArrow.hom ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
inst_7 : R.HasPointwiseLeftKanExtension F
inst_8 : w.GuitartExact
rw :
  (StructuredArrow.right
        ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w)).IsLeftKanExtension
    (StructuredArrow.hom ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w))
⊢ IsIso (X := obj (obj (whiskeringLeft C₁ C₂ D) T ⋙ L.lan) F) (Y := obj (R.lan ⋙ obj (whiskeringLeft C₃ C₄ D) B) F)
    (NatTrans.app w.lanBaseChange F)

Tactic:
rw [isIso_lanBaseChange_app_iff]

Premises used: CategoryTheory.TwoSquare.isIso_lanBaseChange_app_iff
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
inst_7 : R.HasPointwiseLeftKanExtension F
inst_8 : w.GuitartExact
hF : (LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).IsPointwiseLeftKanExtension :=
  isPointwiseLeftKanExtensionOfIsLeftKanExtension (obj R.lan F) (NatTrans.app R.lanUnit F)
⊢ (StructuredArrow.right
        ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w)).IsLeftKanExtension
    (StructuredArrow.hom ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w))

Tactic:
(hF.compTwoSquare w).isLeftKanExtension

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.compTwoSquare
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasLeftKanExtension F
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
inst_7 : R.HasPointwiseLeftKanExtension F
inst_8 : w.GuitartExact
hF : (LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).IsPointwiseLeftKanExtension :=
  isPointwiseLeftKanExtensionOfIsLeftKanExtension (obj R.lan F) (NatTrans.app R.lanUnit F)
⊢ (StructuredArrow.right
        ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w)).IsLeftKanExtension
    (StructuredArrow.hom ((LeftExtension.mk (obj R.lan F) (NatTrans.app R.lanUnit F)).compTwoSquare w))

Tactic:
exact (hF.compTwoSquare w).isLeftKanExtension

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.compTwoSquare
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasPointwiseLeftKanExtension F
inst_7 : w.GuitartExact
rw :
  ∀ (X : Functor.{v₂, v₅, u₂, u₅} C₂ D),
    IsIso (X := obj (obj (whiskeringLeft C₁ C₂ D) T ⋙ L.lan) X) (Y := obj (R.lan ⋙ obj (whiskeringLeft C₃ C₄ D) B) X)
      (NatTrans.app w.lanBaseChange X)
⊢ IsIso (C := Functor.{v₂, v₅, u₂, u₅} C₂ D ⥤ Functor.{v₃, v₅, u₃, u₅} C₃ D) (X :=
    obj (whiskeringLeft C₁ C₂ D) T ⋙ L.lan) (Y := R.lan ⋙ obj (whiskeringLeft C₃ C₄ D) B) w.lanBaseChange

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : ∀ (F : Functor.{v₁, v₅, u₁, u₅} C₁ D), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v₂, v₅, u₂, u₅} C₂ D), R.HasPointwiseLeftKanExtension F
inst_7 : w.GuitartExact
⊢ ∀ (X : Functor.{v₂, v₅, u₂, u₅} C₂ D),
    IsIso (X := obj (obj (whiskeringLeft C₁ C₂ D) T ⋙ L.lan) X) (Y := obj (R.lan ⋙ obj (whiskeringLeft C₃ C₄ D) B) X)
      (NatTrans.app w.lanBaseChange X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GuitartExact.Opposite
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₃ : C₃ᵒᵖ
X₂ : C₂ᵒᵖ
g : B.op.obj X₃ ⟶ R.op.obj X₂
f : (w.op.StructuredArrowRightwards g)ᵒᵖ
⊢ (R.map (StructuredArrow.right (Opposite.unop f)).hom.unop ≫
        w.app (Opposite.unop (StructuredArrow.right (Opposite.unop f)).left) ≫
          B.map (StructuredArrow.hom (Opposite.unop f)).left.unop).op =
    g.unop.op

Tactic:
simpa using CostructuredArrow.w f.unop.hom

Premises used: CategoryTheory.StructuredArrow.hom, CategoryTheory.CostructuredArrow.w, Opposite.unop