awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cone F
X : C
hX : IsTerminal.{v, u} X
f : F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ X
g : F.obj { as := WalkingPair.right : Discrete WalkingPair } ⟶ X
hc :
  IsLimit (F := cospan f g)
    (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair }) (c.π.app { as := WalkingPair.right })
        ⋯ :
      PullbackCone f g)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair } ≫ f =
    hc.lift
        (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
          (m ≫ c.π.app { as := WalkingPair.right }) ⋯) ≫
      c.π.app { as := WalkingPair.left : Discrete WalkingPair } ≫ f

Tactic:
(Category.assoc _ _ _).symm.trans (hc.fac_assoc c' WalkingCospan.left f).symm

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.IsLimit.fac_assoc, CategoryTheory.Limits.WalkingCospan.left, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cone F
X : C
hX : IsTerminal.{v, u} X
f : F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ X
g : F.obj { as := WalkingPair.right : Discrete WalkingPair } ⟶ X
hc :
  IsLimit (F := cospan f g)
    (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair }) (c.π.app { as := WalkingPair.right })
        ⋯ :
      PullbackCone f g)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ Eq (α := s.pt ⟶ (cospan f g).obj (some WalkingPair.left)) (m ≫ c.π.app { as := WalkingPair.left })
    (hc.lift
        (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
          (m ≫ c.π.app { as := WalkingPair.right }) ⋯) ≫
      c.π.app { as := WalkingPair.left : Discrete WalkingPair })

Tactic:
(hc.fac c' WalkingCospan.left).symm

Premises used: CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.cospan, CategoryTheory.Limits.WalkingCospan.left, Eq.symm, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cone F
X : C
hX : IsTerminal.{v, u} X
f : F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ X
g : F.obj { as := WalkingPair.right : Discrete WalkingPair } ⟶ X
hc :
  IsLimit (F := cospan f g)
    (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair }) (c.π.app { as := WalkingPair.right })
        ⋯ :
      PullbackCone f g)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ Eq (α := s.pt ⟶ (cospan f g).obj (some WalkingPair.right)) (m ≫ c.π.app { as := WalkingPair.right })
    (hc.lift
        (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
          (m ≫ c.π.app { as := WalkingPair.right }) ⋯) ≫
      c.π.app { as := WalkingPair.right : Discrete WalkingPair })

Tactic:
(hc.fac c' WalkingCospan.right).symm

Premises used: CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.cospan, Eq.symm, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cone F
X : C
hX : IsTerminal.{v, u} X
f : F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ X
g : F.obj { as := WalkingPair.right : Discrete WalkingPair } ⟶ X
hc :
  IsLimit (F := cospan f g)
    (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair }) (c.π.app { as := WalkingPair.right })
        ⋯ :
      PullbackCone f g)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair } ≫ f =
    hc.lift
        (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
          (m ≫ c.π.app { as := WalkingPair.right }) ⋯) ≫
      c.π.app { as := WalkingPair.left : Discrete WalkingPair } ≫ f

Tactic:
exacts [(Category.assoc _ _ _).symm.trans (hc.fac_assoc c' WalkingCospan.left f).symm,
      (hc.fac c' WalkingCospan.left).symm, (hc.fac c' WalkingCospan.right).symm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.IsLimit.fac_assoc, CategoryTheory.Limits.WalkingCospan.left, Eq.symm, Eq.trans, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal.{v, u} Z
H₂ : IsLimit (F := cospan f g) (PullbackCone.mk h k ⋯)
hc :
  IsLimit (F := cospan f g)
    (PullbackCone.mk ((BinaryFan.mk h k).π.app { as := WalkingPair.left : Discrete WalkingPair })
        ((BinaryFan.mk h k).π.app { as := WalkingPair.right }) ⋯ :
      PullbackCone f g)
f₁ : Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ Z
g₁ : Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶ Z
⊢ IsLimit (BinaryFan.mk h k)

Tactic:
apply isBinaryProductOfIsTerminalIsPullback _ _ H₁

Premises used: isBinaryProductOfIsTerminalIsPullback
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal.{v, u} Z
H₂ : IsLimit (BinaryFan.mk h k)
create :
  (s : PullbackCone f g) →
    { l : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯) //
      l ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst ∧
        l ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd ∧
          ∀ {m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)},
            m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst →
              m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd → m = l }
