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₂ 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 :
  L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom A') =
    StructuredArrow.Hom.right (CostructuredArrow.hom A)
⊢ 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)) ⋯))

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'
h :
  L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom A') =
    StructuredArrow.Hom.right
      ((StructuredArrow.pre (R.obj X₂) L B).map
          (Functor.map (Comma.mapRight (Functor.fromPUnit (R.obj X₂)) w)
            (StructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯)) ≫
        CostructuredArrow.hom A')
⊢ L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom A') =
    StructuredArrow.Hom.right (CostructuredArrow.hom A)

Tactic:
rw [← CostructuredArrow.w φ, structuredArrowDownwards_map]

Premises used: CategoryTheory.CostructuredArrow.w, CategoryTheory.TwoSquare.structuredArrowDownwards_map
-- 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'
⊢ L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom A') =
    StructuredArrow.Hom.right
      ((StructuredArrow.pre (R.obj X₂) L B).map
          (Functor.map (Comma.mapRight (Functor.fromPUnit (R.obj X₂)) w)
            (StructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯)) ≫
        CostructuredArrow.hom A')

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
⊢ w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.StructuredArrowRightwards g)

Tactic:
⟨fun h => h.isConnected_rightwards, fun h => ⟨h⟩⟩

Premises used: CategoryTheory.TwoSquare.GuitartExact.mk, CategoryTheory.TwoSquare.GuitartExact.isConnected_rightwards, Iff.intro
-- 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
⊢ w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g)

Tactic:
simp only [guitartExact_iff_isConnected_rightwards,
    isConnected_rightwards_iff_downwards]

Premises used: CategoryTheory.TwoSquare.isConnected_rightwards_iff_downwards, CategoryTheory.TwoSquare.guitartExact_iff_isConnected_rightwards
-- 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
hw : w.GuitartExact
X₃ : C₃
g : CostructuredArrow R (B.obj X₃)
rw :
  ∀ (hw : ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.StructuredArrowRightwards g)) {X₃ : C₃}
    (g : CostructuredArrow R (B.obj X₃)), IsConnected (StructuredArrow g (w.costructuredArrowRightwards X₃))
⊢ IsConnected (StructuredArrow g (w.costructuredArrowRightwards X₃))

Tactic:
rw [guitartExact_iff_isConnected_rightwards] at hw

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_isConnected_rightwards
-- 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
hw : ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.StructuredArrowRightwards g)
X₃ : C₃
g : CostructuredArrow R (B.obj X₃)
⊢ IsConnected (StructuredArrow g (w.costructuredArrowRightwards X₃))

Tactic:
apply hw
-- 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
hw : w.GuitartExact
X₂ : C₂
g : StructuredArrow (R.obj X₂) B
rw :
  ∀ (hw : ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g)) {X₂ : C₂}
    (g : StructuredArrow (R.obj X₂) B), IsConnected (CostructuredArrow (w.structuredArrowDownwards X₂) g)
⊢ IsConnected (CostructuredArrow (w.structuredArrowDownwards X₂) g)

Tactic:
rw [guitartExact_iff_isConnected_downwards] at hw

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_isConnected_downwards
-- 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
hw : ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g)
X₂ : C₂
g : StructuredArrow (R.obj X₂) B
⊢ IsConnected (CostructuredArrow (w.structuredArrowDownwards X₂) g)

