awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop) b, a,
      x, h₁, h₂ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
subst :
  ∀ (h₁ : J.fst a = J.snd a),
    let f : (left a ⟶ right (J.snd a)) → Prop := fun (x : left a ⟶ right (J.snd a)) ↦
      match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop)
        J.snd a, a, x, h₁, ⋯ with
      | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
      | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False;
    f (Hom.snd a ≫ eqToHom ⋯) = False
⊢ f (Hom.snd a ≫ eqToHom ⋯) = False

Tactic:
subst h₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
h₁ : J.fst a = J.snd a
f : (left a ⟶ right (J.snd a)) → Prop :=
  fun (x : left a ⟶ right (J.snd a)) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop)
      J.snd a, a, x, h₁, ⋯ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
simp :
  (match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop)
      J.snd a, a, Hom.snd a ≫ 𝟙 (right (J.snd a)), h₁, ⋯ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False) =
    False
⊢ f (Hom.snd a ≫ eqToHom ⋯) = False

Tactic:
simp only [eqToHom_refl, f]

Premises used: CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop) b, a,
      x, h₁, h₂ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
tactic :
  ∀ (h₁ : J.fst a = J.snd a),
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop)
      J.snd a, a, Hom.snd a ≫ 𝟙 (right (J.snd a)), h₁, ⋯ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
| f (Hom.snd a ≫ eqToHom ⋯)

Tactic:
tactic => subst h₂; simp only [eqToHom_refl, f]

Premises used: CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop) b, a,
      x, h₁, h₂ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
pos : True ≠ False
⊢ True ≠ f (Hom.snd a ≫ eqToHom ⋯)

Tactic:
conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, f]

Premises used: CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop) b, a,
      x, h₁, h₂ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
⊢ True ≠ False

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : ¬J.snd a = b
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {Hom.fst a ≫ eqToHom ⋯} 0).Nodup

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst a = b
h : J.snd a = b
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 {Hom.snd a ≫ eqToHom ⋯}).Nodup

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst a = b
h : ¬J.snd a = b
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 0).Nodup

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
⊢ Hom.fst a ∈
    {
      val :=
        HAdd.hAdd (α := Multiset (left a ⟶ right (J.fst a)))
          (if e : J.fst a = J.fst a then {Hom.fst a ≫ eqToHom ⋯} else 0)
          (if e : J.snd a = J.fst a then {Hom.snd a ≫ eqToHom ⋯} else 0),
      nodup := ⋯ : Finset (left a ⟶ right (J.fst a)) }

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
⊢ Hom.snd a ∈
    {
      val :=
        HAdd.hAdd (α := Multiset (left a ⟶ right (J.snd a)))
          (if e : J.fst a = J.snd a then {Hom.fst a ≫ eqToHom ⋯} else 0)
          (if e : J.snd a = J.snd a then {Hom.snd a ≫ eqToHom ⋯} else 0),
      nodup := ⋯ : Finset (left a ⟶ right (J.snd a)) }

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.R
⊢ Membership.mem (γ := Finset (right a ⟶ right a)) (if e : a = a then {eqToHom ⋯} else ∅) (Hom.id (right a))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteLimits.{v, u} C
⊢ HasFiniteProducts.{v, u} C

Tactic:
⟨fun _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteProducts.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
ι : Type w
inst_2 : Finite ι
rcases : ∀ (n : ℕ) (e : ι ≃ Fin n), HasLimitsOfShape.{w, w, v, u} (Discrete ι) C
⊢ HasLimitsOfShape.{w, w, v, u} (Discrete ι) C

Tactic:
rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
ι : Type w
inst_2 : Finite ι
n : ℕ
e : ι ≃ Fin n
⊢ HasLimitsOfShape.{0, 0, v, u} (Discrete (Fin n)) C

Tactic:
haveI : HasLimitsOfShape (Discrete (Fin n)) C := HasFiniteProducts.out n
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
ι : Type w
inst_2 : Finite ι
n : ℕ
e : ι ≃ Fin n
this : HasLimitsOfShape.{0, 0, v, u} (Discrete (Fin n)) C
⊢ HasLimitsOfShape.{w, w, v, u} (Discrete ι) C

Tactic:
hasLimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, Equiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
ι : Type w
inst_2 : Finite ι
n : ℕ
e : ι ≃ Fin n
this : HasLimitsOfShape.{0, 0, v, u} (Discrete (Fin n)) C
⊢ HasLimitsOfShape.{w, w, v, u} (Discrete ι) C

