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

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

Tactic:
zigzag_isConnected (fun A₀ A₁ ↦ ?_)

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

Tactic:
refine zigzag_isConnected (fun A₀ A₁ ↦ ?_)

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

Tactic:
obtain ⟨a, ha⟩ := T.map_surjective (e₀.hom ≫ A.left.hom)

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

Tactic:
⟨⟨L.map a ≫ A.hom.right, ?_⟩,
      ⟨CostructuredArrow.homMk (StructuredArrow.homMk a ?_)⟩⟩

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

Tactic:
refine ⟨⟨L.map a ≫ A.hom.right, ?_⟩,
      ⟨CostructuredArrow.homMk (StructuredArrow.homMk a ?_)⟩⟩
-- Module: Mathlib.CategoryTheory.GuitartExact.Quotient
Goal:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} H₀
inst_3 : Category.{v_4, u_4} H
T : Functor.{v_1, v_3, u_1, u_3} C₀ H₀
L : Functor.{v_1, v_2, u_1, u_2} C₀ C
R : Functor.{v_3, v_4, u_3, u_4} H₀ H
B : Functor.{v_2, v_4, u_2, u_4} C H
inst_4 : T.EssSurj
inst_5 : T.Full
inst_6 : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ →
      ∃ (P : Precylinder.{v_1, u_1} X₀), T.map P.i₀ = T.map P.i₁ ∧ Nonempty.{v_2 + 1} ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
X₀ : C₀ := T.objPreimage Y₀
e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
S : Type (max 0 v_2) := { f : L.obj X₀ ⟶ X // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
Z : (s : S) → CostructuredArrowDownwards e.hom g :=
  fun (s : S) ↦ CostructuredArrowDownwards.mk e.hom g X₀ e₀.inv (↑s : L.obj X₀ ⟶ X) ⋯
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
⊢ B.map (L.map a ≫ StructuredArrow.Hom.right (CostructuredArrow.hom A)) = e.inv.app X₀ ≫ R.map e₀.hom ≫ g

Tactic:
simp [← dsimp% NatIso.naturality_1 e a, ha, dsimp% A.hom.w]

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

Tactic:
obtain ⟨s₀, ⟨f₀⟩⟩ := H A₀
-- Module: Mathlib.CategoryTheory.GuitartExact.Quotient
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₀
obtain : ∀ (s₁ : S) (f₁ : Z s₁ ⟶ A₁), Zigzag A₀ A₁
⊢ Zigzag A₀ A₁

Tactic:
obtain ⟨s₁, ⟨f₁⟩⟩ := H A₁
-- Module: Mathlib.CategoryTheory.GuitartExact.Quotient
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₁
⊢ B.map (↑s₀ : L.obj X₀ ⟶ X) = B.map (↑s₁ : L.obj X₀ ⟶ X)

Tactic:
simp [s₀.property, s₁.property]

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.GuitartExact.Quotient
Goal:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H_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₁
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₁
⊢ Zigzag A₀ A₁

Tactic:
obtain ⟨P, hP, ⟨h⟩⟩ := he s₀.val s₁.val (by simp [s₀.property, s₁.property])

Premises used: Subtype.val
-- Module: Mathlib.CategoryTheory.GuitartExact.Quotient
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₁
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)
⊢ R.map (e₀.inv ≫ T.map P.i₀) ≫ e.hom.app P.I ≫ B.map h.h = g

Tactic:
simp [R.map_comp, ← B.map_comp, dsimp% h.h₀, s₀.property,
        dsimp% e.hom.naturality_assoc P.i₀]

Premises used: HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.naturality_assoc, Subtype.property, HomotopicalAlgebra.Precylinder.i₀
-- Module: Mathlib.CategoryTheory.GuitartExact.Quotient
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₁
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)
Z' : CostructuredArrowDownwards e.hom g := CostructuredArrowDownwards.mk e.hom g P.I (e₀.inv ≫ T.map P.i₀) h.h ⋯
⊢ Zigzag A₀ (Z s₀)

Tactic:
.of_inv f₀

Premises used: CategoryTheory.Zigzag.of_inv
-- Module: Mathlib.CategoryTheory.GuitartExact.Quotient
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₁
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)
Z' : CostructuredArrowDownwards e.hom g := CostructuredArrowDownwards.mk e.hom g P.I (e₀.inv ≫ T.map P.i₀) h.h ⋯
⊢ (structuredArrowDownwards e.hom Y₀).map (StructuredArrow.homMk P.i₀ ⋯) ≫ CostructuredArrow.hom Z' =
    CostructuredArrow.hom (Z s₀)

Tactic:
simp [Z, Z', dsimp% h.h₀]

Premises used: HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