awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 f' : (w.op.StructuredArrowRightwards g)ᵒᵖ
φ : f ⟶ f'
h :
  StructuredArrow.Hom.right
      (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 ⋯)) =
    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 ⋯))
⊢ 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 ⋯)

Tactic:
ext
-- 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 f' : (w.op.StructuredArrowRightwards g)ᵒᵖ
φ : f ⟶ f'
⊢ StructuredArrow.Hom.right
      (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 ⋯)) =
    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 ⋯))

Tactic:
Quiver.Hom.op_inj
            ((CostructuredArrow.proj _ _).congr_map (StructuredArrow.w φ.unop))

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, CategoryTheory.StructuredArrow.w, CategoryTheory.Functor.congr_map, CategoryTheory.CostructuredArrow.proj
-- 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 f' : (w.op.StructuredArrowRightwards g)ᵒᵖ
φ : f ⟶ f'
⊢ StructuredArrow.Hom.right
      (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 ⋯)) =
    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 ⋯))

Tactic:
exact Quiver.Hom.op_inj
            ((CostructuredArrow.proj _ _).congr_map (StructuredArrow.w φ.unop))

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, CategoryTheory.StructuredArrow.w, CategoryTheory.Functor.congr_map, CategoryTheory.CostructuredArrow.proj
-- 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 f' : w.CostructuredArrowDownwards g.unop
φ : f ⟶ f'
⊢ (T.op.map (StructuredArrow.Hom.right φ.left).op ≫
        (StructuredArrow.right
            (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f).right)
              (StructuredArrow.Hom.right (CostructuredArrow.hom f)).op (CostructuredArrow.left f).hom.op ⋯)).hom).unop =
    (StructuredArrow.right
          (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f').right)
            (StructuredArrow.Hom.right (CostructuredArrow.hom f')).op (CostructuredArrow.left f').hom.op ⋯)).hom.unop

Tactic:
StructuredArrow.w φ.left

Premises used: Quiver.Hom.unop, CategoryTheory.CommaMorphism.left, CategoryTheory.StructuredArrow.w
-- 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 f' : w.CostructuredArrowDownwards g.unop
φ : f ⟶ f'
⊢ (T.op.map (StructuredArrow.Hom.right φ.left).op ≫
        (StructuredArrow.right
            (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f).right)
              (StructuredArrow.Hom.right (CostructuredArrow.hom f)).op (CostructuredArrow.left f).hom.op ⋯)).hom).unop =
    (StructuredArrow.right
          (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f').right)
            (StructuredArrow.Hom.right (CostructuredArrow.hom f')).op (CostructuredArrow.left f').hom.op ⋯)).hom.unop

Tactic:
exact StructuredArrow.w φ.left

Premises used: CategoryTheory.CommaMorphism.left, CategoryTheory.StructuredArrow.w
-- 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 f' : w.CostructuredArrowDownwards g.unop
φ : f ⟶ f'
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 ⋯) ≫
        (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 ⋯)).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 ⋯) ≫
      (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 ⋯)

Tactic:
ext
-- 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 f' : w.CostructuredArrowDownwards g.unop
φ : f ⟶ f'
⊢ 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 ⋯) ≫
        (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 ⋯)).left

Tactic:
Quiver.Hom.unop_inj
              ((StructuredArrow.proj _ _).congr_map (CostructuredArrow.w φ))

Premises used: CategoryTheory.CostructuredArrow.w, Quiver.Hom.unop_inj, CategoryTheory.Functor.congr_map, CategoryTheory.StructuredArrow.proj
-- 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 f' : w.CostructuredArrowDownwards g.unop
φ : f ⟶ f'
⊢ 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 ⋯) ≫
        (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 ⋯)).left

Tactic:
exact Quiver.Hom.unop_inj
              ((StructuredArrow.proj _ _).congr_map (CostructuredArrow.w φ))

Premises used: CategoryTheory.CostructuredArrow.w, Quiver.Hom.unop_inj, CategoryTheory.Functor.congr_map, CategoryTheory.StructuredArrow.proj
-- 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
inst_4 : w.GuitartExact
rw : ∀ {X₂ : C₃ᵒᵖ} {X₃ : C₂ᵒᵖ} (g : B.op.obj X₂ ⟶ R.op.obj X₃), IsConnected (w.op.StructuredArrowRightwards g)
⊢ w.op.GuitartExact