Tactic:
exact hasLimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, Equiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{w, v, u} C
⊢ HasFiniteProducts.{v, u} C

Tactic:
⟨fun _ => hasLimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift.{w})⟩

Premises used: Equiv.ulift, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.HasFiniteProducts.mk, CategoryTheory.Limits.hasLimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
ι : Type w
inst_2 : Finite ι
rcases : ∀ (n : ℕ) (e : ι ≃ Fin n), HasColimitsOfShape.{w, w, v, u} (Discrete ι) C
⊢ HasColimitsOfShape.{w, w, v, u} (Discrete ι) C

Tactic:
rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
ι : Type w
inst_2 : Finite ι
n : ℕ
e : ι ≃ Fin n
⊢ HasColimitsOfShape.{0, 0, v, u} (Discrete (Fin n)) C

Tactic:
haveI : HasColimitsOfShape (Discrete (Fin n)) C := HasFiniteCoproducts.out n
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
ι : Type w
inst_2 : Finite ι
n : ℕ
e : ι ≃ Fin n
this : HasColimitsOfShape.{0, 0, v, u} (Discrete (Fin n)) C
⊢ HasColimitsOfShape.{w, w, v, u} (Discrete ι) C

Tactic:
hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, Equiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
ι : Type w
inst_2 : Finite ι
n : ℕ
e : ι ≃ Fin n
this : HasColimitsOfShape.{0, 0, v, u} (Discrete (Fin n)) C
⊢ HasColimitsOfShape.{w, w, v, u} (Discrete ι) C

Tactic:
exact hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, Equiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteColimits.{v, u} C
J : ℕ
⊢ HasColimitsOfShape.{0, 0, v, u} (Discrete (Fin J)) C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
⊢ HasFiniteCoproducts.{v, u} C

Tactic:
⟨fun _ => hasColimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift.{w})⟩

Premises used: Equiv.ulift, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Limits.HasFiniteCoproducts.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
τ₁ : F ⟶ F₁
τ₂ : F ⟶ F₂
⊢ lift τ₁ τ₂ ≫ fst = τ₁

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
τ₁ : F ⟶ F₁
τ₂ : F ⟶ F₂
⊢ lift τ₁ τ₂ ≫ snd = τ₂

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : Cone (pair F G)
x_1 : x.pt ⟶ (binaryProductCone F G).pt
h : ∀ (j : Discrete WalkingPair), x_1 ≫ (binaryProductCone F G).π.app j = x.π.app j
simp :
  x_1 =
    prod.lift (x_1 ≫ (binaryProductCone F G).π.app { as := WalkingPair.left })
      (x_1 ≫ (binaryProductCone F G).π.app { as := WalkingPair.right })
⊢ x_1 = prod.lift (BinaryFan.fst x) (BinaryFan.snd x)

Tactic:
simp only [← h ⟨WalkingPair.right⟩, ← h ⟨WalkingPair.left⟩]

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : Cone (pair F G)
x_1 : x.pt ⟶ (binaryProductCone F G).pt
h : ∀ (j : Discrete WalkingPair), x_1 ≫ (binaryProductCone F G).π.app j = x.π.app j
⊢ x_1 =
    prod.lift (x_1 ≫ (binaryProductCone F G).π.app { as := WalkingPair.left })
      (x_1 ≫ (binaryProductCone F G).π.app { as := WalkingPair.right })

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
⊢ (binaryProductIso F G).hom ≫ prod.fst = Limits.prod.fst

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, CategoryTheory.Limits.limit, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
⊢ (binaryProductIso F G).hom ≫ prod.snd = Limits.prod.snd

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, CategoryTheory.Limits.limit, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
⊢ (binaryProductIso F G).inv ≫ Limits.prod.fst = prod.fst

Tactic:
simp [binaryProductIso, binaryProductLimitCone]

Premises used: CategoryTheory.FunctorToTypes.binaryProductLimitCone, CategoryTheory.FunctorToTypes.binaryProductIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
z : (prod F G).obj a
⊢ (hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.fst a) : (a_1 : (F ⨯ G).obj a) → F.obj a)
      ((hom (FC := TypeCat.Fun) ((binaryProductIso F G).inv.app a) : (a_1 : F.obj a × G.obj a) → (F ⨯ G).obj a) z :
        (F ⨯ G).obj a) =
    z.1

