Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: case id.id
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : WidePushoutShape J
⊢ ∀ (xi xj : F.obj i),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id i))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

pp: case id.init
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
j : J
⊢ ∀ (xi : F.obj (some j)) (xj : F.obj none),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id (some j)))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init j))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

pp: case init.id
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi : F.obj none) (xj : F.obj (some i)),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id (some i)))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

pp: case init.init
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi xj : F.obj none),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

Tactic:
· simpa using fun x ↦ ⟨_, 𝟙 _, 𝟙 _, x, by simp⟩

Goal state after:
case id.init
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
j : J
⊢ ∀ (xi : F.obj (some j)) (xj : F.obj none),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id (some j)))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init j))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

case init.id
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi : F.obj none) (xj : F.obj (some i)),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id (some i)))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

case init.init
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi xj : F.obj none),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj