-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
c : BinaryCofan X Y
h₁ :
  Injective (α := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair })) (β :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair }))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
      (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
        (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }))
h₂ :
  Injective (α := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair })) (β :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := right : Discrete WalkingPair }))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
      (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
        (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right }))
h₃ :
  IsCompl (α :=
    Set
      ((fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair })))
    (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
          (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
    (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
          (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })))
this :
  ∀
    (x :
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair })),
    Membership.mem (γ :=
        Set
          ((fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
              { as := left : Discrete WalkingPair })))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
            (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
              (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
        x ∨
      Membership.mem (γ :=
        Set
          ((fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
              { as := right : Discrete WalkingPair })))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
            (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
              (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })))
        x
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : Functor.obj (pair X Y) { as := right : Discrete WalkingPair }
mpr :
  ∀ (x_1 : X)
    (h :
      Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : X) → c.pt) x_1 : c.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : Y) → c.pt) x : c.pt)),
    Eq (α := T)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → T)
          (((Equiv.ofInjective (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) : (a : X) → c.pt) h₁).symm :
                (a : (↑(Set.range (⇑(ConcreteCategory.hom c.inl) : (a : X) → c.pt)) : Type u)) → X)
              (Subtype.mk (p := fun (x : c.pt) ↦
                  Membership.mem (γ := Set c.pt)
                    (Set.range (ι := X) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) : (a : X) → c.pt)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : Y) → c.pt) x) ⋯ :
                { x : c.pt //
                  Membership.mem (γ := Set c.pt)
                    (Set.range (ι := X) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) : (a : X) → c.pt)) x }) :
            X) :
        T)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : Y) → T) x : T)
⊢ Eq (α := T)
    (if h :
          Membership.mem (α := c.pt) (γ := Set c.pt)
            (Set.range (ι := X) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) : (a : X) → c.pt))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : Y) → c.pt) x : c.pt) then
        (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → T)
          (((Equiv.ofInjective (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) : (a : X) → c.pt) h₁).symm :
                (a : (↑(Set.range (⇑(ConcreteCategory.hom c.inl) : (a : X) → c.pt)) : Type u)) → X)
              (Subtype.mk (p := fun (x : c.pt) ↦
                  Membership.mem (γ := Set c.pt)
                    (Set.range (ι := X) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) : (a : X) → c.pt)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : Y) → c.pt) x) h :
                { x : c.pt //
                  Membership.mem (γ := Set c.pt)
                    (Set.range (ι := X) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) : (a : X) → c.pt)) x }) :
            X)
      else
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : Y) → T)
          (((Equiv.ofInjective (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) : (a : Y) → c.pt) h₂).symm :
                (a : (↑(Set.range (⇑(ConcreteCategory.hom c.inr) : (a : Y) → c.pt)) : Type u)) → Y)
              (Subtype.mk (p := fun (x : c.pt) ↦
                  Membership.mem (γ := Set c.pt)
                    (Set.range (ι := Y) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) : (a : Y) → c.pt)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : Y) → c.pt) x) ⋯ :
                { x : c.pt //
                  Membership.mem (γ := Set c.pt)
                    (Set.range (ι := Y) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) : (a : Y) → c.pt)) x }) :
            Y) :
      T)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : Y) → T) x : T)

Tactic:
simp only [Set.mem_range, Equiv.ofInjective_symm_apply, dite_eq_right_iff,
          forall_exists_index]

Premises used: Set.mem_range, forall_exists_index, dite_eq_right_iff, Equiv.ofInjective_symm_apply