awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Opposite (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
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.GuitartExact
have this : w = (w₁ ≫ᵥ w.op.op) ≫ᵥ w₂
Tactic: have : w = (w₁ ≫ᵥ w.op.op) ≫ᵥ w₂ := by cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Opposite (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
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.GuitartExact
have mp : ((w₁ ≫ᵥ w.op.op) ≫ᵥ w₂).GuitartExact
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Opposite (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
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
⊢ (mk F (𝟭 C₁) (𝟭 C₂) F (𝟙 F)).GuitartExact
have rw : (mk F (𝟭 C₁) (𝟭 C₂) F (𝟙 F)).op.GuitartExact
Tactic: rw [← guitartExact_op_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Opposite (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 : T.IsEquivalence
inst_5 : B.IsEquivalence
inst_6 : IsIso w.natTrans
⊢ w.GuitartExact
have rw : w.op.GuitartExact
Tactic: rw [← guitartExact_op_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
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₁)
⊢ GuitartExact e.hom
have rw : ∀ {X₂ : H₀} {X₃ : C} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (CostructuredArrowDownwards e.hom g)
Tactic: rw [guitartExact_iff_isConnected_downwards]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
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) ⋯
⊢ Nonempty (CostructuredArrowDownwards e.hom g)
have obtain : ∀ (f : L.obj X₀ ⟶ X) (hf : B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g), Nonempty (CostructuredArrowDownwards e.hom g)
Tactic: obtain ⟨f, hf⟩ := B.map_surjective (e.inv.app _ ≫ R.map e₀.hom ≫ g)
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (hypothesis)
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) ⋯
⊢ IsConnected (CostructuredArrowDownwards e.hom g)
have this : Nonempty (CostructuredArrowDownwards e.hom g)
Tactic: have : Nonempty (CostructuredArrowDownwards e.hom g) := by
    obtain ⟨f, hf⟩ := B.map_surjective (e.inv.app _ ≫ R.map e₀.hom ≫ g)
    exact ⟨Z ⟨f, hf⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
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) ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
⊢ IsConnected (CostructuredArrowDownwards e.hom g)
have refine : ∀ (A₀ A₁ : CostructuredArrowDownwards e.hom g), Zigzag A₀ A₁
Tactic: refine zigzag_isConnected (fun A₀ A₁ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
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) ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ A : CostructuredArrowDownwards e.hom g
⊢ ∃ (s : S), Nonempty.{v_1 + 1} (Z s ⟶ A)
have obtain : ∀ (a : X₀ ⟶ (CostructuredArrow.left A).right) (ha : T.map a = e₀.hom ≫ (CostructuredArrow.left A).hom),
  ∃ (s : S), Nonempty.{v_1 + 1} (Z s ⟶ A)
Tactic: obtain ⟨a, ha⟩ := T.map_surjective (e₀.hom ≫ A.left.hom)
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
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) ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ A : CostructuredArrowDownwards e.hom g
a : X₀ ⟶ (CostructuredArrow.left A).right
ha : T.map a = e₀.hom ≫ (CostructuredArrow.left A).hom
⊢ ∃ (s : S), Nonempty.{v_1 + 1} (Z s ⟶ A)
have refine_1 : B.map (L.map a ≫ StructuredArrow.Hom.right (CostructuredArrow.hom A)) = e.inv.app X₀ ≫ R.map e₀.hom ≫ g
Tactic: refine ⟨⟨L.map a ≫ A.hom.right, ?_⟩,
      ⟨CostructuredArrow.homMk (StructuredArrow.homMk a ?_)⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
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) ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ A : CostructuredArrowDownwards e.hom g
a : X₀ ⟶ (CostructuredArrow.left A).right
ha : T.map a = e₀.hom ≫ (CostructuredArrow.left A).hom
refine_1 : B.map (L.map a ≫ StructuredArrow.Hom.right (CostructuredArrow.hom A)) = e.inv.app X₀ ≫ R.map e₀.hom ≫ g
⊢ ∃ (s : S), Nonempty.{v_1 + 1} (Z s ⟶ A)
have refine_2 : (CostructuredArrow.left
        (Z
          (Subtype.mk (p := fun (f : L.obj X₀ ⟶ X) ↦ B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g)
            (L.map a ≫ StructuredArrow.Hom.right (CostructuredArrow.hom A)) sorry))).hom ≫
    T.map a =
  (CostructuredArrow.left A).hom