Tactic:
rw [guitartExact_iff_isConnected_rightwards]

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_isConnected_rightwards
-- 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
inst_4 : w.GuitartExact
X₃ : C₃ᵒᵖ
X₂ : C₂ᵒᵖ
g : B.op.obj X₃ ⟶ R.op.obj X₂
rw : IsConnected (w.CostructuredArrowDownwards g.unop)
⊢ IsConnected (w.op.StructuredArrowRightwards g)

Tactic:
rw [← isConnected_op_iff_isConnected,
    isConnected_iff_of_equivalence (w.structuredArrowRightwardsOpEquivalence g)]

Premises used: CategoryTheory.isConnected_op_iff_isConnected, CategoryTheory.isConnected_iff_of_equivalence, CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence
-- 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
inst_4 : w.GuitartExact
X₃ : C₃ᵒᵖ
X₂ : C₂ᵒᵖ
g : B.op.obj X₃ ⟶ R.op.obj X₂
⊢ IsConnected (w.CostructuredArrowDownwards g.unop)

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
mp : w.op.GuitartExact → w.GuitartExact
mpr : w.GuitartExact → w.op.GuitartExact
⊢ w.op.GuitartExact ↔ w.GuitartExact

Tactic:
constructor
-- 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
h : w.op.GuitartExact
w₁ : TwoSquare T (opOp C₁) (opOp C₂) T.op.op := 𝟙 (T ⋙ opOp C₂)
w₂ : TwoSquare B.op.op (unopUnop C₃) (unopUnop C₄) B := 𝟙 (B.op.op ⋙ unopUnop C₄)
⊢ w = (w₁ ≫ᵥ w.op.op) ≫ᵥ w₂

Tactic:
have : w = (w₁ ≫ᵥ w.op.op) ≫ᵥ w₂ := by cat_disch
-- 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
h : w.op.GuitartExact
w₁ : TwoSquare T (opOp C₁) (opOp C₂) T.op.op := 𝟙 (T ⋙ opOp C₂)
w₂ : TwoSquare B.op.op (unopUnop C₃) (unopUnop C₄) B := 𝟙 (B.op.op ⋙ unopUnop C₄)
this : w = (w₁ ≫ᵥ w.op.op) ≫ᵥ w₂
mp : ((w₁ ≫ᵥ w.op.op) ≫ᵥ w₂).GuitartExact
⊢ w.GuitartExact

Tactic:
rw [this]
-- 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
h : w.op.GuitartExact
w₁ : TwoSquare T (opOp C₁) (opOp C₂) T.op.op := 𝟙 (T ⋙ opOp C₂)
w₂ : TwoSquare B.op.op (unopUnop C₃) (unopUnop C₄) B := 𝟙 (B.op.op ⋙ unopUnop C₄)
this : w = (w₁ ≫ᵥ w.op.op) ≫ᵥ w₂
⊢ ((w₁ ≫ᵥ w.op.op) ≫ᵥ w₂).GuitartExact

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
h : w.GuitartExact
⊢ w.op.GuitartExact

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
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
rw : (mk F (𝟭 C₁) (𝟭 C₂) F (𝟙 F)).op.GuitartExact
⊢ (mk F (𝟭 C₁) (𝟭 C₂) F (𝟙 F)).GuitartExact

Tactic:
rw [← guitartExact_op_iff]

Premises used: CategoryTheory.TwoSquare.guitartExact_op_iff
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
⊢ (mk F (𝟭 C₁) (𝟭 C₂) F (𝟙 F)).op.GuitartExact

Tactic:
apply guitartExact_id

Premises used: CategoryTheory.TwoSquare.guitartExact_id
-- 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
inst_4 : T.IsEquivalence
inst_5 : B.IsEquivalence
inst_6 : IsIso w.natTrans
rw : w.op.GuitartExact
⊢ w.GuitartExact

Tactic:
rw [← guitartExact_op_iff]

Premises used: CategoryTheory.TwoSquare.guitartExact_op_iff
-- 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
inst_4 : T.IsEquivalence
inst_5 : B.IsEquivalence
inst_6 : IsIso w.natTrans
⊢ w.op.GuitartExact

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GuitartExact.Quotient
Goal:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} H₀
inst_3 : Category.{v_4, u_4} H
T : Functor.{v_1, v_3, u_1, u_3} C₀ H₀
L : Functor.{v_1, v_2, u_1, u_2} C₀ C
R : Functor.{v_3, v_4, u_3, u_4} H₀ H
B : Functor.{v_2, v_4, u_2, u_4} C H
inst_4 : T.EssSurj
inst_5 : T.Full
inst_6 : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ →
      ∃ (P : Precylinder.{v_1, u_1} X₀), T.map P.i₀ = T.map P.i₁ ∧ Nonempty.{v_2 + 1} ((P.map L).LeftHomotopy f₀ f₁)
