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
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) :=
  StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
X : Z
⊢ F.map (StructuredArrow.hom X).left ≫ (StructuredArrow.right X).hom = (StructuredArrow.right X₀).hom

Tactic:
simpa using CostructuredArrow.w X.hom

Premises used: CategoryTheory.StructuredArrow.hom, 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
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) :=
  StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
have :
  ∀ (φ : (X : Z) → X₀ ⟶ X),
    IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g)
⊢ IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g)

Tactic:
have φ : ∀ (X : Z), X₀ ⟶ X := fun X =>
    StructuredArrow.homMk (CostructuredArrow.homMk X.hom.left
      (by simpa using CostructuredArrow.w X.hom))
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) :=
  StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
φ : (X : Z) → X₀ ⟶ X
⊢ Nonempty Z

Tactic:
have : Nonempty Z := ⟨X₀⟩
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) :=
  StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
φ : (X : Z) → X₀ ⟶ X
this : Nonempty Z
h :
  ∀ (j₁ j₂ : StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g),
    Zigzag j₁ j₂
⊢ IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g)

Tactic:
apply zigzag_isConnected

Premises used: CategoryTheory.zigzag_isConnected
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) :=
  StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
φ : (X : Z) → X₀ ⟶ X
this : Nonempty Z
X Y : StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g
⊢ Zigzag X Y

Tactic:
Zigzag.of_inv_hom (φ X) (φ Y)

Premises used: CategoryTheory.Zigzag.of_inv_hom
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) :=
  StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
φ : (X : Z) → X₀ ⟶ X
this : Nonempty Z
X Y : StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g
⊢ Zigzag X Y

Tactic:
exact Zigzag.of_inv_hom (φ X) (φ Y)

Premises used: CategoryTheory.Zigzag.of_inv_hom
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} D₂
T : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
B : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T L R B
T' : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
B' : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
inst_4 : w.GuitartExact
α : T ≅ T'
β : B ≅ B'
rw : ∀ (X₃ : C₂), ((w.whiskerHorizontal α.inv β.hom).costructuredArrowRightwards X₃).Final
⊢ (w.whiskerHorizontal α.inv β.hom).GuitartExact

Tactic:
rw [guitartExact_iff_final]

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_final
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} D₂
T : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
B : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T L R B
T' : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
B' : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
inst_4 : w.GuitartExact
α : T ≅ T'
β : B ≅ B'
X₂ : C₂
e : (w.whiskerHorizontal α.inv β.hom).costructuredArrowRightwards X₂ ≅
  w.costructuredArrowRightwards X₂ ⋙ Equivalence.functor (CostructuredArrow.mapIso (β.app X₂)) :=
  NatIso.ofComponents (fun (f : CostructuredArrow L X₂) ↦ CostructuredArrow.isoMk (α.symm.app f.left) ⋯) ⋯
rw : (w.costructuredArrowRightwards X₂ ⋙ Equivalence.functor (CostructuredArrow.mapIso (β.app X₂))).Final
⊢ ((w.whiskerHorizontal α.inv β.hom).costructuredArrowRightwards X₂).Final

Tactic:
rw [Functor.final_natIso_iff e]

Premises used: CategoryTheory.Functor.final_natIso_iff
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} D₂
T : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
B : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T L R B
T' : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
B' : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
inst_4 : w.GuitartExact
α : T ≅ T'
β : B ≅ B'
X₂ : C₂
e : (w.whiskerHorizontal α.inv β.hom).costructuredArrowRightwards X₂ ≅
  w.costructuredArrowRightwards X₂ ⋙ Equivalence.functor (CostructuredArrow.mapIso (β.app X₂)) :=
  NatIso.ofComponents (fun (f : CostructuredArrow L X₂) ↦ CostructuredArrow.isoMk (α.symm.app f.left) ⋯) ⋯
⊢ (w.costructuredArrowRightwards X₂ ⋙ Equivalence.functor (CostructuredArrow.mapIso (β.app X₂))).Final

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} D₂
T : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
B : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T L R B
T' : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
B' : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
α : T ≅ T'
β : B ≅ B'
rw :
  (w.whiskerHorizontal α.inv β.hom).op.GuitartExact ↔
    (w.op.whiskerVertical (NatIso.op α.symm).hom (NatIso.op β.symm).inv).GuitartExact
⊢ (w.whiskerHorizontal α.inv β.hom).GuitartExact ↔ w.GuitartExact

Tactic:
rw [← guitartExact_op_iff, ← w.guitartExact_op_iff,
    ← whiskerVertical_iff w.op (NatIso.op α.symm) (NatIso.op β.symm)]

Premises used: CategoryTheory.TwoSquare.GuitartExact.whiskerVertical_iff, CategoryTheory.TwoSquare.guitartExact_op_iff, CategoryTheory.Iso.symm, CategoryTheory.NatIso.op, CategoryTheory.TwoSquare.op
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} D₂
T : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
B : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T L R B
T' : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
B' : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
α : T ≅ T'
β : B ≅ B'
⊢ (w.whiskerHorizontal α.inv β.hom).op.GuitartExact ↔
    (w.op.whiskerVertical (NatIso.op α.symm).hom (NatIso.op β.symm).inv).GuitartExact

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
T : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
B : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T L R B
T' : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
B' : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
inst_6 : w.GuitartExact
α : T' ⟶ T
β : B ⟶ B'
inst_7 : IsIso α
inst_8 : IsIso β
⊢ (w.whiskerHorizontal α β).GuitartExact

Tactic:
whiskerHorizontal w (asIso α).symm (asIso β)

