awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ Eq (α := G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (CategoryStruct.comp (Y :=
        G.obj (piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
        (G.map
          (Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }))
        (G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f)) :
      G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (G.map (Pi.π K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) :
      G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
have simp : Eq (α := G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
  (G.map
      (NatTrans.app
        (Cone.π
          (Fan.mk (piObj.{w, v, u} K.obj) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }))
        { as := f }) :
    G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
  (G.map (Pi.π K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) :
    G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
Tactic: simp only [← G.map_comp, limit.lift_π]
-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ Fork (G.map s) (G.map t)
have apply : G.map i ≫ G.map s = G.map i ≫ G.map t
Tactic: apply Fork.ofι (G.map i)
-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ G.map i ≫ G.map s = G.map i ≫ G.map t
have rw : G.map (i ≫ s) = G.map (i ≫ t)
Tactic: rw [← G.map_comp, ← G.map_comp]
-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ G.map (i ≫ s) = G.map (i ≫ t)
have apply : i ≫ s = i ≫ t
Tactic: apply congrArg G.map
-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ IsLimit (F := parallelPair (G.map s) (G.map t)) (Fork.ofι (G.map i) ⋯ : Fork (G.map s) (G.map t))
have l : IsLimit (Fork.ofι i sorry)
Tactic: apply isLimitForkMapOfIsLimit
-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
l : IsLimit (Fork.ofι i ⋯)
⊢ IsLimit (F := parallelPair (G.map s) (G.map t)) (Fork.ofι (G.map i) ⋯ : Fork (G.map s) (G.map t))
have w : i ≫ s = i ≫ t
Tactic: apply isLimitForkMapOfIsLimit
-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ buildLimit (c₁ := Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) (c₂ :=
      Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
        G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f))
      (G.map s) (G.map t) ⋯ ⋯ (Fork.ofι (G.map i) ⋯) ≅
    G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t)))
have refine : ∀ (j : J),
  NatTrans.app
      (Cone.π
        (buildLimit (c₁ := Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) (c₂ :=
          Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f))
          (G.map s) (G.map t) sorry sorry (Fork.ofι (G.map i) sorry)))
      j =
    Iso.hom
        (Iso.refl
          (Cone.pt.{w, v₂, w, u₂} (J := J) (F := K ⋙ G)
            (buildLimit (c₁ := Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) (c₂ :=
              Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f))
              (G.map s) (G.map t) sorry sorry (Fork.ofι (G.map i) sorry)))) ≫
      (G.mapCone (buildLimit s t sorry sorry (limit.cone (parallelPair s t)))).π.app j
Tactic: refine Cone.ext (Iso.refl _) ?_
-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
j : J
⊢ NatTrans.app
      (Cone.π
        (buildLimit (c₁ := Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) (c₂ :=
          Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f))
          (G.map s) (G.map t) ⋯ ⋯ (Fork.ofι (G.map i) ⋯)))
      j =
    Iso.hom
        (Iso.refl
          (Cone.pt.{w, v₂, w, u₂} (J := J) (F := K ⋙ G)
            (buildLimit (c₁ := Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) (c₂ :=
              Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f))
              (G.map s) (G.map t) ⋯ ⋯ (Fork.ofι (G.map i) ⋯)))) ≫
      (G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t)))).π.app j
have dsimp : G.map (equalizer.ι s t) ≫ G.map (Pi.π K.obj j) =
  𝟙 (G.obj (equalizer s t)) ≫ G.map (equalizer.ι s t ≫ limit.π (Discrete.functor K.obj) { as := j : Discrete J })
Tactic: dsimp [P, Q, I, i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasTerminal.{v, u} C
inst_3 : HasPullbacks.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
⊢ PreservesFiniteLimits G
have this : HasFiniteLimits.{v, u} C
Tactic: have : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasTerminal.{v, u} C
inst_3 : HasPullbacks.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
this : HasFiniteLimits.{v, u} C
⊢ PreservesFiniteLimits G
have this₁ : PreservesLimitsOfShape (Discrete WalkingPair) G
Tactic: have : PreservesLimitsOfShape (Discrete WalkingPair) G :=
    preservesBinaryProducts_of_preservesTerminal_and_pullbacks G
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasTerminal.{v, u} C
inst_3 : HasPullbacks.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
this_1 : HasFiniteLimits.{v, u} C
this : PreservesLimitsOfShape (Discrete WalkingPair) G
⊢ PreservesFiniteLimits G
have this₁ : PreservesLimitsOfShape WalkingParallelPair G
Tactic: have : PreservesLimitsOfShape WalkingParallelPair G :=
    preservesEqualizers_of_preservesPullbacks_and_binaryProducts G
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasTerminal.{v, u} C
inst_3 : HasPullbacks.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
this_1 : HasFiniteLimits.{v, u} C
this_2 : PreservesLimitsOfShape (Discrete WalkingPair) G
this : PreservesLimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteLimits G
have this₁ : PreservesFiniteProducts G
Tactic: have : PreservesFiniteProducts G := .of_preserves_binary_and_terminal _
-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{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).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      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).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π =
    (c₂.ι.app { as := j₁ : Discrete J } ≫ i.π) ≫ Functor.map (Functor.obj (Functor.const J) i.pt) f
have dsimp : F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = (c₂.ι.app { as := j₁ : Discrete J } ≫ i.π) ≫ 𝟙 i.pt
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{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).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      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).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = (c₂.ι.app { as := j₁ : Discrete J } ≫ i.π) ≫ 𝟙 i.pt
have reassoced : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} {h : c₂.pt ⟶ W},
  c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
    F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫ c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
Tactic: have reassoced (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} {h : _ ⟶ W} :
          c₁.ι.app ⟨f⟩ ≫ s ≫ h = F.map f.snd ≫ c₂.ι.app ⟨f.fst.snd⟩ ≫ h := by
            simp only [← Category.assoc, eq_whisker (hs f)]
-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{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).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      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).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
reassoced :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} {h : c₂.pt ⟶ W},
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
⊢ F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = (c₂.ι.app { as := j₁ : Discrete J } ≫ i.π) ≫ 𝟙 i.pt
have rw : F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = c₂.ι.app { as := j₁ } ≫ i.π
Tactic: rw [Category.comp_id, ← reassoced ⟨⟨_, _⟩, f⟩, i.condition, ← Category.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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{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).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      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).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
reassoced :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} {h : c₂.pt ⟶ W},
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
rw : F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = c₂.ι.app { as := j₁ } ≫ i.π
⊢ F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = (c₂.ι.app { as := j₁ : Discrete J } ≫ i.π) ≫ 𝟙 i.pt
have rw₁ : c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫
    s ≫ i.π =
  c₂.ι.app { as := j₁ } ≫ i.π
Tactic: rw [Category.comp_id, ← reassoced ⟨⟨_, _⟩, f⟩, i.condition, ← Category.assoc, ht]