awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ c₂.inr ≫ m = t₁.desc { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } }
have h₂ : ∀ (j : Discrete (Fin n)),
  c₁.ι.app j ≫ c₂.inr ≫ m =
    NatTrans.app
      (Cocone.ι { pt := s.1, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } }) j
Tactic: apply t₁.uniq ⟨_, _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) })
      (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
        { pt := s.1, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } }))
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m)
    (NatTrans.app
      (Cocone.ι { pt := s.1, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } })
      { as := j })
have h₂ : Eq (α :=
  Quiver.Hom.{v, u} (V := C)
    (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
  (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) (s.ι.app { as := j.succ })
Tactic: dsimp only [Discrete.natTrans_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) (s.ι.app { as := j.succ })
have h₂ : Eq (α :=
  Quiver.Hom.{v, u} (V := C)
    (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
  (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) ((extendCofan c₁ c₂).ι.app { as := j.succ } ≫ m)
Tactic: rw [← w ⟨j.succ⟩]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) ((extendCofan c₁ c₂).ι.app { as := j.succ } ≫ m)
have h₂ : Eq (α :=
  Quiver.Hom.{v, u} (V := C)
    (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
  (c₁.ι.app { as := j } ≫ c₂.inr ≫ m)
  (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ f x ⟶ c₂.pt) c₂.inl (fun (i : Fin n) ↦ c₁.ι.app { as := i } ≫ c₂.inr)
      j.succ ≫
    m)
Tactic: dsimp only [extendCofan_ι_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ f x ⟶ c₂.pt) c₂.inl (fun (i : Fin n) ↦ c₁.ι.app { as := i } ≫ c₂.inr)
        j.succ ≫
      m)
have h₂ : Eq (α :=
  Quiver.Hom.{v, u} (V := C)
    (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
  (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) ((c₁.ι.app { as := j } ≫ c₂.inr) ≫ m)
Tactic: rw [Fin.cases_succ, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
h₂ :
  Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) ((c₁.ι.app { as := j } ≫ c₂.inr) ≫ m)
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ f x ⟶ c₂.pt) c₂.inl (fun (i : Fin n) ↦ c₁.ι.app { as := i } ≫ c₂.inr)
        j.succ ≫
      m)
have h₃ : Eq (α :=
  Quiver.Hom.{v, u} (V := C)
    (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
  (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) (c₁.ι.app { as := j } ≫ c₂.inr ≫ m)
Tactic: rw [Fin.cases_succ, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
n : ℕ
K : Functor.{0, v, 0, u} (Discrete (Fin n)) C
that : K ≅ Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 } :=
  Discrete.natIso fun (x : Discrete (Fin n)) ↦
    match (motive :=
      (x : Discrete (Fin n)) →
        K.obj x ≅ Functor.obj.{0, v, 0, u} (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) x)
      x with
    | { as := as } => Iso.refl (K.obj { as := as })
⊢ HasColimit K
have rw : HasColimit.{0, 0, v, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 })
Tactic: rw [hasColimit_iff_of_iso that]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteCoproducts.{v, u} C
n : ℕ
⊢ ∀ (f : Fin (n + 1) → C), PreservesColimit (Discrete.functor f) F
have this : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
Tactic: haveI := preserves_fin_of_preserves_binary_and_initial n
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteCoproducts.{v, u} C
n : ℕ
this : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ PreservesColimit (Discrete.functor f) F
have f₁ : IsColimit (J := Discrete (Fin (n + 1))) (F := Discrete.functor f ⋙ F)
  (F.mapCocone
    (extendCofan (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))
      (colimit.cocone
        (pair (f 0)
          (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
            (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
Tactic: apply
      preservesColimit_of_preserves_colimit_cocone
        (extendCofanIsColimit f (colimit.isColimit _) (colimit.isColimit _)) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteCoproducts.{v, u} C
n : ℕ
this : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ IsColimit (J := Discrete (Fin (n + 1))) (F := Discrete.functor f ⋙ F)
    (F.mapCocone
      (extendCofan (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))
        (colimit.cocone
          (pair (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
have apply : IsColimit.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (F := Discrete.functor fun (j : Fin (n + 1)) ↦ F.obj (f j))
  (Cofan.mk
    (F.obj
      (Cocone.pt.{0, v, 0, u} (F :=
        pair (f 0)
          (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
            (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
        (colimit.cocone
          (pair (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
    fun (j : Fin (n + 1)) ↦
    F.map
      (Fin.cases (motive := fun (x : Fin (n + 1)) ↦
        f x ⟶
          Cocone.pt.{0, v, 0, u} (F :=
            pair (f 0)
              (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
            (colimit.cocone
              (pair (f 0)
                (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                  (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
        (BinaryCofan.inl
          (colimit.cocone
            (pair (f 0)
              (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
        (fun (i : Fin n) ↦
          NatTrans.app (Cocone.ι (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))) { as := i } ≫
            BinaryCofan.inr
              (colimit.cocone
                (pair (f 0)
                  (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                    (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
        j))
Tactic: apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteCoproducts.{v, u} C
n : ℕ
K : Functor.{0, v, 0, u} (Discrete (Fin n)) C
that : (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun (x : Discrete (Fin n)) ↦
    match (motive :=
      (x : Discrete (Fin n)) →
        Functor.obj.{0, v, 0, u} (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) x ≅ K.obj x)
      x with
    | { as := i } =>
      Iso.refl
        (Functor.obj.{0, v, 0, u} (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 })
          { as := i : Discrete (Fin n) })
⊢ PreservesColimit K F
have this : PreservesColimit (J := Discrete (Fin n)) (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) F
Tactic: haveI := preserves_fin_of_preserves_binary_and_initial F n fun n => K.obj ⟨n⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ Functor.map (Functor.obj (Functor.const J) i.pt) f ≫ i.ι ≫ c₁.π.app { as := j₂ } =
    (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
have dsimp : 𝟙 i.pt ≫ i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ 𝟙 i.pt ≫ i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
have rw : i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
Tactic: rw [Category.id_comp, Category.assoc, ← hs ⟨⟨_, _⟩, f⟩, i.condition_assoc, ht]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
rw : i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
⊢ 𝟙 i.pt ≫ i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
have rw₁ : i.ι ≫ c₁.π.app { as := j₂ } = i.ι ≫ c₁.π.app { as := j₁ : Discrete J } ≫ F.map f
Tactic: rw [Category.id_comp, Category.assoc, ← hs ⟨⟨_, _⟩, f⟩, i.condition_assoc, ht]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
rw : i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
rw₁ : i.ι ≫ c₁.π.app { as := j₂ } = i.ι ≫ c₁.π.app { as := j₁ : Discrete J } ≫ F.map f
⊢ 𝟙 i.pt ≫ i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
have rw₂ : Eq (α := i.pt ⟶ F.obj j₂) (i.ι ≫ c₁.π.app { as := j₂ })
  (i.ι ≫ s ≫ c₂.π.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f })
Tactic: rw [Category.id_comp, Category.assoc, ← hs ⟨⟨_, _⟩, f⟩, i.condition_assoc, ht]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
rw : i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
rw₁ : i.ι ≫ c₁.π.app { as := j₂ } = i.ι ≫ c₁.π.app { as := j₁ : Discrete J } ≫ F.map f
rw₂ :
  Eq (α := i.pt ⟶ F.obj j₂) (i.ι ≫ c₁.π.app { as := j₂ })
    (i.ι ≫ s ≫ c₂.π.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f })
⊢ 𝟙 i.pt ≫ i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
have rw₃ : Eq (α := i.pt ⟶ F.obj j₂) (i.ι ≫ c₁.π.app { as := j₂ })
  (i.ι ≫ t ≫ c₂.π.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f })
Tactic: rw [Category.id_comp, Category.assoc, ← hs ⟨⟨_, _⟩, f⟩, i.condition_assoc, ht]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
rw : i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
rw₁ : i.ι ≫ c₁.π.app { as := j₂ } = i.ι ≫ c₁.π.app { as := j₁ : Discrete J } ≫ F.map f
rw₂ :
  Eq (α := i.pt ⟶ F.obj j₂) (i.ι ≫ c₁.π.app { as := j₂ })
    (i.ι ≫ s ≫ c₂.π.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f })
rw₃ :
  Eq (α := i.pt ⟶ F.obj j₂) (i.ι ≫ c₁.π.app { as := j₂ })
    (i.ι ≫ t ≫ c₂.π.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f })
⊢ 𝟙 i.pt ≫ i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
have rw₄ : Eq (α := i.pt ⟶ F.obj j₂) (i.ι ≫ c₁.π.app { as := j₂ })
  (i.ι ≫
    c₁.π.app
      {
        as :=
          (Sigma.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f)).2 })
Tactic: rw [Category.id_comp, Category.assoc, ← hs ⟨⟨_, _⟩, f⟩, i.condition_assoc, ht]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
⊢ q.pt ⟶ (buildLimit s t hs ht i).pt
have refine_1 : q.1 ⟶ c₁.pt
Tactic: refine hi.lift (Fork.ofι ?_ ?_)