Tactic: refine ⟨⟨L.map a ≫ A.hom.right, ?_⟩,
      ⟨CostructuredArrow.homMk (StructuredArrow.homMk a ?_)⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (hypothesis)
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) ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ : CostructuredArrowDownwards e.hom g
⊢ Zigzag A₀ A₁
have H₁ : ∀ (A : CostructuredArrowDownwards e.hom g), ∃ (s : S), Nonempty.{v_1 + 1} (Z s ⟶ A)
Tactic: have H (A : CostructuredArrowDownwards e.hom g) : ∃ s, Nonempty (Z s ⟶ A) := by
    obtain ⟨a, ha⟩ := T.map_surjective (e₀.hom ≫ A.left.hom)
    refine ⟨⟨L.map a ≫ A.hom.right, ?_⟩,
      ⟨CostructuredArrow.homMk (StructuredArrow.homMk a ?_)⟩⟩
    · simp [← dsimp% NatIso.naturality_1 e a, ha, dsimp% A.hom.w]
    · cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
Goal:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H_1 : 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_1
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_1
B : Functor.{v_2, v_4, u_2, u_4} C H_1
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) ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ : CostructuredArrowDownwards e.hom g
H : ∀ (A : CostructuredArrowDownwards e.hom g), ∃ (s : S), Nonempty.{v_1 + 1} (Z s ⟶ A)
⊢ Zigzag A₀ A₁
have obtain : ∀ (s₀ : S) (f₀ : Z s₀ ⟶ A₀), Zigzag A₀ A₁
Tactic: obtain ⟨s₀, ⟨f₀⟩⟩ := H A₀
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
Goal:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H_1 : 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_1
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_1
B : Functor.{v_2, v_4, u_2, u_4} C H_1
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) ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ : CostructuredArrowDownwards e.hom g
H : ∀ (A : CostructuredArrowDownwards e.hom g), ∃ (s : S), Nonempty.{v_1 + 1} (Z s ⟶ A)
s₀ : S
f₀ : Z s₀ ⟶ A₀
⊢ Zigzag A₀ A₁
have obtain : ∀ (s₁ : S) (f₁ : Z s₁ ⟶ A₁), Zigzag A₀ A₁
Tactic: obtain ⟨s₁, ⟨f₁⟩⟩ := H A₁
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
Goal:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H_1 : 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_1
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_1
B : Functor.{v_2, v_4, u_2, u_4} C H_1
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) ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ : CostructuredArrowDownwards e.hom g
H : ∀ (A : CostructuredArrowDownwards e.hom g), ∃ (s : S), Nonempty.{v_1 + 1} (Z s ⟶ A)
s₀ : S
f₀ : Z s₀ ⟶ A₀
s₁ : S
f₁ : Z s₁ ⟶ A₁
⊢ Zigzag A₀ A₁
have obtain : ∀ (P : Precylinder.{v_1, u_1} X₀) (hP : T.map P.i₀ = T.map P.i₁)
  (h : (P.map L).LeftHomotopy (↑s₀ : L.obj X₀ ⟶ X) (↑s₁ : L.obj X₀ ⟶ X)), Zigzag A₀ A₁
Tactic: obtain ⟨P, hP, ⟨h⟩⟩ := he s₀.val s₁.val (by simp [s₀.property, s₁.property])
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
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₁ : X ⟶ L.obj Y₀),
    B.map f₀ = B.map f₁ →
      ∃ (P : PrepathObject.{v_1, u_1} Y₀), T.map P.p₀ = T.map P.p₁ ∧ Nonempty.{v_2 + 1} ((P.map L).RightHomotopy f₀ f₁)
⊢ GuitartExact e.inv
have rw : (op e.inv).GuitartExact
Tactic: rw [← guitartExact_op_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
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₁ : X ⟶ L.obj Y₀),
    B.map f₀ = B.map f₁ →
      ∃ (P : PrepathObject.{v_1, u_1} Y₀), T.map P.p₀ = T.map P.p₁ ∧ Nonempty.{v_2 + 1} ((P.map L).RightHomotopy f₀ f₁)
