-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
theorem widePushout_exists_rep {B : C} {α : Type _} {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)) :
    (∃ y : ToType B, head f y = x) ∨ ∃ (i : α) (y : ToType (X i)), ι f i y = x

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
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)
⊢ (∃ y, (ConcreteCategory.hom (head f)) y = x) ∨ ∃ i y, (ConcreteCategory.hom (ι f i)) y = x

Tactic:
obtain ⟨_ | j, y, rfl⟩ := Concrete.colimit_exists_rep _ x

Result:
case intro.none.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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ (∃ y_1, (ConcreteCategory.hom (head f)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) none)) y) ∨
    ∃ i y_1, (ConcreteCategory.hom (ι f i)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) none)) y

case intro.some.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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ (∃ y_1, (ConcreteCategory.hom (head f)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) (some j))) y) ∨
    ∃ i y_1, (ConcreteCategory.hom (ι f i)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) (some j))) y

Proof state:
case intro.some.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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ (∃ y_1, (ConcreteCategory.hom (head f)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) (some j))) y) ∨
    ∃ i y_1, (ConcreteCategory.hom (ι f i)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) (some j))) y

Tactic:
right

Result:
case intro.some.intro.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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ ∃ i y_1, (ConcreteCategory.hom (ι f i)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) (some j))) y

Proof state:
case intro.none.intro.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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ ∃ y_1, (ConcreteCategory.hom (head f)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) none)) y

Tactic:
use 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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ (ConcreteCategory.hom (head f)) y = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) none)) 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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ (ConcreteCategory.hom (ι f j)) y = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) (some j))) y

Tactic:
rfl

Result:
no goals

Proof state:
case intro.some.intro.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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ ∃ i y_1, (ConcreteCategory.hom (ι f i)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) (some j))) y

Tactic:
use j, 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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ (ConcreteCategory.hom (ι f j)) y = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) (some j))) y

Proof state:
case intro.none.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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ (∃ y_1, (ConcreteCategory.hom (head f)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) none)) y) ∨
    ∃ i y_1, (ConcreteCategory.hom (ι f i)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) none)) y

Tactic:
left

Result:
case intro.none.intro.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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ ∃ y_1, (ConcreteCategory.hom (head f)) y_1 = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) none)) 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
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ (ConcreteCategory.hom (head f)) y = (ConcreteCategory.hom (colimit.ι (wideSpan B X f) none)) y

Tactic:
rfl

Result:
no goals