Premises used: CategoryTheory.Iso.symm, CategoryTheory.asIso, CategoryTheory.TwoSquare.GuitartExact.whiskerHorizontal
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : w.GuitartExact
inst_7 : w'.GuitartExact
rw : (w ≫ₕ w').op.GuitartExact
⊢ (w ≫ₕ w').GuitartExact

Tactic:
rw [← guitartExact_op_iff]

Premises used: CategoryTheory.TwoSquare.guitartExact_op_iff
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : w.GuitartExact
inst_7 : w'.GuitartExact
h : ∀ (X : C₁ᵒᵖ), (w ≫ₕ w').op.natTrans.app X = (w.op ≫ᵥ w'.op).natTrans.app X
⊢ (w ≫ₕ w').op = w.op ≫ᵥ w'.op

Tactic:
ext
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : w.GuitartExact
inst_7 : w'.GuitartExact
X : C₁ᵒᵖ
⊢ (w ≫ₕ w').op.natTrans.app X = (w.op ≫ᵥ w'.op).natTrans.app X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : w.GuitartExact
inst_7 : w'.GuitartExact
⊢ (w ≫ₕ w').op = w.op ≫ᵥ w'.op

Tactic:
have : (w ≫ₕ w').op = w.op ≫ᵥ w'.op := by ext; simp
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : w.GuitartExact
inst_7 : w'.GuitartExact
this : (w ≫ₕ w').op = w.op ≫ᵥ w'.op
rw : (w.op ≫ᵥ w'.op).GuitartExact
⊢ (w ≫ₕ w').op.GuitartExact

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : w.GuitartExact
inst_7 : w'.GuitartExact
this : (w ≫ₕ w').op = w.op ≫ᵥ w'.op
⊢ (w.op ≫ᵥ w'.op).GuitartExact

Tactic:
inferInstanceAs (w.op ≫ᵥ w'.op).GuitartExact

Premises used: _private.0.CategoryTheory.TwoSquare.GuitartExact.hComp._proof_1
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : w.GuitartExact
inst_7 : w'.GuitartExact
this : (w ≫ₕ w').op = w.op ≫ᵥ w'.op
⊢ (w.op ≫ᵥ w'.op).GuitartExact

Tactic:
exact inferInstanceAs (w.op ≫ᵥ w'.op).GuitartExact
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
T₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
B₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eT : T₁ ⋙ T₂ ≅ T₁₂
eB : B₁ ⋙ B₂ ≅ B₁₂
inst_6 : w.GuitartExact
inst_7 : w'.GuitartExact
⊢ ((w ≫ₕ w').whiskerHorizontal eT.inv eB.hom).GuitartExact

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : B₁.EssSurj
inst_7 : w.GuitartExact
inst_8 : (w ≫ₕ w').GuitartExact
rw : ∀ (X₃ : D₂), (w'.costructuredArrowRightwards X₃).Final
⊢ w'.GuitartExact

Tactic:
rw [guitartExact_iff_final]

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_final
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : B₁.EssSurj
inst_7 : w.GuitartExact
inst_8 : (w ≫ₕ w').GuitartExact
Y₂ : D₂
rw :
  Functor.Final (C := CostructuredArrow V₂ (B₁.obj (B₁.objPreimage Y₂)))
    (w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂)))
⊢ (w'.costructuredArrowRightwards Y₂).Final

Tactic:
rw [costructuredArrowRightwards_final_iff_of_iso _ (B₁.objObjPreimageIso Y₂).symm]

Premises used: CategoryTheory.TwoSquare.costructuredArrowRightwards_final_iff_of_iso, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : B₁.EssSurj
inst_7 : w.GuitartExact
inst_8 : (w ≫ₕ w').GuitartExact
Y₂ : D₂
⊢ Functor.Final (C := CostructuredArrow V₁ (B₁.objPreimage Y₂))
    (w.costructuredArrowRightwards (B₁.objPreimage Y₂) ⋙ w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂)))

Tactic:
have : (w.costructuredArrowRightwards (B₁.objPreimage Y₂) ⋙
      w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂))).Final :=
    (Functor.final_of_natIso (costructuredArrowRightwardsComp w w' _).symm :)
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : B₁.EssSurj
inst_7 : w.GuitartExact
inst_8 : (w ≫ₕ w').GuitartExact
Y₂ : D₂
this :
  Functor.Final (C := CostructuredArrow V₁ (B₁.objPreimage Y₂))
    (w.costructuredArrowRightwards (B₁.objPreimage Y₂) ⋙ w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂)))
⊢ Functor.Final (C := CostructuredArrow V₂ (B₁.obj (B₁.objPreimage Y₂)))
    (w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂)))

Tactic:
Functor.final_of_final_comp (w.costructuredArrowRightwards (B₁.objPreimage Y₂)) _

Premises used: CategoryTheory.Functor.final_of_final_comp, CategoryTheory.Functor.objPreimage, CategoryTheory.TwoSquare.costructuredArrowRightwards
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : B₁.EssSurj
inst_7 : w.GuitartExact
inst_8 : (w ≫ₕ w').GuitartExact
Y₂ : D₂
this :
  Functor.Final (C := CostructuredArrow V₁ (B₁.objPreimage Y₂))
    (w.costructuredArrowRightwards (B₁.objPreimage Y₂) ⋙ w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂)))
⊢ Functor.Final (C := CostructuredArrow V₂ (B₁.obj (B₁.objPreimage Y₂)))
    (w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂)))

Tactic:
exact Functor.final_of_final_comp (w.costructuredArrowRightwards (B₁.objPreimage Y₂)) _

Premises used: CategoryTheory.Functor.final_of_final_comp, CategoryTheory.Functor.objPreimage, CategoryTheory.TwoSquare.costructuredArrowRightwards