⊢ IsLimit (F := cospan f g) (PullbackCone.mk h k ⋯)

Tactic:
apply PullbackCone.isLimitAux'

Premises used: CategoryTheory.Limits.PullbackCone.isLimitAux'
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal.{v, u} Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
property :
  BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst ∧
    BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd ∧
      ∀ {m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)},
        m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst →
          m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd → m = BinaryFan.IsLimit.lift H₂ s.fst s.snd
⊢ { l : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯) //
    l ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst ∧
      l ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd ∧
        ∀ {m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)},
          m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst →
            m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd → m = l }

Tactic:
use BinaryFan.IsLimit.lift H₂ s.fst s.snd

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.PullbackCone.snd
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal.{v, u} Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
right :
  BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd ∧
    ∀ {m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)},
      m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst →
        m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd → m = BinaryFan.IsLimit.lift H₂ s.fst s.snd
⊢ BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst ∧
    BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd ∧
      ∀ {m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)},
        m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst →
          m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd → m = BinaryFan.IsLimit.lift H₂ s.fst s.snd

Tactic:
use BinaryFan.IsLimit.lift_fst _ _ _

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal.{v, u} Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
right :
  ∀ {m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)},
    m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst →
      m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd → m = BinaryFan.IsLimit.lift H₂ s.fst s.snd
⊢ BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd ∧
    ∀ {m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)},
      m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst →
        m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd → m = BinaryFan.IsLimit.lift H₂ s.fst s.snd

Tactic:
use BinaryFan.IsLimit.lift_snd _ _ _

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift_snd
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal.{v, u} Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)
h₁ : m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst
h₂ : m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd
right :
  ∀ (j : Discrete WalkingPair),
    m ≫ (BinaryFan.mk h k).π.app j = BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ (BinaryFan.mk h k).π.app j
⊢ m = BinaryFan.IsLimit.lift H₂ s.fst s.snd

Tactic:
apply H₂.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal.{v, u} Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)
h₁ : m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst
h₂ : m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd
⊢ Eq (α := s.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.left })
    (BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.left })

Tactic:
h₁.trans (H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.left⟩).symm

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Discrete.mk, CategoryTheory.Limits.PullbackCone.snd, CategoryTheory.Limits.WalkingPair.left, Eq.symm, Eq.trans, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal.{v, u} Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)
h₁ : m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst
h₂ : m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd
⊢ Eq (α := s.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.left })
    (BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.left })

Tactic:
exact h₁.trans (H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.left⟩).symm

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Discrete.mk, CategoryTheory.Limits.PullbackCone.snd, CategoryTheory.Limits.WalkingPair.left, Eq.symm, Eq.trans, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal.{v, u} Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)
h₁ : m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst
h₂ : m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd
⊢ Eq (α := s.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (m ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.right })
    (BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.right })

Tactic:
h₂.trans (H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.right⟩).symm

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Discrete.mk, CategoryTheory.Limits.PullbackCone.snd, Eq.symm, Eq.trans, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal.{v, u} Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ Cone.pt (F := cospan f g) (PullbackCone.mk h k ⋯)
h₁ : m ≫ PullbackCone.fst (PullbackCone.mk h k ⋯) = s.fst
h₂ : m ≫ PullbackCone.snd (PullbackCone.mk h k ⋯) = s.snd
⊢ Eq (α := s.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (m ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.right })
    (BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.right })

Tactic:
exact h₂.trans (H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.right⟩).symm

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Discrete.mk, CategoryTheory.Limits.PullbackCone.snd, Eq.symm, Eq.trans, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
⊢ HasBinaryProducts.{v, u} C

