awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
f : J → C
inst_1 : HasProduct.{w, v, u} f
D : Type t
inst_2 : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst_3 : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst_4 : ConcreteCategory D FD (CC := DD)
F : Functor.{v, r, u, t} C D
inst_5 : PreservesLimit (Discrete.functor f) F
inst_6 : HasProduct.{w, r, t} (C := D) fun (j : J) ↦ F.obj (f j)
inst_7 : PreservesLimitsOfShape WalkingCospan (forget D (FC := FD) (CC := DD))
inst_8 : PreservesLimit (J := Discrete J) (Discrete.functor fun (b : J) ↦ F.obj (f b)) (forget D (FC := FD) (CC := DD))
x y : ToType (FC := FD) (CC := DD) (F.obj (piObj.{w, v, u} f))
h :
  ∀ (i : J),
    Eq (α := DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) x : DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) y : DD (F.obj (f i)))
j : J
a :
  Eq (α := DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
    ((hom (FC := FD) (CC := DD) (F.map (Pi.π f j)) :
          (a : DD (F.obj (∏ᶜ f))) → DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
        x :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
    ((hom (FC := FD) (CC := DD) (F.map (Pi.π f j)) :
          (a : DD (F.obj (∏ᶜ f))) → DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
        y :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
⊢ Eq (α := DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
    ((hom (FC := FD) (CC := DD) (limit.π (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }) :
          (a : DD (limit (Discrete.functor fun (b : J) ↦ F.obj (f b)))) →
            DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
        ((hom (FC := FD) (CC := DD) (piComparison F f) : (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (b : J) ↦ F.obj (f b)))
          x) :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
    ((hom (FC := FD) (CC := DD) (limit.π (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }) :
          (a : DD (limit (Discrete.functor fun (b : J) ↦ F.obj (f b)))) →
            DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
        ((hom (FC := FD) (CC := DD) (piComparison F f) : (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (b : J) ↦ F.obj (f b)))
          y) :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, piComparison_comp_π]

Premises used: CategoryTheory.Limits.piComparison_comp_π, CategoryTheory.ConcreteCategory.comp_apply
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
f : J → C
inst_1 : HasProduct.{w, v, u} f
D : Type t
inst_2 : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst_3 : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst_4 : ConcreteCategory D FD (CC := DD)
F : Functor.{v, r, u, t} C D
inst_5 : PreservesLimit (Discrete.functor f) F
inst_6 : HasProduct.{w, r, t} (C := D) fun (j : J) ↦ F.obj (f j)
inst_7 : PreservesLimitsOfShape WalkingCospan (forget D (FC := FD) (CC := DD))
inst_8 : PreservesLimit (J := Discrete J) (Discrete.functor fun (b : J) ↦ F.obj (f b)) (forget D (FC := FD) (CC := DD))
x y : ToType (FC := FD) (CC := DD) (F.obj (piObj.{w, v, u} f))
h :
  ∀ (i : J),
    Eq (α := DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) x : DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) y : DD (F.obj (f i)))
j : J
⊢ Eq (α := DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
    ((hom (FC := FD) (CC := DD) (F.map (Pi.π f j)) :
          (a : DD (F.obj (∏ᶜ f))) → DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
        x :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
    ((hom (FC := FD) (CC := DD) (F.map (Pi.π f j)) :
          (a : DD (F.obj (∏ᶜ f))) → DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
        y :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))

Tactic:
h j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
f : J → C
inst_1 : HasProduct.{w, v, u} f
D : Type t
inst_2 : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst_3 : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst_4 : ConcreteCategory D FD (CC := DD)
F : Functor.{v, r, u, t} C D
inst_5 : PreservesLimit (Discrete.functor f) F
inst_6 : HasProduct.{w, r, t} (C := D) fun (j : J) ↦ F.obj (f j)
inst_7 : PreservesLimitsOfShape WalkingCospan (forget D (FC := FD) (CC := DD))
inst_8 : PreservesLimit (J := Discrete J) (Discrete.functor fun (b : J) ↦ F.obj (f b)) (forget D (FC := FD) (CC := DD))
x y : ToType (FC := FD) (CC := DD) (F.obj (piObj.{w, v, u} f))
h :
  ∀ (i : J),
    Eq (α := DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) x : DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) y : DD (F.obj (f i)))
j : J
⊢ Eq (α := DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
    ((hom (FC := FD) (CC := DD) (F.map (Pi.π f j)) :
          (a : DD (F.obj (∏ᶜ f))) → DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
        x :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))
    ((hom (FC := FD) (CC := DD) (F.map (Pi.π f j)) :
          (a : DD (F.obj (∏ᶜ f))) → DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj { as := j }))
        y :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) { as := j : Discrete J }))

Tactic:
exact h j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 : PreservesColimit.{0, 0, v, w, u, w + 1} (Functor.empty C) (forget C (FC := FC) (CC := CC))
X : C
h : Nonempty (IsInitial.{v, u} X)
rw : Nonempty.{w + 2} (IsInitial (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X))
⊢ IsEmpty.{w + 1} (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X)

Tactic:
rw [← Types.initial_iff_empty]

Premises used: CategoryTheory.Limits.Types.initial_iff_empty
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 : PreservesColimit.{0, 0, v, w, u, w + 1} (Functor.empty C) (forget C (FC := FC) (CC := CC))
X : C
h : Nonempty (IsInitial.{v, u} X)
⊢ Nonempty.{w + 2} (IsInitial (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X))

Tactic:
Nonempty.map (IsInitial.isInitialObj (forget C) _) h

Premises used: CategoryTheory.Limits.IsInitial.isInitialObj, CategoryTheory.forget, Nonempty.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 : PreservesColimit.{0, 0, v, w, u, w + 1} (Functor.empty C) (forget C (FC := FC) (CC := CC))
X : C
h : Nonempty (IsInitial.{v, u} X)
⊢ Nonempty.{w + 2} (IsInitial (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X))

Tactic:
exact Nonempty.map (IsInitial.isInitialObj (forget C) _) h

Premises used: CategoryTheory.Limits.IsInitial.isInitialObj, CategoryTheory.forget, Nonempty.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 : ReflectsColimit.{0, 0, v, w, u, w + 1} (Functor.empty C) (forget C (FC := FC) (CC := CC))
X : C
h : IsEmpty.{w + 1} (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X)
⊢ Nonempty (IsInitial.{v, u} X)

Tactic:
Nonempty.map (IsInitial.isInitialOfObj (forget C) _) <|
    (Types.initial_iff_empty (ToType X)).mpr h

Premises used: Iff.mpr, CategoryTheory.Limits.Types.initial_iff_empty, CategoryTheory.Limits.IsInitial.isInitialOfObj, CategoryTheory.forget, CategoryTheory.ToType, Nonempty.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 : PreservesColimit.{0, 0, v, w, u, w + 1} (Functor.empty C) (forget C (FC := FC) (CC := CC))
inst_4 : ReflectsColimit.{0, 0, v, w, u, w + 1} (Functor.empty C) (forget C (FC := FC) (CC := CC))
X : C
rw : Nonempty (IsInitial.{v, u} X) ↔ Nonempty.{w + 2} (IsInitial (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X))
rw₁ rw₂ :
  Nonempty.{w + 2} (IsInitial (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)) ↔
    Nonempty.{w + 2} (IsInitial (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X))
⊢ Nonempty (IsInitial.{v, u} X) ↔ IsEmpty.{w + 1} (ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X)

Tactic:
rw [← Types.initial_iff_empty, (IsInitial.isInitialIffObj (forget C) X).nonempty_congr]

Premises used: CategoryTheory.Limits.Types.initial_iff_empty, CategoryTheory.Limits.IsInitial.isInitialIffObj, CategoryTheory.forget, Equiv.nonempty_congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X₁ X₂ : C
inst_3 : HasBinaryProduct.{v, u} X₁ X₂
inst_4 : PreservesLimit.{0, 0, v, w, u, w + 1} (pair X₁ X₂) (forget C (FC := FC) (CC := CC))
x : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)
⊢ Eq (α := ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁)
    (((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) x).1 :
      ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁)
    ((hom (FC := FC) (CC := CC) prod.fst : (a : CC (X₁ ⨯ X₂)) → CC X₁) x : CC X₁)

Tactic:
simpa using congr_hom (prodComparison_fst (forget C) X₁ X₂) x

Premises used: CategoryTheory.Limits.prodComparison_fst, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X₁ X₂ : C
inst_3 : HasBinaryProduct.{v, u} X₁ X₂
inst_4 : PreservesLimit.{0, 0, v, w, u, w + 1} (pair X₁ X₂) (forget C (FC := FC) (CC := CC))
x : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)
⊢ Eq (α := ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂)
    (((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) x).2 :
      ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂)
    ((hom (FC := FC) (CC := CC) prod.snd : (a : CC (X₁ ⨯ X₂)) → CC X₂) x : CC X₂)

Tactic:
simpa using congr_hom (prodComparison_snd (forget C) X₁ X₂) x

Premises used: CategoryTheory.Limits.prodComparison_snd, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X₁ X₂ : C
inst_3 : HasBinaryProduct.{v, u} X₁ X₂
inst_4 : PreservesLimit.{0, 0, v, w, u, w + 1} (pair X₁ X₂) (forget C (FC := FC) (CC := CC))
x : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁ × ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂
obtain :
  ∀ (y : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)),
    Eq (α := CC X₁)
      ((hom (FC := FC) (CC := CC) prod.fst : (a : CC (X₁ ⨯ X₂)) → CC X₁)
          ((Equiv.symm (prodEquiv (FC := FC) (CC := CC) X₁ X₂) : (a : ToType X₁ × ToType X₂) → ToType (X₁ ⨯ X₂))
              ((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y :
                ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁ × ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂) :
            ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)) :
        CC X₁)
      (((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y).1 :
        ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁)
⊢ (hom (FC := FC) (CC := CC) prod.fst : (a : CC (X₁ ⨯ X₂)) → CC X₁)
      ((Equiv.symm (prodEquiv (FC := FC) (CC := CC) X₁ X₂) : (a : ToType X₁ × ToType X₂) → ToType (X₁ ⨯ X₂)) x :
        ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)) =
    x.1

Tactic:
obtain ⟨y, rfl⟩ := (prodEquiv X₁ X₂).surjective x

Premises used: CategoryTheory.Limits.Concrete.prodEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X₁ X₂ : C
inst_3 : HasBinaryProduct.{v, u} X₁ X₂
inst_4 : PreservesLimit.{0, 0, v, w, u, w + 1} (pair X₁ X₂) (forget C (FC := FC) (CC := CC))
y : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)
⊢ Eq (α := CC X₁)
    ((hom (FC := FC) (CC := CC) prod.fst : (a : CC (X₁ ⨯ X₂)) → CC X₁)
        ((Equiv.symm (prodEquiv (FC := FC) (CC := CC) X₁ X₂) : (a : ToType X₁ × ToType X₂) → ToType (X₁ ⨯ X₂))
            ((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y :
              ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁ × ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂) :
          ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)) :
      CC X₁)
    (((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y).1 :
      ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X₁ X₂ : C
inst_3 : HasBinaryProduct.{v, u} X₁ X₂
inst_4 : PreservesLimit.{0, 0, v, w, u, w + 1} (pair X₁ X₂) (forget C (FC := FC) (CC := CC))
x : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁ × ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂
obtain :
  ∀ (y : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)),
    Eq (α := CC X₂)
      ((hom (FC := FC) (CC := CC) prod.snd : (a : CC (X₁ ⨯ X₂)) → CC X₂)
          ((Equiv.symm (prodEquiv (FC := FC) (CC := CC) X₁ X₂) : (a : ToType X₁ × ToType X₂) → ToType (X₁ ⨯ X₂))
              ((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y :
                ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁ × ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂) :
            ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)) :
        CC X₂)
      (((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y).2 :
        ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂)
⊢ (hom (FC := FC) (CC := CC) prod.snd : (a : CC (X₁ ⨯ X₂)) → CC X₂)
      ((Equiv.symm (prodEquiv (FC := FC) (CC := CC) X₁ X₂) : (a : ToType X₁ × ToType X₂) → ToType (X₁ ⨯ X₂)) x :
        ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)) =
    x.2

Tactic:
obtain ⟨y, rfl⟩ := (prodEquiv X₁ X₂).surjective x

Premises used: CategoryTheory.Limits.Concrete.prodEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X₁ X₂ : C
inst_3 : HasBinaryProduct.{v, u} X₁ X₂
inst_4 : PreservesLimit.{0, 0, v, w, u, w + 1} (pair X₁ X₂) (forget C (FC := FC) (CC := CC))
y : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)
⊢ Eq (α := CC X₂)
    ((hom (FC := FC) (CC := CC) prod.snd : (a : CC (X₁ ⨯ X₂)) → CC X₂)
        ((Equiv.symm (prodEquiv (FC := FC) (CC := CC) X₁ X₂) : (a : ToType X₁ × ToType X₂) → ToType (X₁ ⨯ X₂))
            ((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y :
              ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₁ × ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂) :
          ToType.{w, v, u, u_1} (FC := FC) (CC := CC) (prod.{v, u} X₁ X₂)) :
      CC X₂)
    (((prodEquiv (FC := FC) (CC := CC) X₁ X₂ : (a : ToType (X₁ ⨯ X₂)) → ToType X₁ × ToType X₂) y).2 :
      ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst_3 : HasPullback f₁ f₂
inst_4 : PreservesLimit (cospan f₁ f₂) (forget C (FC := FC) (CC := CC))
x : ToType (FC := FC) (CC := CC) (pullback f₁ f₂)
obtain :
  ∀ (x₁ : ToType (FC := FC) (CC := CC) X₁) (x₂ : ToType (FC := FC) (CC := CC) X₂)
    (h :
      Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) (x₁, x₂).1 : CC S)
        ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) (x₁, x₂).2 : CC S)),
    ∃ (x₁_1 : ToType (FC := FC) (CC := CC) X₁) (x₂_1 : ToType (FC := FC) (CC := CC) X₂) (h_1 :
      Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) x₁_1 : CC S)
        ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) x₂_1 : CC S)),
      Eq (α := ToType (FC := FC) (CC := CC) (pullback f₁ f₂))
        ((Equiv.symm (pullbackEquiv (FC := FC) (CC := CC) f₁ f₂) :
              (a :
                  { p : ToType X₁ × ToType X₂ //
                    (hom f₁ : (a : CC X₁) → CC S) p.1 = (hom f₂ : (a : CC X₂) → CC S) p.2 }) →
                ToType (pullback f₁ f₂))
            (Subtype.mk (p := fun (p : ToType (FC := FC) (CC := CC) X₁ × ToType (FC := FC) (CC := CC) X₂) ↦
              Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) p.1 : CC S)
                ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) p.2 : CC S))
              (x₁, x₂) h) :
          ToType (FC := FC) (CC := CC) (pullback f₁ f₂))
        (pullbackMk (FC := FC) (CC := CC) f₁ f₂ x₁_1 x₂_1 h_1 : ToType (FC := FC) (CC := CC) (pullback f₁ f₂))
