awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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 : w.GuitartExact
inst_6 : B.EssSurj
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
⊢ (∀ (Y : C₃), L.HasPointwiseLeftKanExtensionAt (T ⋙ F) Y) ↔ ∀ (Y : C₄), R.HasPointwiseLeftKanExtensionAt F Y
have simp : (∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)) ↔ ∀ (Y : C₄), R.HasPointwiseLeftKanExtensionAt F Y
Tactic: simp only [hasPointwiseLeftKanExtensionAt_iff w]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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 : w.GuitartExact
inst_6 : B.EssSurj
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
⊢ (∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)) ↔ ∀ (Y : C₄), R.HasPointwiseLeftKanExtensionAt F Y
have refine : ∀ (h : ∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)) (X₄ : C₄), R.HasPointwiseLeftKanExtensionAt F X₄
Tactic: refine ⟨fun h X₄ ↦ ?_, fun h _ ↦ h _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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 : w.GuitartExact
inst_6 : B.EssSurj
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
h : ∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)
X₄ : C₄
⊢ R.HasPointwiseLeftKanExtensionAt F X₄
have rw : R.HasPointwiseLeftKanExtensionAt F (B.obj (B.objPreimage X₄))
Tactic: rw [← Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso _ _ (B.objObjPreimageIso X₄)]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (hypothesis)
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 : w.GuitartExact
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
inst_6 : R.HasPointwiseLeftKanExtension F
⊢ L.HasLeftKanExtension (T ⋙ F)
have this : L.HasPointwiseLeftKanExtension (T ⋙ F)
Tactic: have := w.hasPointwiseLeftKanExtension F
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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 (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) τ)
have 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 τ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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 τ))
have 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₂)
Tactic: refine (Adjunction.homEquiv_naturality_left_symm ..).symm.trans
      (Eq.trans ?_ (Adjunction.homEquiv_naturality_right_symm ..))
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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₂)
    ((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₂)
have 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 τ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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₂
⊢ 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 τ))
have 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
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (hypothesis)
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₁
⊢ (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
have 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))
Tactic: have := R.lanUnit.naturality_app (T.obj X) τ
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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
⊢ 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))
have 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))
Tactic: rw [lanBaseChange_app, isIso_lanAdjunction_homEquiv_symm_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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
⊢ 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)
have 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))
Tactic: rw [isIso_lanBaseChange_app_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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
⊢ 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
have 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)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Opposite (goal)
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 f' : (w.op.StructuredArrowRightwards g)ᵒᵖ
φ : f ⟶ f'
⊢ Functor.map (w.structuredArrowDownwards (Opposite.unop X₂))
        (StructuredArrow.homMk (StructuredArrow.Hom.right φ.unop).left.unop ⋯) ≫
      CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g.unop (Opposite.unop (StructuredArrow.right (Opposite.unop f')).left)
          (StructuredArrow.right (Opposite.unop f')).hom.unop (StructuredArrow.hom (Opposite.unop f')).left.unop ⋯) =
    CostructuredArrow.hom
      (CostructuredArrowDownwards.mk w g.unop (Opposite.unop (StructuredArrow.right (Opposite.unop f)).left)
        (StructuredArrow.right (Opposite.unop f)).hom.unop (StructuredArrow.hom (Opposite.unop f)).left.unop ⋯)
have h : StructuredArrow.Hom.right
    (Functor.map (w.structuredArrowDownwards (Opposite.unop X₂))
        (StructuredArrow.homMk (StructuredArrow.Hom.right φ.unop).left.unop sorry) ≫
      CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g.unop (Opposite.unop (StructuredArrow.right (Opposite.unop f')).left)
          (StructuredArrow.right (Opposite.unop f')).hom.unop (StructuredArrow.hom (Opposite.unop f')).left.unop sorry)) =
  StructuredArrow.Hom.right
    (CostructuredArrow.hom
      (CostructuredArrowDownwards.mk w g.unop (Opposite.unop (StructuredArrow.right (Opposite.unop f)).left)
        (StructuredArrow.right (Opposite.unop f)).hom.unop (StructuredArrow.hom (Opposite.unop f)).left.unop sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Opposite (goal)
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 f' : w.CostructuredArrowDownwards g.unop
φ : f ⟶ f'
⊢ StructuredArrow.hom
        (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f').right)
          (StructuredArrow.Hom.right (CostructuredArrow.hom f')).op (CostructuredArrow.left f').hom.op ⋯) ≫
      (w.op.costructuredArrowRightwards X₂).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left).op ⋯) =
    StructuredArrow.hom
      (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f).right)
        (StructuredArrow.Hom.right (CostructuredArrow.hom f)).op (CostructuredArrow.left f).hom.op ⋯)
have h : CommaMorphism.left
    (StructuredArrow.hom
        (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f').right)
          (StructuredArrow.Hom.right (CostructuredArrow.hom f')).op (CostructuredArrow.left f').hom.op sorry) ≫
      (w.op.costructuredArrowRightwards X₂).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left).op sorry)) =
  (StructuredArrow.hom
      (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f).right)
        (StructuredArrow.Hom.right (CostructuredArrow.hom f)).op (CostructuredArrow.left f).hom.op sorry)).left
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Opposite (goal)
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
inst_4 : w.GuitartExact
⊢ w.op.GuitartExact
have rw : ∀ {X₂ : C₃ᵒᵖ} {X₃ : C₂ᵒᵖ} (g : B.op.obj X₂ ⟶ R.op.obj X₃), IsConnected (w.op.StructuredArrowRightwards g)
Tactic: rw [guitartExact_iff_isConnected_rightwards]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Opposite (goal)
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
inst_4 : w.GuitartExact
X₃ : C₃ᵒᵖ
X₂ : C₂ᵒᵖ
g : B.op.obj X₃ ⟶ R.op.obj X₂
⊢ IsConnected (w.op.StructuredArrowRightwards g)
have rw : IsConnected (w.CostructuredArrowDownwards g.unop)
Tactic: rw [← isConnected_op_iff_isConnected,
    isConnected_iff_of_equivalence (w.structuredArrowRightwardsOpEquivalence g)]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Opposite (goal)
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
⊢ w.op.GuitartExact ↔ w.GuitartExact
have mp : w.op.GuitartExact → w.GuitartExact
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Opposite (goal)
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
mp : w.op.GuitartExact → w.GuitartExact
⊢ w.op.GuitartExact ↔ w.GuitartExact
have mpr : w.GuitartExact → w.op.GuitartExact
Tactic: constructor