e' : T.op ⋙ R.op ≅ L.op ⋙ B.op := NatIso.op e.symm
⊢ (op e.inv).GuitartExact
have refine : ∀ (X₀ : C₀ᵒᵖ) (Y : Cᵒᵖ) (f₀ f₁ : L.op.obj X₀ ⟶ Y) (h : B.op.map f₀ = B.op.map f₁),
  ∃ (P : Precylinder.{v_1, u_1} X₀),
    T.op.map P.i₀ = T.op.map P.i₁ ∧ Nonempty.{v_2 + 1} ((P.map L.op).LeftHomotopy f₀ f₁)
Tactic: refine quotient_of_nonempty_leftHomotopy e' (fun X₀ Y f₀ f₁ h ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Quotient (goal)
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₁ : X ⟶ L.obj Y₀),
    B.map f₀ = B.map f₁ →
      ∃ (P : PrepathObject.{v_1, u_1} Y₀), T.map P.p₀ = T.map P.p₁ ∧ Nonempty.{v_2 + 1} ((P.map L).RightHomotopy f₀ f₁)
e' : T.op ⋙ R.op ≅ L.op ⋙ B.op := NatIso.op e.symm
X₀ : C₀ᵒᵖ
Y : Cᵒᵖ
f₀ f₁ : L.op.obj X₀ ⟶ Y
h : B.op.map f₀ = B.op.map f₁
⊢ ∃ (P : Precylinder.{v_1, u_1} X₀),
    T.op.map P.i₀ = T.op.map P.i₁ ∧ Nonempty.{v_2 + 1} ((P.map L.op).LeftHomotopy f₀ f₁)
have obtain : ∀ (P : PrepathObject.{v_1, u_1} (unop X₀)) (hP : T.map P.p₀ = T.map P.p₁) (h : (P.map L).RightHomotopy f₀.unop f₁.unop),
  ∃ (P : Precylinder.{v_1, u_1} X₀),
    T.op.map P.i₀ = T.op.map P.i₁ ∧ Nonempty.{v_2 + 1} ((P.map L.op).LeftHomotopy f₀ f₁)
Tactic: obtain ⟨P, hP, ⟨h⟩⟩ := he f₀.unop f₁.unop (Quiver.Hom.op_inj h)
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.VerticalComposition (goal)
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
L' : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R' : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
inst_4 : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact
have rw : ∀ (X₂ : D₁), ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial
Tactic: rw [guitartExact_iff_initial]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.VerticalComposition (goal)
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
L' : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R' : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
inst_4 : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
f : StructuredArrow X₂ T
⊢ (((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).obj f).hom ≫ B.map (Iso.hom (α.symm.app f.right)) =
    ((w.structuredArrowDownwards X₂ ⋙ Equivalence.functor (StructuredArrow.mapIso (β.app X₂))).obj f).hom
have dsimp : (R'.map f.hom ≫ β.inv.app (T.obj f.right) ≫ w.natTrans.app f.right ≫ B.map (α.hom.app f.right)) ≫
    B.map (α.inv.app f.right) =
  β.inv.app X₂ ≫ R.map f.hom ≫ w.app f.right
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.VerticalComposition (goal)
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
L' : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R' : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
inst_4 : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
e : (w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂ ≅
  w.structuredArrowDownwards X₂ ⋙ Equivalence.functor (StructuredArrow.mapIso (β.app X₂)) :=
  NatIso.ofComponents (fun (f : StructuredArrow X₂ T) ↦ StructuredArrow.isoMk (α.symm.app f.right) ⋯) ⋯
⊢ ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial
have rw : (w.structuredArrowDownwards X₂ ⋙ Equivalence.functor (StructuredArrow.mapIso (β.app X₂))).Initial
Tactic: rw [Functor.initial_natIso_iff e]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.VerticalComposition (goal)
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
L' : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R' : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact ↔ w.GuitartExact
have mp : (w.whiskerVertical α.hom β.inv).GuitartExact → w.GuitartExact
Tactic: constructor