⊢ ∃ (x₁ : ToType (FC := FC) (CC := CC) X₁) (x₂ : ToType (FC := FC) (CC := CC) X₂) (h :
    Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) x₁ : CC S)
      ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) x₂ : CC S)),
    x = pullbackMk (FC := FC) (CC := CC) f₁ f₂ x₁ x₂ h

Tactic:
obtain ⟨⟨⟨x₁, x₂⟩, h⟩, rfl⟩ := (pullbackEquiv f₁ f₂).symm.surjective x

Premises used: CategoryTheory.Limits.Concrete.pullbackEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst_3 : HasPullback f₁ f₂
inst_4 : PreservesLimit (cospan f₁ f₂) (forget C (FC := FC) (CC := CC))
x₁ : ToType (FC := FC) (CC := CC) X₁
x₂ : ToType (FC := FC) (CC := CC) X₂
h :
  Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) (x₁, x₂).1 : CC S)
    ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) (x₁, x₂).2 : CC S)
⊢ ∃ (x₁_1 : ToType (FC := FC) (CC := CC) X₁) (x₂_1 : ToType (FC := FC) (CC := CC) X₂) (h_1 :
    Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) x₁_1 : CC S)
      ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) x₂_1 : CC S)),
    Eq (α := ToType (FC := FC) (CC := CC) (pullback f₁ f₂))
      ((Equiv.symm (pullbackEquiv (FC := FC) (CC := CC) f₁ f₂) :
            (a :
                { p : ToType X₁ × ToType X₂ //
                  (hom f₁ : (a : CC X₁) → CC S) p.1 = (hom f₂ : (a : CC X₂) → CC S) p.2 }) →
              ToType (pullback f₁ f₂))
          (Subtype.mk (p := fun (p : ToType (FC := FC) (CC := CC) X₁ × ToType (FC := FC) (CC := CC) X₂) ↦
            Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) p.1 : CC S)
              ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) p.2 : CC S))
            (x₁, x₂) h) :
        ToType (FC := FC) (CC := CC) (pullback f₁ f₂))
      (pullbackMk (FC := FC) (CC := CC) f₁ f₂ x₁_1 x₂_1 h_1 : ToType (FC := FC) (CC := CC) (pullback f₁ f₂))