rw : ∀ {X₂ : H₀} {X₃ : C} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (CostructuredArrowDownwards e.hom g)
⊢ GuitartExact e.hom

Tactic:
rw [guitartExact_iff_isConnected_downwards]

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_isConnected_downwards
-- Module: Mathlib.CategoryTheory.GuitartExact.Quotient
Goal:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} H₀
inst_3 : Category.{v_4, u_4} H
T : Functor.{v_1, v_3, u_1, u_3} C₀ H₀
L : Functor.{v_1, v_2, u_1, u_2} C₀ C
R : Functor.{v_3, v_4, u_3, u_4} H₀ H
B : Functor.{v_2, v_4, u_2, u_4} C H
inst_4 : T.EssSurj
inst_5 : T.Full
inst_6 : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ →
      ∃ (P : Precylinder.{v_1, u_1} X₀), T.map P.i₀ = T.map P.i₁ ∧ Nonempty.{v_2 + 1} ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
X₀ : C₀ := T.objPreimage Y₀
e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
S : Type (max 0 v_2) := { f : L.obj X₀ ⟶ X // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
s : S
⊢ R.map e₀.inv ≫ e.hom.app X₀ ≫ B.map (↑s : L.obj X₀ ⟶ X) = g

Tactic:
simp [s.property]

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.GuitartExact.Quotient
Goal:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} H₀
inst_3 : Category.{v_4, u_4} H
T : Functor.{v_1, v_3, u_1, u_3} C₀ H₀
L : Functor.{v_1, v_2, u_1, u_2} C₀ C
R : Functor.{v_3, v_4, u_3, u_4} H₀ H
B : Functor.{v_2, v_4, u_2, u_4} C H
inst_4 : T.EssSurj
inst_5 : T.Full
inst_6 : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ →
      ∃ (P : Precylinder.{v_1, u_1} X₀), T.map P.i₀ = T.map P.i₁ ∧ Nonempty.{v_2 + 1} ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
X₀ : C₀ := T.objPreimage Y₀
e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
S : Type (max 0 v_2) := { f : L.obj X₀ ⟶ X // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
Z : (s : S) → CostructuredArrowDownwards e.hom g :=
  fun (s : S) ↦ CostructuredArrowDownwards.mk e.hom g X₀ e₀.inv (↑s : L.obj X₀ ⟶ X) ⋯
obtain :
  ∀ (f : L.obj X₀ ⟶ X) (hf : B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g), Nonempty (CostructuredArrowDownwards e.hom g)
⊢ Nonempty (CostructuredArrowDownwards e.hom g)

Tactic:
obtain ⟨f, hf⟩ := B.map_surjective (e.inv.app _ ≫ R.map e₀.hom ≫ g)

Premises used: CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.GuitartExact.Quotient
Goal:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} H₀
inst_3 : Category.{v_4, u_4} H
T : Functor.{v_1, v_3, u_1, u_3} C₀ H₀
L : Functor.{v_1, v_2, u_1, u_2} C₀ C
R : Functor.{v_3, v_4, u_3, u_4} H₀ H
B : Functor.{v_2, v_4, u_2, u_4} C H
inst_4 : T.EssSurj
inst_5 : T.Full
inst_6 : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ →
      ∃ (P : Precylinder.{v_1, u_1} X₀), T.map P.i₀ = T.map P.i₁ ∧ Nonempty.{v_2 + 1} ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
X₀ : C₀ := T.objPreimage Y₀
e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
S : Type (max 0 v_2) := { f : L.obj X₀ ⟶ X // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
Z : (s : S) → CostructuredArrowDownwards e.hom g :=
  fun (s : S) ↦ CostructuredArrowDownwards.mk e.hom g X₀ e₀.inv (↑s : L.obj X₀ ⟶ X) ⋯
f : L.obj X₀ ⟶ X
hf : B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g
⊢ Nonempty (CostructuredArrowDownwards e.hom g)

Tactic:
⟨Z ⟨f, hf⟩⟩

Premises used: Nonempty.intro, Subtype.mk