awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
dsimp : (StructuredArrow.hom f₁).left ≫ T.map (StructuredArrow.Hom.right φ).left = (StructuredArrow.hom f₂).left
⊢ StructuredArrow.hom
        (CostructuredArrow.left (D := StructuredArrow (R.obj X₂) B) (S := w.structuredArrowDownwards X₂) (T :=
          StructuredArrow.mk g)
          (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₁).left)
            (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯))) ≫
      T.map (StructuredArrow.Hom.right φ).left =
    StructuredArrow.hom
      (CostructuredArrow.left (D := StructuredArrow (R.obj X₂) B) (S := w.structuredArrowDownwards X₂) (T :=
        StructuredArrow.mk g)
        (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₂).left)
          (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
rw :
  (StructuredArrow.hom f₁).left ≫ T.map (StructuredArrow.Hom.right φ).left =
    (StructuredArrow.hom f₁ ≫ (w.costructuredArrowRightwards X₃).map (StructuredArrow.Hom.right φ)).left
⊢ (StructuredArrow.hom f₁).left ≫ T.map (StructuredArrow.Hom.right φ).left = (StructuredArrow.hom f₂).left

Tactic:
rw [← StructuredArrow.w φ]

Premises used: CategoryTheory.StructuredArrow.w
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
⊢ (StructuredArrow.hom f₁).left ≫ T.map (StructuredArrow.Hom.right φ).left =
    (StructuredArrow.hom f₁ ≫ (w.costructuredArrowRightwards X₃).map (StructuredArrow.Hom.right φ)).left

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
h :
  Eq (α :=
    ((w.structuredArrowDownwards X₂).obj
          (CostructuredArrow.left (D := StructuredArrow (R.obj X₂) B) (S := w.structuredArrowDownwards X₂) (T :=
            StructuredArrow.mk g)
            (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₁).left)
              (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯)))).right ⟶
      (StructuredArrow.mk g).right)
    (StructuredArrow.Hom.right
      (CategoryStruct.comp (Y :=
        (w.structuredArrowDownwards X₂).obj
          (CostructuredArrow.left (D := StructuredArrow (R.obj X₂) B) (S := w.structuredArrowDownwards X₂) (T :=
            StructuredArrow.mk g)
            (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₂).left)
              (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯))))
        ((w.structuredArrowDownwards X₂).map (StructuredArrow.homMk (StructuredArrow.Hom.right φ).left ⋯))
        (CostructuredArrow.hom
          (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₂).left)
            (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯)))))
    (StructuredArrow.Hom.right
      (CostructuredArrow.hom
        (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₁).left)
          (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯))))
⊢ Eq (α :=
    (w.structuredArrowDownwards X₂).obj
        (CostructuredArrow.left (D := StructuredArrow (R.obj X₂) B) (S := w.structuredArrowDownwards X₂) (T :=
          StructuredArrow.mk g)
          (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₁).left)
            (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯))) ⟶
      StructuredArrow.mk g)
    (CategoryStruct.comp (Y :=
      (w.structuredArrowDownwards X₂).obj
        (CostructuredArrow.left (D := StructuredArrow (R.obj X₂) B) (S := w.structuredArrowDownwards X₂) (T :=
          StructuredArrow.mk g)
          (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₂).left)
            (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯))))
      ((w.structuredArrowDownwards X₂).map (StructuredArrow.homMk (StructuredArrow.Hom.right φ).left ⋯))
      (CostructuredArrow.hom
        (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₂).left)
          (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯))))
    (CostructuredArrow.hom
      (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₁).left)
        (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
⊢ Eq (α :=
    ((w.structuredArrowDownwards X₂).obj
          (CostructuredArrow.left (D := StructuredArrow (R.obj X₂) B) (S := w.structuredArrowDownwards X₂) (T :=
            StructuredArrow.mk g)
            (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₁).left)
              (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯)))).right ⟶
      (StructuredArrow.mk g).right)
    (StructuredArrow.Hom.right
      (CategoryStruct.comp (Y :=
        (w.structuredArrowDownwards X₂).obj
          (CostructuredArrow.left (D := StructuredArrow (R.obj X₂) B) (S := w.structuredArrowDownwards X₂) (T :=
            StructuredArrow.mk g)
            (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₂).left)
              (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯))))
        ((w.structuredArrowDownwards X₂).map (StructuredArrow.homMk (StructuredArrow.Hom.right φ).left ⋯))
        (CostructuredArrow.hom
          (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₂).left)
            (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯)))))
    (StructuredArrow.Hom.right
      (CostructuredArrow.hom
        (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₁).left)
          (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯))))

