awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
a : X₂ ⟶ T.obj X₁
φ : (w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a) ⟶ StructuredArrow.mk g
⊢ ∃ (X₁_1 : C₁) (a_1 : X₂ ⟶ T.obj X₁_1) (b : L.obj X₁_1 ⟶ X₃) (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b = g),
    CostructuredArrow.mk φ = mk w g X₁_1 a_1 b comm
have obtain : ∀ (b : ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).right ⟶ (StructuredArrow.mk g).right)
  (hb : ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).hom ≫ B.map b = (StructuredArrow.mk g).hom),
  ∃ (X₁_1 : C₁) (a_1 : X₂ ⟶ T.obj X₁_1) (b_1 : L.obj X₁_1 ⟶ X₃) (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b_1 = g),
    CostructuredArrow.mk (StructuredArrow.homMk b hb) = mk w g X₁_1 a_1 b_1 comm
Tactic: obtain ⟨b, hb, rfl⟩ := StructuredArrow.homMk_surjective φ
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
⊢ 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 ⋯)))
have dsimp : (StructuredArrow.hom f₁).left ≫ T.map (StructuredArrow.Hom.right φ).left = (StructuredArrow.hom f₂).left
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : 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₂).left
have rw : (StructuredArrow.hom f₁).left ≫ T.map (StructuredArrow.Hom.right φ).left =
  (StructuredArrow.hom f₁ ≫ (w.costructuredArrowRightwards X₃).map (StructuredArrow.Hom.right φ)).left
Tactic: rw [← StructuredArrow.w φ]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : 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 ⋯))) ⟶
      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 ⋯)))
have 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 sorry)))).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 sorry))))
      ((w.structuredArrowDownwards X₂).map (StructuredArrow.homMk (StructuredArrow.Hom.right φ).left sorry))
      (CostructuredArrow.hom
        (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₂).left)
          (StructuredArrow.homMk (StructuredArrow.right f₂).hom sorry)))))
  (StructuredArrow.Hom.right
    (CostructuredArrow.hom
      (CostructuredArrow.mk (Y := StructuredArrow.mk (StructuredArrow.hom f₁).left)
        (StructuredArrow.homMk (StructuredArrow.right f₁).hom sorry))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ 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 ⋯))))
have dsimp : L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom f₂) =
  StructuredArrow.Hom.right (CostructuredArrow.hom f₁)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : 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 (CostructuredArrow.hom f₁)
have rw : L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom f₂) =
  StructuredArrow.Hom.right ((w.structuredArrowDownwards X₂).map φ.left ≫ CostructuredArrow.hom f₂)
Tactic: rw [← CostructuredArrow.w φ]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ 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'
⊢ (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
have dsimp : (γ ≫ (CostructuredArrow.left A).hom) ≫ T.map (StructuredArrow.Hom.right φ.left) = γ ≫ (CostructuredArrow.left A').hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ 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'
⊢ (γ ≫ (CostructuredArrow.left A).hom) ≫ T.map (StructuredArrow.Hom.right φ.left) = γ ≫ (CostructuredArrow.left A').hom
have rw : γ ≫ (CostructuredArrow.left A).hom ≫ T.map (StructuredArrow.Hom.right φ.left) = γ ≫ (CostructuredArrow.left A').hom
Tactic: rw [assoc, StructuredArrow.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ 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
⊢ (γ ≫ (CostructuredArrow.left A).hom) ≫ T.map (StructuredArrow.Hom.right φ.left) = γ ≫ (CostructuredArrow.left A').hom
have rw₁ : γ ≫ A'.left.hom = γ ≫ (CostructuredArrow.left A').hom
Tactic: rw [assoc, StructuredArrow.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ 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'
⊢ (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)) ⋯)
have h : StructuredArrow.Hom.right
    ((w.structuredArrowDownwards X₂').map (StructuredArrow.homMk (StructuredArrow.Hom.right φ.left) sorry) ≫
      CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A').right (γ ≫ (CostructuredArrow.left A').hom)
          (StructuredArrow.Hom.right (CostructuredArrow.hom A')) sorry)) =
  StructuredArrow.Hom.right
    (CostructuredArrow.hom
      (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A).right (γ ≫ (CostructuredArrow.left A).hom)
        (StructuredArrow.Hom.right (CostructuredArrow.hom A)) sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ 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'
⊢ 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)) ⋯))
have h : L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom A') =
  StructuredArrow.Hom.right (CostructuredArrow.hom A)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ 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 (CostructuredArrow.hom A)
have 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) sorry)) ≫
      CostructuredArrow.hom A')
Tactic: rw [← CostructuredArrow.w φ, structuredArrowDownwards_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
hw : w.GuitartExact
X₃ : C₃
g : CostructuredArrow R (B.obj X₃)
⊢ IsConnected (StructuredArrow g (w.costructuredArrowRightwards X₃))
have 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₃))
Tactic: rw [guitartExact_iff_isConnected_rightwards] at hw
Cleared hypotheses: hw, X₃, g
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
hw : w.GuitartExact
X₂ : C₂
g : StructuredArrow (R.obj X₂) B
⊢ IsConnected (CostructuredArrow (w.structuredArrowDownwards X₂) g)
have 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)
Tactic: rw [guitartExact_iff_isConnected_downwards] at hw
Cleared hypotheses: hw, X₂, g
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₃ X₃' : C₃
e : X₃ ≅ X₃'
⊢ (w.costructuredArrowRightwards X₃).Final ↔ (w.costructuredArrowRightwards X₃').Final
have rw : (w.costructuredArrowRightwards X₃ ⋙ Equivalence.functor (CostructuredArrow.mapIso (B.mapIso e))).Final ↔
  (Equivalence.functor (CostructuredArrow.mapIso e) ⋙ 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
hw : w.GuitartExact
X₃ : C₃
⊢ (w.costructuredArrowRightwards X₃).Final
have rw : ∀ (hw : ∀ (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final) (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final
Tactic: rw [guitartExact_iff_final] at hw
Cleared hypotheses: hw, X₃
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ X₂' : C₂
e : X₂ ≅ X₂'
⊢ (w.structuredArrowDownwards X₂).Initial ↔ (w.structuredArrowDownwards X₂').Initial
have rw : (w.structuredArrowDownwards X₂ ⋙ Equivalence.functor (StructuredArrow.mapIso (R.mapIso e))).Initial ↔
  (Equivalence.functor (StructuredArrow.mapIso e) ⋙ 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
⊢ (∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) → w.GuitartExact
have rw : (∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) →
  ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g)
Tactic: rw [guitartExact_iff_isConnected_downwards]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
hw : w.GuitartExact
X₂ : C₂
⊢ (w.structuredArrowDownwards X₂).Initial
have rw : ∀ (hw : ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
Tactic: rw [guitartExact_iff_initial] at hw
Cleared hypotheses: hw, X₂
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_4 : L.IsEquivalence
inst_5 : R.IsEquivalence
inst_6 : IsIso w.natTrans
⊢ w.GuitartExact
have rw : ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
Tactic: rw [guitartExact_iff_initial]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (hypothesis)
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₂
⊢ (w.structuredArrowDownwards X₂).Initial
have this : (StructuredArrow.post X₂ T R).IsEquivalence
Tactic: have := StructuredArrow.isEquivalence_post X₂ T R
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (hypothesis)
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
⊢ (w.structuredArrowDownwards X₂).Initial
have this₁ : 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