Tactic:
⟨x₁, x₂, h, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst_3 : HasPullback f₁ f₂
inst_4 : PreservesLimit (cospan f₁ f₂) (forget C (FC := FC) (CC := CC))
x₁ : ToType (FC := FC) (CC := CC) X₁
x₂ : ToType (FC := FC) (CC := CC) X₂
h :
  Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) (x₁, x₂).1 : CC S)
    ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) (x₁, x₂).2 : CC S)
⊢ ∃ (x₁_1 : ToType (FC := FC) (CC := CC) X₁) (x₂_1 : ToType (FC := FC) (CC := CC) X₂) (h_1 :
    Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) x₁_1 : CC S)
      ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) x₂_1 : CC S)),
    Eq (α := ToType (FC := FC) (CC := CC) (pullback f₁ f₂))
      ((Equiv.symm (pullbackEquiv (FC := FC) (CC := CC) f₁ f₂) :
            (a :
                { p : ToType X₁ × ToType X₂ //
                  (hom f₁ : (a : CC X₁) → CC S) p.1 = (hom f₂ : (a : CC X₂) → CC S) p.2 }) →
              ToType (pullback f₁ f₂))
          (Subtype.mk (p := fun (p : ToType (FC := FC) (CC := CC) X₁ × ToType (FC := FC) (CC := CC) X₂) ↦
            Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) p.1 : CC S)
              ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) p.2 : CC S))
            (x₁, x₂) h) :
        ToType (FC := FC) (CC := CC) (pullback f₁ f₂))
      (pullbackMk (FC := FC) (CC := CC) f₁ f₂ x₁_1 x₂_1 h_1 : ToType (FC := FC) (CC := CC) (pullback f₁ f₂))

Tactic:
exact ⟨x₁, x₂, h, rfl⟩