Tactic:
CostructuredArrow.w φ.right

Premises used: CategoryTheory.Functor.comp, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.w, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
⊢ Eq (α :=
    ((w.structuredArrowDownwards X₂).obj
          (CostructuredArrow.left (D := StructuredArrow (R.obj X₂) B) (S := w.structuredArrowDownwards X₂) (T :=
            StructuredArrow.mk g)
            (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₁).left)
              (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯)))).right ⟶
      (StructuredArrow.mk g).right)
    (StructuredArrow.Hom.right
      (CategoryStruct.comp (Y :=
        (w.structuredArrowDownwards X₂).obj
          (CostructuredArrow.left (D := StructuredArrow (R.obj X₂) B) (S := w.structuredArrowDownwards X₂) (T :=
            StructuredArrow.mk g)
            (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₂).left)
              (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯))))
        ((w.structuredArrowDownwards X₂).map (StructuredArrow.homMk (StructuredArrow.Hom.right φ).left ⋯))
        (CostructuredArrow.hom
          (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₂).left)
            (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯)))))
    (StructuredArrow.Hom.right
      (CostructuredArrow.hom
        (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₁).left)
          (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯))))

Tactic:
exact CostructuredArrow.w φ.right

Premises used: CategoryTheory.CostructuredArrow.w, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f : w.CostructuredArrowDownwards g
⊢ R.map (CostructuredArrow.left f).hom ≫
      ((w.costructuredArrowRightwards X₃).obj
          (CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f)))).hom =
    (CostructuredArrow.mk g).hom

Tactic:
simpa using StructuredArrow.w f.hom

Premises used: CategoryTheory.CostructuredArrow.hom, CategoryTheory.StructuredArrow.w
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
dsimp :
  L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom f₂) =
    StructuredArrow.Hom.right (CostructuredArrow.hom f₁)
⊢ Eq (α :=
    L.obj
        (CostructuredArrow.left.{v₁, v₃, u₁, u₃} (D := C₃) (S := L) (T := (StructuredArrow.mk g).right)
          (StructuredArrow.right (D := CostructuredArrow R (B.obj X₃)) (S := CostructuredArrow.mk g) (T :=
            w.costructuredArrowRightwards X₃)
            (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₁)))
              (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯)))) ⟶
      (StructuredArrow.mk g).right)
    (L.map (StructuredArrow.Hom.right φ.left) ≫
      CostructuredArrow.hom
        (StructuredArrow.right (D := CostructuredArrow R (B.obj X₃)) (S := CostructuredArrow.mk g) (T :=
          w.costructuredArrowRightwards X₃)
          (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₂)))
            (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯))))
    (CostructuredArrow.hom
      (StructuredArrow.right (D := CostructuredArrow R (B.obj X₃)) (S := CostructuredArrow.mk g) (T :=
        w.costructuredArrowRightwards X₃)
        (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₁)))
          (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯))))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
rw :
  L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom f₂) =
    StructuredArrow.Hom.right ((w.structuredArrowDownwards X₂).map φ.left ≫ CostructuredArrow.hom f₂)
⊢ L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom f₂) =
    StructuredArrow.Hom.right (CostructuredArrow.hom f₁)

Tactic:
rw [← CostructuredArrow.w φ]

Premises used: CategoryTheory.CostructuredArrow.w
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
⊢ L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom f₂) =
    StructuredArrow.Hom.right ((w.structuredArrowDownwards X₂).map φ.left ≫ CostructuredArrow.hom f₂)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
⊢ Eq (α :=
    (CostructuredArrow.mk g).left ⟶
      ((w.costructuredArrowRightwards X₃).obj
          (StructuredArrow.right (D := CostructuredArrow R (B.obj X₃)) (S := CostructuredArrow.mk g) (T :=
            w.costructuredArrowRightwards X₃)
            (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₂)))
              (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯)))).left)
    (CommaMorphism.left
      (CategoryStruct.comp (Y :=
        (w.costructuredArrowRightwards X₃).obj
          (StructuredArrow.right (D := CostructuredArrow R (B.obj X₃)) (S := CostructuredArrow.mk g) (T :=
            w.costructuredArrowRightwards X₃)
            (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₁)))
              (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯))))
        (StructuredArrow.hom
          (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₁)))
            (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯)))
        ((w.costructuredArrowRightwards X₃).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯))))
    (CommaMorphism.left
      (StructuredArrow.hom
        (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₂)))
          (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯))))

Tactic:
StructuredArrow.w φ.left

Premises used: CategoryTheory.CommaMorphism.left, CategoryTheory.StructuredArrow.w, CategoryTheory.StructuredArrow
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
⊢ Eq (α :=
    (CostructuredArrow.mk g).left ⟶
      ((w.costructuredArrowRightwards X₃).obj
          (StructuredArrow.right (D := CostructuredArrow R (B.obj X₃)) (S := CostructuredArrow.mk g) (T :=
            w.costructuredArrowRightwards X₃)
            (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₂)))
              (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯)))).left)
    (CommaMorphism.left
      (CategoryStruct.comp (Y :=
        (w.costructuredArrowRightwards X₃).obj
          (StructuredArrow.right (D := CostructuredArrow R (B.obj X₃)) (S := CostructuredArrow.mk g) (T :=
            w.costructuredArrowRightwards X₃)
            (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₁)))
              (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯))))
        (StructuredArrow.hom
          (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₁)))
            (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯)))
        ((w.costructuredArrowRightwards X₃).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯))))
    (CommaMorphism.left
      (StructuredArrow.hom
        (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₂)))
          (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯))))

Tactic:
exact StructuredArrow.w φ.left

Premises used: CategoryTheory.CommaMorphism.left, CategoryTheory.StructuredArrow.w
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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 : R.obj X₂ ⟶ B.obj X₃
⊢ IsConnected (w.StructuredArrowRightwards g) ↔ IsConnected (w.CostructuredArrowDownwards g)

Tactic:
isConnected_iff_of_equivalence (w.equivalenceJ g)

Premises used: CategoryTheory.isConnected_iff_of_equivalence, CategoryTheory.TwoSquare.equivalenceJ
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A : w.CostructuredArrowDownwards g
⊢ R.map (γ ≫ (CostructuredArrow.left A).hom) ≫
      w.app (CostructuredArrow.left A).right ≫ B.map (StructuredArrow.Hom.right (CostructuredArrow.hom A)) =
    g'

Tactic:
simpa [← hγ] using R.map γ ≫= StructuredArrow.w A.hom

Premises used: CategoryTheory.CostructuredArrow.hom, CategoryTheory.Functor.map, CategoryTheory.StructuredArrow.w
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A A' : w.CostructuredArrowDownwards g
φ : A ⟶ A'
dsimp :
  (γ ≫ (CostructuredArrow.left A).hom) ≫ T.map (StructuredArrow.Hom.right φ.left) = γ ≫ (CostructuredArrow.left A').hom
⊢ (CostructuredArrow.left
          (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A).right (γ ≫ (CostructuredArrow.left A).hom)
            (StructuredArrow.Hom.right (CostructuredArrow.hom A)) ⋯)).hom ≫
      T.map (StructuredArrow.Hom.right φ.left) =
    (CostructuredArrow.left
        (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A').right (γ ≫ (CostructuredArrow.left A').hom)
          (StructuredArrow.Hom.right (CostructuredArrow.hom A')) ⋯)).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A A' : w.CostructuredArrowDownwards g
φ : A ⟶ A'
rw : γ ≫ (CostructuredArrow.left A).hom ≫ T.map (StructuredArrow.Hom.right φ.left) = γ ≫ (CostructuredArrow.left A').hom
rw₁ rw₂ : γ ≫ A'.left.hom = γ ≫ (CostructuredArrow.left A').hom
⊢ (γ ≫ (CostructuredArrow.left A).hom) ≫ T.map (StructuredArrow.Hom.right φ.left) = γ ≫ (CostructuredArrow.left A').hom

Tactic:
rw [assoc, StructuredArrow.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.StructuredArrow.w
-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
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₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A A' : w.CostructuredArrowDownwards g
φ : A ⟶ A'
h :
  StructuredArrow.Hom.right
      ((w.structuredArrowDownwards X₂').map (StructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯) ≫
        CostructuredArrow.hom
          (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A').right (γ ≫ (CostructuredArrow.left A').hom)
            (StructuredArrow.Hom.right (CostructuredArrow.hom A')) ⋯)) =
    StructuredArrow.Hom.right
      (CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A).right (γ ≫ (CostructuredArrow.left A).hom)
          (StructuredArrow.Hom.right (CostructuredArrow.hom A)) ⋯))
⊢ (w.structuredArrowDownwards X₂').map (StructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯) ≫
      CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A').right (γ ≫ (CostructuredArrow.left A').hom)
          (StructuredArrow.Hom.right (CostructuredArrow.hom A')) ⋯) =
    CostructuredArrow.hom
      (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A).right (γ ≫ (CostructuredArrow.left A).hom)
        (StructuredArrow.Hom.right (CostructuredArrow.hom A)) ⋯)

Tactic:
ext