Tactic:
congr_hom (congr_app (binaryProductIso_inv_comp_fst F G) a) z

Premises used: CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.congr_app, CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
⊢ (binaryProductIso F G).inv ≫ Limits.prod.snd = prod.snd

Tactic:
simp [binaryProductIso, binaryProductLimitCone]

Premises used: CategoryTheory.FunctorToTypes.binaryProductLimitCone, CategoryTheory.FunctorToTypes.binaryProductIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
z : (prod F G).obj a
⊢ (hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.snd a) : (a_1 : (F ⨯ G).obj a) → G.obj a)
      ((hom (FC := TypeCat.Fun) ((binaryProductIso F G).inv.app a) : (a_1 : F.obj a × G.obj a) → (F ⨯ G).obj a) z :
        (F ⨯ G).obj a) =
    z.2

Tactic:
congr_hom (congr_app (binaryProductIso_inv_comp_snd F G) a) z

Premises used: CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.congr_app, CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
x : F.obj a
y : G.obj a
⊢ (hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.fst a) :
        (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (F.obj a))
      (prodMk x y) =
    x

Tactic:
simp [prodMk]

Premises used: CategoryTheory.FunctorToTypes.prodMk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
z w : (prod F G).obj a
h1 : z.1 = w.1
h2 : z.2 = w.2
⊢ z = w

Tactic:
Prod.ext h1 h2

Premises used: Prod.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
x : (F ⨯ G).obj a
⊢ (fun (z : F.obj a × G.obj a) ↦ prodMk z.1 z.2)
      ((fun (z : (F ⨯ G).obj a) ↦
          ((((hom (FC := TypeCat.Fun) ((binaryProductIso F G).hom.app a) :
                    (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) ((prod F G).obj a))
                  z).1,
              ((hom (FC := TypeCat.Fun) ((binaryProductIso F G).hom.app a) :
                    (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) ((prod F G).obj a))
                  z).2) :
            F.obj a × G.obj a))
        x) =
    x

Tactic:
simp [-prod_obj, prodMk]

Premises used: CategoryTheory.FunctorToTypes.prod_obj, CategoryTheory.FunctorToTypes.prodMk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
x : F.obj a × G.obj a
⊢ (fun (z : (F ⨯ G).obj a) ↦
        ((((hom (FC := TypeCat.Fun) ((binaryProductIso F G).hom.app a) :
                  (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) ((prod F G).obj a))
                z).1,
            ((hom (FC := TypeCat.Fun) ((binaryProductIso F G).hom.app a) :
                  (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) ((prod F G).obj a))
                z).2) :
          F.obj a × G.obj a))
      ((fun (z : F.obj a × G.obj a) ↦ prodMk z.1 z.2) x) =
    x

Tactic:
simp [-prod_obj, prodMk]

Premises used: CategoryTheory.FunctorToTypes.prod_obj, CategoryTheory.FunctorToTypes.prodMk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
z w : (F ⨯ G).obj a
h1 :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.fst a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (F.obj a))
        z :
      (fun (X : Type w) ↦ X) (F.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.fst a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (F.obj a))
        w :
      (fun (X : Type w) ↦ X) (F.obj a))
h2 :
  Eq (α := (fun (X : Type w) ↦ X) (G.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.snd a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (G.obj a))
        z :
      (fun (X : Type w) ↦ X) (G.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.snd a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (G.obj a))
        w :
      (fun (X : Type w) ↦ X) (G.obj a))
a₁ :
  Eq (α := F.obj a × G.obj a)
    ((binaryProductEquiv F G a : (a_1 : (F ⨯ G).obj a) → F.obj a × G.obj a) z : F.obj a × G.obj a)
    ((binaryProductEquiv F G a : (a_1 : (F ⨯ G).obj a) → F.obj a × G.obj a) w : F.obj a × G.obj a)
⊢ z = w

Tactic:
apply Equiv.injective (binaryProductEquiv F G a)

Premises used: Equiv.injective, CategoryTheory.FunctorToTypes.binaryProductEquiv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
z w : (F ⨯ G).obj a
h1 :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.fst a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (F.obj a))
        z :
      (fun (X : Type w) ↦ X) (F.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.fst a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (F.obj a))
        w :
      (fun (X : Type w) ↦ X) (F.obj a))
