-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
theorem widePushout_exists_rep' {B : C} {α : Type _} [Nonempty α] {X : α → C}
    (f : ∀ j : α, B ⟶ X j) [HasWidePushout.{v} B X f] [PreservesColimit (wideSpan B X f) (forget C)]
    (x : ToType (widePushout B X f)) : ∃ (i : α) (y : ToType (X i)), ι f i y = x

Proof state:
case inl.intro
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType B
⊢ ∃ i y_1, (ConcreteCategory.hom (ι f i)) y_1 = (ConcreteCategory.hom (head f)) y

Tactic:
inhabit α

Result:
case inl.intro
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType B
inhabited_h : Inhabited α
⊢ ∃ i y_1, (ConcreteCategory.hom (ι f i)) y_1 = (ConcreteCategory.hom (head f)) y

Proof state:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType B
inhabited_h : Inhabited α
⊢ (ConcreteCategory.hom (ι f default)) ((ConcreteCategory.hom (f default)) y) = (ConcreteCategory.hom (head f)) y

Tactic:
simp only [← arrow_ι _ default, ConcreteCategory.comp_apply]

Result:
no goals

Proof state:
case inl.intro
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType B
inhabited_h : Inhabited α
⊢ ∃ i y_1, (ConcreteCategory.hom (ι f i)) y_1 = (ConcreteCategory.hom (head f)) y

Tactic:
use default, f _ y

Result:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType B
inhabited_h : Inhabited α
⊢ (ConcreteCategory.hom (ι f default)) ((ConcreteCategory.hom (f default)) y) = (ConcreteCategory.hom (head f)) y

Proof state:
case inr.intro.intro
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
i : α
y : ToType (X i)
⊢ ∃ i_1 y_1, (ConcreteCategory.hom (ι f i_1)) y_1 = (ConcreteCategory.hom (ι f i)) y

Tactic:
use i, y

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
x : ToType (widePushout B X f)
⊢ ∃ i y, (ConcreteCategory.hom (ι f i)) y = x

Tactic:
rcases Concrete.widePushout_exists_rep f x with (⟨y, rfl⟩ | ⟨i, y, rfl⟩)

Result:
case inl.intro
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType B
⊢ ∃ i y_1, (ConcreteCategory.hom (ι f i)) y_1 = (ConcreteCategory.hom (head f)) y

case inr.intro.intro
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
i : α
y : ToType (X i)
⊢ ∃ i_1 y_1, (ConcreteCategory.hom (ι f i_1)) y_1 = (ConcreteCategory.hom (ι f i)) y