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_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₁
-- 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 (Z s₁) A₁

Tactic:
.of_hom f₁

Premises used: CategoryTheory.Zigzag.of_hom
-- 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₀ A₁

Tactic:
calc
    Zigzag A₀ (Z s₀) := .of_inv f₀
    Zigzag (Z s₀) Z' := .of_hom <|
      CostructuredArrow.homMk (StructuredArrow.homMk P.i₀) (by simp [Z, Z', dsimp% h.h₀])
    Zigzag Z' (Z s₁) := .of_inv <|
      CostructuredArrow.homMk (StructuredArrow.homMk P.i₁) (by simp [Z, Z', dsimp% h.h₁])
    Zigzag (Z s₁) A₁ := .of_hom f₁

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Zigzag
-- 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₁ : 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₁)
rw : (op e.inv).GuitartExact
⊢ GuitartExact e.inv

Tactic:
rw [← guitartExact_op_iff]

Premises used: CategoryTheory.TwoSquare.guitartExact_op_iff
-- 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₁ : 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

Tactic:
quotient_of_nonempty_leftHomotopy e' (fun X₀ Y f₀ f₁ h ↦ ?_)

Premises used: CategoryTheory.NatTrans.op, CategoryTheory.TwoSquare.op, CategoryTheory.TwoSquare.GuitartExact.quotient_of_nonempty_leftHomotopy
-- 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₁ : 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
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₁)
⊢ (op e.inv).GuitartExact

Tactic:
refine quotient_of_nonempty_leftHomotopy e' (fun X₀ Y f₀ f₁ h ↦ ?_)

Premises used: CategoryTheory.TwoSquare.GuitartExact.quotient_of_nonempty_leftHomotopy
-- 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₁ : 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₁
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₁)
⊢ ∃ (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)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop
-- 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₁ : 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_1 : B.op.map f₀ = B.op.map f₁
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:
⟨P.op, Quiver.Hom.unop_inj hP, ⟨h.op⟩⟩

Premises used: Nonempty.intro, Quiver.Hom.unop_inj, And.intro, HomotopicalAlgebra.PrepathObject.op, Exists.intro, HomotopicalAlgebra.PrepathObject.RightHomotopy.op
-- 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₁ : 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_1 : B.op.map f₀ = B.op.map f₁
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:
exact ⟨P.op, Quiver.Hom.unop_inj hP, ⟨h.op⟩⟩
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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'
rw : ∀ (X₂ : D₁), ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact

Tactic:
rw [guitartExact_iff_initial]

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_initial
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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
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
⊢ (((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

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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
⊢ (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:
simp only [NatTrans.naturality_assoc, assoc, ← B.map_comp,
        Iso.hom_inv_id_app, B.map_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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) ⋯) ⋯
rw : (w.structuredArrowDownwards X₂ ⋙ Equivalence.functor (StructuredArrow.mapIso (β.app X₂))).Initial
⊢ ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial

Tactic:
rw [Functor.initial_natIso_iff e]

Premises used: CategoryTheory.Functor.initial_natIso_iff
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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.structuredArrowDownwards X₂ ⋙ Equivalence.functor (StructuredArrow.mapIso (β.app X₂))).Initial

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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'
mp : (w.whiskerVertical α.hom β.inv).GuitartExact → w.GuitartExact
mpr : w.GuitartExact → (w.whiskerVertical α.hom β.inv).GuitartExact
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact ↔ w.GuitartExact

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
h₁ : ∀ (X₁ : C₁), w.natTrans.app X₁ = ((w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom).natTrans.app X₁
⊢ w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom

Tactic:
ext X₁
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
X₁ : C₁
⊢ w.natTrans.app X₁ = ((w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom).natTrans.app X₁

Tactic:
simp only [Functor.comp_obj, whiskerVertical_app, assoc, Iso.hom_inv_id_app_assoc,
        ← B.map_comp, Iso.hom_inv_id_app, B.map_id, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.TwoSquare.whiskerVertical_app, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
⊢ w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom

Tactic:
have : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom := by
      ext X₁
      simp only [Functor.comp_obj, whiskerVertical_app, assoc, Iso.hom_inv_id_app_assoc,
        ← B.map_comp, Iso.hom_inv_id_app, B.map_id, comp_id]
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
this : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom
mp : ((w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom).GuitartExact
⊢ w.GuitartExact

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
this : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom
⊢ ((w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom).GuitartExact

Tactic:
whiskerVertical (w.whiskerVertical α.hom β.inv) α.symm β.symm

Premises used: CategoryTheory.TwoSquare.whiskerVertical, CategoryTheory.Iso.symm, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.TwoSquare.GuitartExact.whiskerVertical
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
this : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom
⊢ ((w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom).GuitartExact

Tactic:
exact whiskerVertical (w.whiskerVertical α.hom β.inv) α.symm β.symm

Premises used: CategoryTheory.TwoSquare.whiskerVertical, CategoryTheory.Iso.symm, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.TwoSquare.GuitartExact.whiskerVertical
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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'
h : w.GuitartExact
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact

Tactic:
whiskerVertical w α β

Premises used: CategoryTheory.TwoSquare.GuitartExact.whiskerVertical
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
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'
h : w.GuitartExact
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact

Tactic:
exact whiskerVertical w α β

Premises used: CategoryTheory.TwoSquare.GuitartExact.whiskerVertical