h2 :
  Eq (α := (fun (X : Type w) ↦ X) (G.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.snd a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (G.obj a))
        z :
      (fun (X : Type w) ↦ X) (G.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.snd a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (G.obj a))
        w :
      (fun (X : Type w) ↦ X) (G.obj a))
⊢ Eq (α := F.obj a × G.obj a)
    ((binaryProductEquiv F G a : (a_1 : (F ⨯ G).obj a) → F.obj a × G.obj a) z : F.obj a × G.obj a)
    ((binaryProductEquiv F G a : (a_1 : (F ⨯ G).obj a) → F.obj a × G.obj a) w : F.obj a × G.obj a)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : C
h :
  ∀ (val : F.obj x),
    TypeCat.Fun.toFun (X := F.obj x ⊕ G.obj x)
        (hom (FC := TypeCat.Fun)
          (↾Sum.map
              (⇑(hom (FC := TypeCat.Fun) (F.map (𝟙 x))) :
                (a : (fun (X : Type w) ↦ X) (F.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
              (⇑(hom (FC := TypeCat.Fun) (G.map (𝟙 x))) :
                (a : (fun (X : Type w) ↦ X) (G.obj x)) → (fun (X : Type w) ↦ X) (G.obj x))))
        (Sum.inl val) =
      (hom (FC := TypeCat.Fun) (𝟙 (F.obj x ⊕ G.obj x))).toFun (Sum.inl val)
h₁ :
  ∀ (val : G.obj x),
    TypeCat.Fun.toFun (X := F.obj x ⊕ G.obj x)
        (hom (FC := TypeCat.Fun)
          (↾Sum.map
              (⇑(hom (FC := TypeCat.Fun) (F.map (𝟙 x))) :
                (a : (fun (X : Type w) ↦ X) (F.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
              (⇑(hom (FC := TypeCat.Fun) (G.map (𝟙 x))) :
                (a : (fun (X : Type w) ↦ X) (G.obj x)) → (fun (X : Type w) ↦ X) (G.obj x))))
        (Sum.inr val) =
      (hom (FC := TypeCat.Fun) (𝟙 (F.obj x ⊕ G.obj x))).toFun (Sum.inr val)
⊢ ↾Sum.map
        (⇑(hom (FC := TypeCat.Fun) (F.map (𝟙 x))) :
          (a : (fun (X : Type w) ↦ X) (F.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
        (⇑(hom (FC := TypeCat.Fun) (G.map (𝟙 x))) :
          (a : (fun (X : Type w) ↦ X) (G.obj x)) → (fun (X : Type w) ↦ X) (G.obj x)) =
    𝟙 (F.obj x ⊕ G.obj x)

Tactic:
ext ⟨⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : C
val : F.obj x
⊢ TypeCat.Fun.toFun (X := F.obj x ⊕ G.obj x)
      (hom (FC := TypeCat.Fun)
        (↾Sum.map
            (⇑(hom (FC := TypeCat.Fun) (F.map (𝟙 x))) :
              (a : (fun (X : Type w) ↦ X) (F.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
            (⇑(hom (FC := TypeCat.Fun) (G.map (𝟙 x))) :
              (a : (fun (X : Type w) ↦ X) (G.obj x)) → (fun (X : Type w) ↦ X) (G.obj x))))
      (Sum.inl val) =
    (hom (FC := TypeCat.Fun) (𝟙 (F.obj x ⊕ G.obj x))).toFun (Sum.inl val)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : C
val : G.obj x
⊢ TypeCat.Fun.toFun (X := F.obj x ⊕ G.obj x)
      (hom (FC := TypeCat.Fun)
        (↾Sum.map
            (⇑(hom (FC := TypeCat.Fun) (F.map (𝟙 x))) :
              (a : (fun (X : Type w) ↦ X) (F.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
            (⇑(hom (FC := TypeCat.Fun) (G.map (𝟙 x))) :
              (a : (fun (X : Type w) ↦ X) (G.obj x)) → (fun (X : Type w) ↦ X) (G.obj x))))
      (Sum.inr val) =
    (hom (FC := TypeCat.Fun) (𝟙 (F.obj x ⊕ G.obj x))).toFun (Sum.inr val)

Tactic:
simp