Tactic:
{ has_limit := fun F => HasLimit.mk (limitConeOfTerminalAndPullbacks F) }

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Limits.HasLimit.mk, limitConeOfTerminalAndPullbacks
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
inst_2 : HasTerminal.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst_5 : PreservesLimitsOfShape WalkingCospan F
K : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
hc :
  IsLimit (F :=
    cospan (X := (K ⋙ F).obj { as := WalkingPair.left }) (Z := F.obj (terminal.{v, u} C))
      (F.2 (terminal.from (K.obj { as := WalkingPair.left })))
      (F.map (terminal.from (K.obj { as := WalkingPair.right }))))
    (PullbackCone.mk
        ((F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π.app { as := WalkingPair.left : Discrete WalkingPair })
        ((F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π.app { as := WalkingPair.right }) ⋯ :
      PullbackCone (X := (K ⋙ F).obj { as := WalkingPair.left }) (Z := F.obj (terminal.{v, u} C))
        (F.2 (terminal.from (K.obj { as := WalkingPair.left })))
        (F.map (terminal.from (K.obj { as := WalkingPair.right }))))
f : (K ⋙ F).obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ F.obj (terminal.{v, u} C)
g : (K ⋙ F).obj { as := WalkingPair.right : Discrete WalkingPair } ⟶ F.obj (terminal.{v, u} C)
⊢ IsLimit (F.mapCone (limitConeOfTerminalAndPullbacks K).cone)

Tactic:
apply
          isBinaryProductOfIsTerminalIsPullback _ _ (isLimitOfHasTerminalOfPreservesLimit F)

Premises used: CategoryTheory.Limits.isLimitOfHasTerminalOfPreservesLimit, isBinaryProductOfIsTerminalIsPullback
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : C
inst_3 : HasBinaryProduct.{v, u} X Y
⊢ Eq.{v + 1} (α := Limits.prod.{v, u} X Y ⟶ X)
    (CategoryStruct.comp (Y := pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y))
      (Iso.hom (prodIsoPullback X Y) :
        Limits.prod.{v, u} X Y ⟶ pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y))
      (pullback.fst (terminal.from X) (terminal.from Y) :
        pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y) ⟶ X))
    prod.fst

Tactic:
limit.isoLimitCone_hom_π (limitConeOfTerminalAndPullbacks _) ⟨.left⟩

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Discrete.functor, CategoryTheory.Limits.limit.isoLimitCone_hom_π, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Discrete.mk, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan, limitConeOfTerminalAndPullbacks, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : C
inst_3 : HasBinaryProduct.{v, u} X Y
⊢ Eq.{v + 1} (α := Limits.prod.{v, u} X Y ⟶ Y)
    (CategoryStruct.comp (Y := pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y))
      (Iso.hom (prodIsoPullback X Y) :
        Limits.prod.{v, u} X Y ⟶ pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y))
      (pullback.snd (terminal.from X) (terminal.from Y) :
        pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y) ⟶ Y))
    prod.snd

Tactic:
limit.isoLimitCone_hom_π (limitConeOfTerminalAndPullbacks _) ⟨.right⟩

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Discrete.functor, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.limit.isoLimitCone_hom_π, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Discrete.mk, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan, limitConeOfTerminalAndPullbacks
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : C
inst_3 : HasBinaryProduct.{v, u} X Y
⊢ Eq.{v + 1} (α := pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y) ⟶ X)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X Y) (Iso.inv (prodIsoPullback X Y)) prod.fst :
      pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y) ⟶ X)
    (pullback.fst (terminal.from X) (terminal.from Y) :
      pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y) ⟶ X)

Tactic:
limit.isoLimitCone_inv_π (limitConeOfTerminalAndPullbacks _) ⟨.left⟩

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Discrete.functor, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Discrete.mk, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan, CategoryTheory.Limits.limit.isoLimitCone_inv_π, limitConeOfTerminalAndPullbacks, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : C
inst_3 : HasBinaryProduct.{v, u} X Y
⊢ Eq.{v + 1} (α := pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y) ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X Y) (Iso.inv (prodIsoPullback X Y)) prod.snd :
      pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y) ⟶ Y)
    (pullback.snd (terminal.from X) (terminal.from Y) :
      pullback.{v, u} (Z := terminal.{v, u} C) (terminal.from X) (terminal.from Y) ⟶ Y)

Tactic:
limit.isoLimitCone_inv_π (limitConeOfTerminalAndPullbacks _) ⟨.right⟩

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Discrete.functor, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Discrete.mk, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan, CategoryTheory.Limits.limit.isoLimitCone_inv_π, limitConeOfTerminalAndPullbacks
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
dsimp :
  m =
    hc.desc
      (PushoutCocone.mk (s.ι.app { as := WalkingPair.left : Discrete WalkingPair })
        (s.ι.app { as := WalkingPair.right }) ⋯)
⊢ m =
    hc.desc
      (PushoutCocone.mk (s.ι.app { as := WalkingPair.left : Discrete WalkingPair })
        (s.ι.app { as := WalkingPair.right }) ⋯)

Tactic:
dsimp