-- Mathlib/CategoryTheory/GuitartExact/Basic.lean
lemma StructuredArrowRightwards.mk_surjective
    (f : w.StructuredArrowRightwards g) :
    ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃)
      (comm : R.map a ≫ w.app X₁ ≫ B.map b = g), f = mk w g X₁ a b comm

Proof state:
case intro.intro.intro.intro.intro.intro
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
b : L.obj X₁ ⟶ X₃
a : (CostructuredArrow.mk g).left ⟶ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).left
ha : R.map a ≫ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).hom = (CostructuredArrow.mk g).hom
⊢ ∃ X₁_1 a_1 b_1,
    ∃ (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b_1 = g),
      StructuredArrow.mk (CostructuredArrow.homMk a ha) = mk w g X₁_1 a_1 b_1 comm

Tactic:
exact ⟨X₁, a, b, by simpa using ha, rfl⟩

Result:
no goals

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f : w.StructuredArrowRightwards g
⊢ ∃ X₁ a b, ∃ (comm : R.map a ≫ w.app X₁ ≫ B.map b = g), f = mk w g X₁ a b comm

Tactic:
obtain ⟨g, φ, rfl⟩ := StructuredArrow.mk_surjective f

Result:
case intro.intro
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g✝ : R.obj X₂ ⟶ B.obj X₃
g : CostructuredArrow L X₃
φ : CostructuredArrow.mk g✝ ⟶ (w.costructuredArrowRightwards X₃).obj g
⊢ ∃ X₁ a b, ∃ (comm : R.map a ≫ w.app X₁ ≫ B.map b = g✝), StructuredArrow.mk φ = mk w g✝ X₁ a b comm

Proof state:
case intro.intro
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g✝ : R.obj X₂ ⟶ B.obj X₃
g : CostructuredArrow L X₃
φ : CostructuredArrow.mk g✝ ⟶ (w.costructuredArrowRightwards X₃).obj g
⊢ ∃ X₁ a b, ∃ (comm : R.map a ≫ w.app X₁ ≫ B.map b = g✝), StructuredArrow.mk φ = mk w g✝ X₁ a b comm

Tactic:
obtain ⟨X₁, b, rfl⟩ := g.mk_surjective

Result:
case intro.intro.intro.intro
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
b : L.obj X₁ ⟶ X₃
φ : CostructuredArrow.mk g ⟶ (w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)
⊢ ∃ X₁_1 a b_1, ∃ (comm : R.map a ≫ w.app X₁_1 ≫ B.map b_1 = g), StructuredArrow.mk φ = mk w g X₁_1 a b_1 comm

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
b : L.obj X₁ ⟶ X₃
a : (CostructuredArrow.mk g).left ⟶ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).left
ha : R.map a ≫ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).hom = (CostructuredArrow.mk g).hom
⊢ R.map a ≫ w.app X₁ ≫ B.map b = g

Tactic:
simpa using ha

Result:
no goals

Proof state:
case intro.intro.intro.intro
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
b : L.obj X₁ ⟶ X₃
φ : CostructuredArrow.mk g ⟶ (w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)
⊢ ∃ X₁_1 a b_1, ∃ (comm : R.map a ≫ w.app X₁_1 ≫ B.map b_1 = g), StructuredArrow.mk φ = mk w g X₁_1 a b_1 comm

Tactic:
obtain ⟨a, ha, rfl⟩ := CostructuredArrow.homMk_surjective φ

Result:
case intro.intro.intro.intro.intro.intro
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
b : L.obj X₁ ⟶ X₃
a : (CostructuredArrow.mk g).left ⟶ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).left
ha : R.map a ≫ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).hom = (CostructuredArrow.mk g).hom
⊢ ∃ X₁_1 a_1 b_1,
    ∃ (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b_1 = g),
      StructuredArrow.mk (CostructuredArrow.homMk a ha) = mk w g X₁_1 a_1 b_1 comm