-- Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean
lemma isConnected :
    IsConnected ((TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 _)
      (Functor.rightUnitor _).inv).CostructuredArrowDownwards y)

Proof state:
case intro.intro.intro.intro.refine_2.f
C₁ : Type u_1
C₂ : Type u_2
inst✝⁷ : Category.{u_4, u_1} C₁
inst✝⁶ : Category.{u_5, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{u_6, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) :=
  TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv
this✝ : Nonempty (w.CostructuredArrowDownwards y)
c : C₁
g : X₂ ⟶ Φ.functor.obj c
x : L.obj (Φ.functor.obj c) ⟶ X₃
fac✝ : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary (Φ.arrow.RightResolution (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (𝟙 (Φ.functor.obj c)) ⋯))
    ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk ρ.w.right ⋯))
⊢ (fromRightResolution Φ L y).obj (RightResolution.mk ρ.w.left ⋯) ⟶
    (fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk ρ.w.right ⋯)

Tactic:
refine CostructuredArrow.homMk (StructuredArrow.homMk ρ.X₁.hom (by simp)) ?_

Result:
case intro.intro.intro.intro.refine_2.f
C₁ : Type u_1
C₂ : Type u_2
inst✝⁷ : Category.{u_4, u_1} C₁
inst✝⁶ : Category.{u_5, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{u_6, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) :=
  TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv
this✝ : Nonempty (w.CostructuredArrowDownwards y)
c : C₁
g : X₂ ⟶ Φ.functor.obj c
x : L.obj (Φ.functor.obj c) ⟶ X₃
fac✝ : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary (Φ.arrow.RightResolution (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (𝟙 (Φ.functor.obj c)) ⋯))
    ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk ρ.w.right ⋯))
⊢ ((TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv).structuredArrowDownwards X₂).map
        (StructuredArrow.homMk ρ.X₁.hom ⋯) ≫
      ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
          (RightResolution.mk ρ.w.right ⋯)).hom =
    ((fromRightResolution Φ L y).obj (RightResolution.mk ρ.w.left ⋯)).hom

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁷ : Category.{u_4, u_1} C₁
inst✝⁶ : Category.{u_5, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{u_6, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
⊢ IsConnected
    ((TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv).CostructuredArrowDownwards y)

Tactic:
let w := (TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 _) (Functor.rightUnitor _).inv)

Result:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁷ : Category.{u_4, u_1} C₁
inst✝⁶ : Category.{u_5, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{u_6, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) :=
  TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv
⊢ IsConnected
    ((TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv).CostructuredArrowDownwards y)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁷ : Category.{u_4, u_1} C₁
inst✝⁶ : Category.{u_5, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{u_6, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) :=
  TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv
this : Nonempty (w.CostructuredArrowDownwards y)
X : w.CostructuredArrowDownwards y
⊢ ∃ Y, Zigzag X ((fromRightResolution Φ L y).obj Y)

Tactic:
obtain ⟨c, g, x, fac, rfl⟩ := TwoSquare.CostructuredArrowDownwards.mk_surjective X

Result:
case intro.intro.intro.intro
C₁ : Type u_1
C₂ : Type u_2
inst✝⁷ : Category.{u_4, u_1} C₁
inst✝⁶ : Category.{u_5, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{u_6, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) :=
  TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv
this : Nonempty (w.CostructuredArrowDownwards y)
c : C₁
g : X₂ ⟶ Φ.functor.obj c
x : (Φ.functor ⋙ L).obj c ⟶ X₃
fac : L.map g ≫ w.app c ≫ (𝟭 D).map x = y
⊢ ∃ Y, Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac) ((fromRightResolution Φ L y).obj Y)