Tactic:
apply hw
-- 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₃
e : X₃ ≅ X₃'
rw :
  (w.costructuredArrowRightwards X₃ ⋙ Equivalence.functor (CostructuredArrow.mapIso (B.mapIso e))).Final ↔
    (Equivalence.functor (CostructuredArrow.mapIso e) ⋙ w.costructuredArrowRightwards X₃').Final
⊢ (w.costructuredArrowRightwards X₃).Final ↔ (w.costructuredArrowRightwards X₃').Final

Tactic:
rw [Functor.final_iff_comp_equivalence _ (CostructuredArrow.mapIso (B.mapIso e)).functor,
    Functor.final_iff_equivalence_comp (CostructuredArrow.mapIso e).functor]

Premises used: CategoryTheory.Functor.final_iff_comp_equivalence, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.final_iff_equivalence_comp, CategoryTheory.CostructuredArrow.mapIso, CategoryTheory.Functor.mapIso
-- 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₃
e : X₃ ≅ X₃'
⊢ (w.costructuredArrowRightwards X₃ ⋙ Equivalence.functor (CostructuredArrow.mapIso (B.mapIso e))).Final ↔
    (Equivalence.functor (CostructuredArrow.mapIso e) ⋙ w.costructuredArrowRightwards X₃').Final

Tactic:
Functor.final_natIso_iff
    (NatIso.ofComponents (fun _ ↦ CostructuredArrow.isoMk (Iso.refl _)))

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.final_natIso_iff, CategoryTheory.CostructuredArrow.isoMk, CategoryTheory.CostructuredArrow.mapIso, CategoryTheory.TwoSquare.costructuredArrowRightwards, CategoryTheory.CostructuredArrow.left, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj, CategoryTheory.NatIso.ofComponents
-- 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₃
e : X₃ ≅ X₃'
⊢ (w.costructuredArrowRightwards X₃ ⋙ Equivalence.functor (CostructuredArrow.mapIso (B.mapIso e))).Final ↔
    (Equivalence.functor (CostructuredArrow.mapIso e) ⋙ w.costructuredArrowRightwards X₃').Final

Tactic:
exact Functor.final_natIso_iff
    (NatIso.ofComponents (fun _ ↦ CostructuredArrow.isoMk (Iso.refl _)))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Functor.final_natIso_iff, CategoryTheory.CostructuredArrow.isoMk, CategoryTheory.CostructuredArrow.left, CategoryTheory.Functor.obj, CategoryTheory.NatIso.ofComponents
-- 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
⊢ w.GuitartExact ↔ ∀ (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final

Tactic:
⟨fun _ _ => ⟨fun _ => inferInstance⟩, fun _ => ⟨fun _ => inferInstance⟩⟩

Premises used: inferInstance, CategoryTheory.TwoSquare.GuitartExact.mk, CategoryTheory.Functor.Final.mk, Iff.intro
-- 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
hw : w.GuitartExact
X₃ : C₃
rw : ∀ (hw : ∀ (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final) (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final
⊢ (w.costructuredArrowRightwards X₃).Final

Tactic:
rw [guitartExact_iff_final] at hw

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_final
-- 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
hw : ∀ (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final
X₃ : C₃
⊢ (w.costructuredArrowRightwards X₃).Final

Tactic:
apply hw
-- 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₂
e : X₂ ≅ X₂'
rw :
  (w.structuredArrowDownwards X₂ ⋙ Equivalence.functor (StructuredArrow.mapIso (R.mapIso e))).Initial ↔
    (Equivalence.functor (StructuredArrow.mapIso e) ⋙ w.structuredArrowDownwards X₂').Initial
⊢ (w.structuredArrowDownwards X₂).Initial ↔ (w.structuredArrowDownwards X₂').Initial

Tactic:
rw [Functor.initial_iff_comp_equivalence _ (StructuredArrow.mapIso (R.mapIso e)).functor,
    Functor.initial_iff_equivalence_comp (StructuredArrow.mapIso e).functor]

Premises used: CategoryTheory.Functor.initial_iff_equivalence_comp, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.initial_iff_comp_equivalence, CategoryTheory.StructuredArrow.mapIso, CategoryTheory.Functor.mapIso
-- 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₂
e : X₂ ≅ X₂'
⊢ (w.structuredArrowDownwards X₂ ⋙ Equivalence.functor (StructuredArrow.mapIso (R.mapIso e))).Initial ↔
    (Equivalence.functor (StructuredArrow.mapIso e) ⋙ w.structuredArrowDownwards X₂').Initial

Tactic:
Functor.initial_natIso_iff
    (NatIso.ofComponents (fun _ ↦ StructuredArrow.isoMk (Iso.refl _)))

Premises used: CategoryTheory.StructuredArrow.isoMk, CategoryTheory.Functor.initial_natIso_iff, CategoryTheory.Functor.comp, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, CategoryTheory.TwoSquare.structuredArrowDownwards, CategoryTheory.StructuredArrow.mapIso, CategoryTheory.StructuredArrow.right, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj, CategoryTheory.NatIso.ofComponents
-- 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₂
e : X₂ ≅ X₂'
⊢ (w.structuredArrowDownwards X₂ ⋙ Equivalence.functor (StructuredArrow.mapIso (R.mapIso e))).Initial ↔
    (Equivalence.functor (StructuredArrow.mapIso e) ⋙ w.structuredArrowDownwards X₂').Initial

Tactic:
exact Functor.initial_natIso_iff
    (NatIso.ofComponents (fun _ ↦ StructuredArrow.isoMk (Iso.refl _)))

Premises used: CategoryTheory.StructuredArrow.isoMk, CategoryTheory.Functor.initial_natIso_iff, CategoryTheory.Iso.refl, CategoryTheory.StructuredArrow.right, CategoryTheory.Functor.obj, CategoryTheory.NatIso.ofComponents
-- 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
rw :
  (∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) →
    ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g)
⊢ (∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) → w.GuitartExact

Tactic:
rw [guitartExact_iff_isConnected_downwards]

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_isConnected_downwards
-- 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
h : ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
⊢ IsConnected (w.CostructuredArrowDownwards g)

Tactic:
infer_instance
-- 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
hw : w.GuitartExact
X₂ : C₂
rw : ∀ (hw : ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
⊢ (w.structuredArrowDownwards X₂).Initial

Tactic:
rw [guitartExact_iff_initial] at hw

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_initial
-- 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
hw : ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
X₂ : C₂
⊢ (w.structuredArrowDownwards X₂).Initial

Tactic:
apply hw
-- 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
inst_4 : L.IsEquivalence
inst_5 : R.IsEquivalence
inst_6 : IsIso w.natTrans
rw : ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
⊢ w.GuitartExact

Tactic:
rw [guitartExact_iff_initial]

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_initial
-- 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
inst_4 : L.IsEquivalence
inst_5 : R.IsEquivalence
inst_6 : IsIso w.natTrans
X₂ : C₂
⊢ (StructuredArrow.post X₂ T R).IsEquivalence

Tactic:
have := StructuredArrow.isEquivalence_post X₂ T R
-- 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
inst_4 : L.IsEquivalence
inst_5 : R.IsEquivalence
inst_6 : IsIso w.natTrans
X₂ : C₂
this : (StructuredArrow.post X₂ T R).IsEquivalence
⊢ Functor.IsEquivalence (C := Comma (Functor.fromPUnit (R.obj X₂)) (T ⋙ R))
    (Comma.mapRight (Functor.fromPUnit (R.obj X₂)) w)

Tactic:
have : (Comma.mapRight _ w : StructuredArrow (R.obj X₂) _ ⥤ _).IsEquivalence :=
    (Comma.mapRightIso _ (asIso w)).isEquivalence_functor
-- 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
inst_4 : L.IsEquivalence
inst_5 : R.IsEquivalence
inst_6 : IsIso w.natTrans
X₂ : C₂
this_1 : (StructuredArrow.post X₂ T R).IsEquivalence
this :
  Functor.IsEquivalence (C := Comma (Functor.fromPUnit (R.obj X₂)) (T ⋙ R))
    (Comma.mapRight (Functor.fromPUnit (R.obj X₂)) w)
⊢ (StructuredArrow.pre (R.obj X₂) L B).IsEquivalence

Tactic:
have := StructuredArrow.isEquivalence_pre (R.obj X₂) L B
-- 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
inst_4 : L.IsEquivalence
inst_5 : R.IsEquivalence
inst_6 : IsIso w.natTrans
X₂ : C₂
this_1 : (StructuredArrow.post X₂ T R).IsEquivalence
this_2 :
  Functor.IsEquivalence (C := Comma (Functor.fromPUnit (R.obj X₂)) (T ⋙ R))
    (Comma.mapRight (Functor.fromPUnit (R.obj X₂)) w)
this : (StructuredArrow.pre (R.obj X₂) L B).IsEquivalence
⊢ (StructuredArrow.post X₂ T R ⋙
      Comma.mapRight (Functor.fromPUnit (R.obj X₂)) w ⋙ StructuredArrow.pre (R.obj X₂) L B).Initial

Tactic:
infer_instance
-- 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₂
rw :
  ∀ {X₂ : C₁} {X₃ : C₂} (g : F.obj X₂ ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 C₂) X₃),
    IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) g)
⊢ GuitartExact (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F))

Tactic:
rw [guitartExact_iff_isConnected_rightwards]

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_isConnected_rightwards
-- 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₂
X₄ :
  ∀ (g : F.obj X₂ ⟶ X₃),
    IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g)
⊢ ∀ (g : F.obj X₂ ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 C₂) X₃),
    IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) g)

Tactic:
(g : F.obj X₂ ⟶ X₃)